diff options
| author | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-29 14:54:22 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown01@ed.ac.uk> | 2022-11-29 14:54:22 +0000 |
| commit | 07b5788d540bb81334389d68eeddfe81eadb1c90 (patch) | |
| tree | 9153fd2b26067d41f35bf8c453401236cd71bd38 | |
| parent | e8d6ac1f1d9c05b71bb9098a1590e29e5c93b0b8 (diff) | |
refactor: name arguments.
| -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 = |