diff options
Diffstat (limited to 'src/Soat')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 07ab248..99f7e32 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -186,14 +186,14 @@ bindHomo env = MkHomomorphism _ (bindIsHomo _ env) public export bindUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) - -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) + -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.relation t (f.func t tm) (g.func t tm) public export bindsUnique' : {v : ISetoid sig.T} -> {a : Algebra sig} -> (f, g : Homomorphism (FreeAlgebra v) a) - -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) + -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (g.func t (Done i))) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) -> Pointwise a.relation (map f.func tms) (map g.func tms) @@ -212,7 +212,7 @@ bindsUnique' f g cong (t :: ts) = bindUnique' f g cong t :: bindsUnique' f g con public export bindUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) - -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) + -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {t : sig.T} -> (tm : Term sig v.U t) -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm) bindUnique env f = bindUnique' f (bindHomo env) @@ -220,7 +220,7 @@ bindUnique env f = bindUnique' f (bindHomo env) public export bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid) -> (f : Homomorphism (FreeAlgebra v) a) - -> ({t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) + -> (cong : {t : sig.T} -> (i : v.U t) -> a.relation t (f.func t (Done i)) (env.func t i)) -> {ts : List sig.T} -> (tms : Term sig v.U ^ ts) -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms) bindsUnique env f cong ts = |