diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:49:23 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-12-05 15:49:23 +0000 |
| commit | 1f378ce7d61e16a3dc805ce63f87b5b8202f3f8e (patch) | |
| tree | 7dd559a7e8b2107730e66d89728040e0543c894a | |
| parent | 2301a52aaad73e2f70aba46682ec69686f35aa6c (diff) | |
refactor: remove commented code.
| -rw-r--r-- | src/Soat/SecondOrder/Algebra/Lift.idr | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr index 4ed29cf..9a88446 100644 --- a/src/Soat/SecondOrder/Algebra/Lift.idr +++ b/src/Soat/SecondOrder/Algebra/Lift.idr @@ -119,14 +119,6 @@ indexFunc tms = MkIFunction (\_ => index tms) (\_ => ((FreeIsAlgebra (isetoid (flip Elem _))).equivalence _).equalImpliesEq . cong (index tms)) --- renameFunc : (f : ctx `Sublist` ctx') --- -> IFunction --- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx))).setoid --- (FreeAlgebra {sig = sig} (isetoid (flip Elem ctx'))).setoid --- renameFunc f = MkIFunction --- (\_ => bindTerm {a = Free _} (renameBodyFunc f).func) --- (\t => bindTermCong {a = FreeAlgebra (isetoid (flip Elem _))} (renameBodyFunc f)) - public export Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig) Initial sig = MkRawAlgebra @@ -175,23 +167,6 @@ InitialIsAlgebra sig = MkIsAlgebra equalImpliesPwEq Refl) $ equalImpliesPwEq $ mapUnwrap _ _) - -- Pointwise.map (\_ => tmRelReflexive (\_ => MkReflexive reflexive)) $ - -- transitive (equalImpliesPwEq $ bindTermsIsMap {a = Free _} _ (unwrap (MkPair []) tms)) $ - -- transitive - -- (mapIntro - -- (\t, eq => - -- bindTermCong' - -- {v = isetoid (flip Elem _)} - -- {a = FreeAlgebra (isetoid (flip Elem _))} - -- (\_, Refl => Done' $ sym $ curryUncurry (curry f) _) $ - -- tmRelReflexive (\_ => MkReflexive reflexive) $ - -- eq) $ - -- equalImpliesPwEq Refl) $ - -- equalImpliesPwEq $ - -- mapUnwrap - -- (MkPair []) - -- (\ty => (renameFunc (reflexive ++ f)).func (snd ty)) - -- tms) (\_, _ => Done' Refl) (\t, f, tm, tms => bindUnique |