From 00fcc3517b7f680d31028abe83664a96305101b6 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Thu, 24 Nov 2022 14:13:43 +0000
Subject: Define lifting of first-order signatures.

---
 src/Soat/SecondOrder/Signature/Lift.idr | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 src/Soat/SecondOrder/Signature/Lift.idr

(limited to 'src')

diff --git a/src/Soat/SecondOrder/Signature/Lift.idr b/src/Soat/SecondOrder/Signature/Lift.idr
new file mode 100644
index 0000000..159cdb3
--- /dev/null
+++ b/src/Soat/SecondOrder/Signature/Lift.idr
@@ -0,0 +1,14 @@
+module Soat.SecondOrder.Signature.Lift
+
+import public Soat.FirstOrder.Signature
+import public Soat.SecondOrder.Signature
+
+%default total
+
+public export
+data LiftOp : (O : a -> List a -> Type) -> (i : a) -> (ctx : List (Pair (List a) a)) -> Type where
+  Op : forall i . {ctx : List a} -> (op : o i ctx) -> LiftOp o i (map (MkPair []) ctx)
+
+public export
+lift : FirstOrder.Signature.Signature -> SecondOrder.Signature.Signature
+lift sig = MkSignature sig.T (LiftOp sig.O)
-- 
cgit v1.2.3