diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:07:32 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-25 15:07:32 +0000 |
| commit | d7fa1ccbbb6dcf78d16b8adfeab4e1a167a2f0b3 (patch) | |
| tree | b1edf7ec9dcd3d12350ab8465034cf35546e074c /src | |
| parent | 466a0a43490abf471ee879571f0faf40343c37c4 (diff) | |
refactor: rename bind -> bindHomo.
Diffstat (limited to 'src')
| -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) |