diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 14:30:36 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 14:30:36 +0000 |
| commit | 865e9dbdd0a7ed2b0dad75f2c672ad84e9e85bcc (patch) | |
| tree | 72488a96f195321a26c5248a156941ed9ce42fe6 /src/Soat/FirstOrder/Term.idr | |
| parent | 7c8591b566baeb6af42a22b8979c53ebdcab5479 (diff) | |
Make proofs relevant.
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 5f5e57b..af6539b 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -116,12 +116,12 @@ public export FreeAlgebra : ISetoid sig.T -> Algebra sig FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v) -public export 0 +public export bindTermCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm' -> a.rel t (bindTerm {a = a.raw} env.f tm) (bindTerm {a = a.raw} env.f tm') -public export 0 +public export bindTermsCong : {a : Algebra sig} -> (env : SetoidEnvironment x a.setoid) -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms' -> Pointwise a.rel (bindTerms {a = a.raw} env.f tms) (bindTerms {a = a.raw} env.f tms') @@ -148,15 +148,15 @@ public export bind : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> Homomorphism (FreeAlgebra v) a bind env = MkHomomorphism _ (bindHomo _ env) -public export 0 -bindUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +public export +bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i)) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.rel t (f.f t tm) ((Term.bind {a = a} env).f t tm) -public export 0 -bindsUnique : {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) +public export +bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : SetoidEnvironment v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) -> ({t : sig.T} -> (i : v.U t) -> a.rel t (f.f t (Done i)) (env.f t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) |