diff options
Diffstat (limited to 'src/Soat/FirstOrder/Term.idr')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 92f35cc..e39e7ac 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -157,16 +157,16 @@ 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.f t (Done i)) (g.f t (Done i))) + -> ({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.f t tm) (g.f t tm) + -> 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.f t (Done i)) (g.f t (Done i))) + -> ({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.f tms) (map g.f tms) + -> Pointwise a.relation (map f.func tms) (map g.func tms) bindUnique' f g cong (Done i) = cong i bindUnique' f g cong (Call op ts) = @@ -183,17 +183,17 @@ 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.f t (Done i)) (env.func t i)) + -> ({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.f t tm) (bindTerm {a = a.raw} env.func tm) + -> a.relation t (f.func t tm) (bindTerm {a = a.raw} env.func tm) 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.f t (Done i)) (env.func t i)) + -> ({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.f tms) (bindTerms {a = a.raw} env.func tms) + -> Pointwise a.relation (map f.func tms) (bindTerms {a = a.raw} env.func tms) bindsUnique env f cong ts = pwTrans (\i => (a.algebra.equivalence i).trans) (bindsUnique' f (bindHomo env) cong ts) $ |