summaryrefslogtreecommitdiff
path: root/src/Soat/SecondOrder/Algebra/Lift.idr
diff options
context:
space:
mode:
authorGreg Brown <greg.brown01@ed.ac.uk>2022-12-05 14:43:50 +0000
committerGreg Brown <greg.brown01@ed.ac.uk>2022-12-05 14:43:50 +0000
commitf77aeb6c4b25b381e897a4ab59c1008e34005404 (patch)
tree07e8f0ec56bda51e9489b7b49558a3c2d860f932 /src/Soat/SecondOrder/Algebra/Lift.idr
parent8ff37b98737f4af5bd11d3006ae1b26902a1a82f (diff)
refactor: rename MakeRawAlgebra -> MkRawAlgebra.
Diffstat (limited to 'src/Soat/SecondOrder/Algebra/Lift.idr')
-rw-r--r--src/Soat/SecondOrder/Algebra/Lift.idr4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Soat/SecondOrder/Algebra/Lift.idr b/src/Soat/SecondOrder/Algebra/Lift.idr
index b08eb0e..5be7dd1 100644
--- a/src/Soat/SecondOrder/Algebra/Lift.idr
+++ b/src/Soat/SecondOrder/Algebra/Lift.idr
@@ -16,7 +16,7 @@ import Soat.SecondOrder.Signature.Lift
public export
project : SecondOrder.Algebra.RawAlgebra (lift sig) -> (ctx : List sig.T)
-> FirstOrder.Algebra.RawAlgebra sig
-project a ctx = MakeRawAlgebra
+project a ctx = MkRawAlgebra
(flip a.U ctx)
(\op => a.sem ctx (MkOp (Op op.op)) . wrap (MkPair []))
@@ -133,7 +133,7 @@ indexFunc tms = MkIFunction
public export
Initial : (0 sig : _) -> SecondOrder.Algebra.RawAlgebra (lift sig)
-Initial sig = MakeRawAlgebra
+Initial sig = MkRawAlgebra
(\t, ctx => Term sig (flip Elem ctx) t)
(\t, f => bindTerm {a = Free _} (renameBodyFunc f).func)
(\_, (MkOp (Op op)) => Call (MkOp op) . unwrap (MkPair []))