From 8516f58b1d4af49126f84c8e90d1ba182515a1b6 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 2 Mar 2024 14:13:02 -0800 Subject: [PATCH] Remove helper comment. Signed-off-by: Danila Fedorin --- Main.agda | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/Main.agda b/Main.agda index af67b7b..99ae755 100644 --- a/Main.agda +++ b/Main.agda @@ -56,14 +56,4 @@ dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} { open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂) --- module Fixedpoint {a} {A : Set a} --- {h : ℕ} --- {_≈_ : A → A → Set a} --- {_⊔_ : A → A → A} {_⊓_ : A → A → A} --- (≈-dec : IsDecidable _≈_) --- (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) --- (f : A → A) --- (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA) --- (IsFiniteHeightLattice._≼_ flA) f) where - main = run {0ℓ} (putStrLn (showMap aᶠ))