DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Slightly tweak module style in Forward.agda

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-12-31 12:55:29 -08:00
parent b28994e1d2
commit f01df5af4b
1 changed files with 3 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Analysis/Forward.agda
View File

@ -259,7 +259,7 @@ module WithProg (prog : Program) where
open WithEvaluator open WithEvaluator
open WithEvaluator using (result; analyze; result≈analyze-result) public 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ˡ open LatticeInterpretation latticeInterpretationˡ
using () using ()
renaming renaming
@ -300,8 +300,6 @@ module WithProg (prog : Program) where
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ ⟦⟧ᵛ-⊔ᵛ-∨ {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
(inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss')) (inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
open WithInterpretation
module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
open Evaluator evaluator open Evaluator evaluator
open LatticeInterpretation interpretation open LatticeInterpretation interpretation
@ -314,8 +312,8 @@ module WithProg (prog : Program) where
{{evaluator}} : Evaluator {{evaluator}} : Evaluator
{{interpretation}} : LatticeInterpretation isLatticeˡ {{interpretation}} : LatticeInterpretation isLatticeˡ
open Evaluator evaluator open Evaluator evaluator public
open LatticeInterpretation interpretation open LatticeInterpretation interpretation public
field field
valid : IsValid valid : IsValid