From f01df5af4b130eb279d3c999b04e74d7d881f30e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 31 Dec 2024 12:55:29 -0800 Subject: [PATCH] Slightly tweak module style in Forward.agda Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 3e4627c..9702bf9 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -259,7 +259,7 @@ module WithProg (prog : Program) where open WithEvaluator open WithEvaluator using (result; analyze; result≈analyze-result) public - private module WithInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where + private module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where open LatticeInterpretation latticeInterpretationˡ using () renaming @@ -300,8 +300,6 @@ module WithProg (prog : Program) where ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss')) - open WithInterpretation - module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where open Evaluator evaluator open LatticeInterpretation interpretation @@ -314,8 +312,8 @@ module WithProg (prog : Program) where {{evaluator}} : Evaluator {{interpretation}} : LatticeInterpretation isLatticeˡ - open Evaluator evaluator - open LatticeInterpretation interpretation + open Evaluator evaluator public + open LatticeInterpretation interpretation public field valid : IsValid