From 07b5788d540bb81334389d68eeddfe81eadb1c90 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 29 Nov 2022 14:54:22 +0000
Subject: refactor: name arguments.

---
 src/Soat/FirstOrder/Term.idr | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src')

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 =
-- 
cgit v1.2.3