diff options
Diffstat (limited to 'src/Soat/FirstOrder')
| -rw-r--r-- | src/Soat/FirstOrder/Term.idr | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr index 7c2fca1..8f1b71a 100644 --- a/src/Soat/FirstOrder/Term.idr +++ b/src/Soat/FirstOrder/Term.idr @@ -138,9 +138,9 @@ bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid) bindTermsCong env = bindTermsCong' env.cong public export -bindHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) +bindIsHomo : (a : Algebra sig) -> (env : IFunction v a.setoid) -> IsHomomorphism (FreeAlgebra v) a (\t => bindTerm {a = a.raw} env.func) -bindHomo a env = MkIsHomomorphism +bindIsHomo a env = MkIsHomomorphism (\t, eq => bindTermCong env eq) (\op, tms => a.algebra.semCong op $ @@ -149,15 +149,15 @@ bindHomo a env = MkIsHomomorphism bindTermsIsMap {a = a.raw} env.func tms) public export -bind : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a -bind env = MkHomomorphism _ (bindHomo _ env) +bindHomo : {a : Algebra sig} -> (env : IFunction v a.setoid) -> Homomorphism (FreeAlgebra v) a +bindHomo env = MkHomomorphism _ (bindIsHomo _ env) 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.rel t (f.f t (Done i)) (env.func 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) + -> a.rel t (f.f t tm) (bindTerm {a = a.raw} env.func tm) public export bindsUnique : {v : ISetoid sig.T} -> {a : Algebra sig} -> (env : IFunction v a.setoid) |