From f77aeb6c4b25b381e897a4ab59c1008e34005404 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Mon, 5 Dec 2022 14:43:50 +0000
Subject: refactor: rename MakeRawAlgebra -> MkRawAlgebra.

---
 src/Soat/FirstOrder/Algebra.idr           | 10 +---------
 src/Soat/FirstOrder/Algebra/Coproduct.idr |  2 +-
 src/Soat/FirstOrder/Term.idr              |  2 +-
 3 files changed, 3 insertions(+), 11 deletions(-)

(limited to 'src/Soat/FirstOrder')

diff --git a/src/Soat/FirstOrder/Algebra.idr b/src/Soat/FirstOrder/Algebra.idr
index b8cbc0c..f002dec 100644
--- a/src/Soat/FirstOrder/Algebra.idr
+++ b/src/Soat/FirstOrder/Algebra.idr
@@ -12,20 +12,12 @@ public export 0
 algebraOver : (sig : Signature) -> (U : sig.T -> Type) -> Type
 algebraOver sig x = {t : sig.T} -> (op : Op sig t) -> x ^ op.arity -> x t
 
-public export 0
-algebraOver' : (sig : Signature) -> (U : sig.T -> Type) -> Type
-algebraOver' sig x = {t : sig.T} -> (op : Op sig t) -> map x op.arity `ary` x t
-
 public export
 record RawAlgebra (0 sig : Signature) where
-  constructor MakeRawAlgebra
+  constructor MkRawAlgebra
   0 U : sig.T -> Type
   sem : sig `algebraOver` U
 
-public export
-MkRawAlgebra : (0 U : sig.T -> Type) -> (sem : sig `algebraOver'` U) -> RawAlgebra sig
-MkRawAlgebra u sem = MakeRawAlgebra u (\o => uncurry (sem o))
-
 public export
 record RawAlgebraWithRelation (0 sig : Signature) where
   constructor MkRawAlgebraWithRelation
diff --git a/src/Soat/FirstOrder/Algebra/Coproduct.idr b/src/Soat/FirstOrder/Algebra/Coproduct.idr
index d0b1b14..84ac436 100644
--- a/src/Soat/FirstOrder/Algebra/Coproduct.idr
+++ b/src/Soat/FirstOrder/Algebra/Coproduct.idr
@@ -67,7 +67,7 @@ parameters {0 x, y : RawAlgebraWithRelation sig}
 
 public export
 Coproduct : (x, y : RawAlgebra sig) -> RawAlgebra sig
-Coproduct x y = MakeRawAlgebra
+Coproduct x y = MkRawAlgebra
   { U   = CoproductSet sig x.U y.U
   , sem = Call
   }
diff --git a/src/Soat/FirstOrder/Term.idr b/src/Soat/FirstOrder/Term.idr
index 4a51f94..eaa2da2 100644
--- a/src/Soat/FirstOrder/Term.idr
+++ b/src/Soat/FirstOrder/Term.idr
@@ -127,7 +127,7 @@ namespace Rel
 
 public export
 Free : (0 V : sig.T -> Type) -> RawAlgebra sig
-Free v = MakeRawAlgebra (Term sig v) Call
+Free v = MkRawAlgebra (Term sig v) Call
 
 public export
 FreeIsAlgebra : (v : ISetoid sig.T) -> IsAlgebra sig (Free v.U) ((~=~) v.relation)
-- 
cgit v1.2.3