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

Move proof of least element into FiniteHeightLattice

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2025-07-26 13:16:22 +02:00
parent d99d4a2893
commit f5457d8841
4 changed files with 31 additions and 22 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
Analysis/Forward.agda
View File

@@ -21,7 +21,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
using () renaming (isLattice to isLatticeˡ)
module WithProg (prog : Program) where
open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
open import Analysis.Forward.Evaluation L prog
open Program prog
@@ -66,7 +66,7 @@ module WithProg (prog : Program) where
(joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
-- The fixed point of the 'analyze' function is our final goal.
open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
open import Fixedpoint analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
using ()
renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
public