refactor: rename x -> v

1 files changed, 18 insertions, 20 deletions

diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index ff0796c..5935254 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -12,16 +12,14 @@ import Soat.Relation
 
 public export
 data Term : (0 sig : Signature) -> (0 _ : sig.T -> Type) -> sig.T -> Type where
-  Done : (i : x t) -> Term sig x t
-  Call : (op : Op sig t) -> (ts : Term sig x ^ op.arity) -> Term sig x t
+  Done : (i : v t) -> Term sig v t
+  Call : (op : Op sig t) -> (ts : Term sig v ^ op.arity) -> Term sig v t
 
 public export
-bindTerm : {auto a : RawAlgebra sig}
-  -> IFunc x a.U -> {t : _} -> Term sig x t -> a.U t
+bindTerm : {auto a : RawAlgebra sig} -> IFunc v a.U -> {t : _} -> Term sig v t -> a.U t
 
 public export
-bindTerms : {auto a : RawAlgebra sig}
-  -> IFunc x a.U -> {ts : _} -> Term sig x ^ ts -> a.U ^ ts
+bindTerms : {auto a : RawAlgebra sig} -> IFunc v a.U -> {ts : _} -> Term sig v ^ ts -> a.U ^ ts
 
 bindTerm         env (Done i)     = env _ i
 bindTerm {a = a} env (Call op ts) = a.sem op (bindTerms env ts)
@@ -31,23 +29,23 @@ bindTerms env (t :: ts) = bindTerm env t :: bindTerms env ts
 
 public export
 bindTermsIsMap : {auto a : RawAlgebra sig}
-  -> (env : IFunc x a.U) -> {ts : _} -> (tms : Term sig x ^ ts)
+  -> (env : IFunc v a.U) -> {ts : _} -> (tms : Term sig v ^ ts)
   -> bindTerms (\tm => env tm) tms = map (\t => bindTerm (\tm => env tm)) tms
 bindTermsIsMap env []        = Refl
 bindTermsIsMap env (t :: ts) = cong ((::) (bindTerm env t)) (bindTermsIsMap env ts)
 
 namespace Rel
   public export
-  data (~=~) : forall x . (0 r : IRel x) -> IRel (Term sig x)
+  data (~=~) : forall v . (0 r : IRel v) -> IRel (Term sig v)
     where
-    Done' : {0 x : sig.T -> Type} -> {0 r : IRel x}
-      -> {t : sig.T} -> {i, j : x t}
+    Done' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+      -> {t : sig.T} -> {i, j : v t}
       -> r t i j
-      -> (~=~) {sig = sig} {x = x} r t (Done i) (Done j)
-    Call' : {0 x : sig.T -> Type} -> {0 r : IRel x}
-      -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig x ^ op.arity}
-      -> Pointwise ((~=~) {sig = sig} {x = x} r) tms tms'
-      -> (~=~) {sig = sig} {x = x} r t (Call op tms) (Call op tms')
+      -> (~=~) {sig} {v} r t (Done i) (Done j)
+    Call' : {0 v : sig.T -> Type} -> {0 r : IRel v}
+      -> {t : sig.T} -> (op : Op sig t) -> {tms, tms' : Term sig v ^ op.arity}
+      -> Pointwise ((~=~) {sig} {v} r) tms tms'
+      -> (~=~) {sig} {v} r t (Call op tms) (Call op tms')
 
   tmRelRefl : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IReflexive V rel
     -> {t : sig.T} -> (tm : Term sig V t) -> (~=~) rel t tm tm
@@ -91,7 +89,7 @@ namespace Rel
 
   export
   tmRelEq : {0 V : sig.T -> Type} -> {0 rel : IRel V} -> IEquivalence V rel
-    -> IEquivalence _ ((~=~) {sig = sig} {x = V} rel)
+    -> IEquivalence _ ((~=~) {sig = sig} {v = V} rel)
   tmRelEq eq t = MkEquivalence
     (MkReflexive $ tmRelRefl (\t => (eq t).refl) _)
     (MkSymmetric $ tmRelSym (\t => (eq t).sym))
@@ -110,13 +108,13 @@ FreeAlgebra : ISetoid sig.T -> Algebra sig
 FreeAlgebra v = MkAlgebra _ _ (FreeIsAlgebra v)
 
 public export
-bindTermCong : {a : Algebra sig} -> (env : IFunction x a.setoid)
-  -> {t : sig.T} -> {tm, tm' : Term sig x.U t} -> (~=~) x.relation t tm tm'
+bindTermCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
+  -> {t : sig.T} -> {tm, tm' : Term sig v.U t} -> (~=~) v.relation t tm tm'
   -> a.rel t (bindTerm {a = a.raw} env.func tm) (bindTerm {a = a.raw} env.func tm')
 
 public export
-bindTermsCong : {a : Algebra sig} -> (env : IFunction x a.setoid)
-  -> {ts : List sig.T} -> {tms, tms' : Term sig x.U ^ ts} -> Pointwise ((~=~) x.relation) tms tms'
+bindTermsCong : {a : Algebra sig} -> (env : IFunction v a.setoid)
+  -> {ts : List sig.T} -> {tms, tms' : Term sig v.U ^ ts} -> Pointwise ((~=~) v.relation) tms tms'
   -> Pointwise a.rel (bindTerms {a = a.raw} env.func tms) (bindTerms {a = a.raw} env.func tms')
 
 bindTermCong         env (Done' i)     = env.cong _ i