diff options
| -rw-r--r-- | soat.ipkg | 1 | ||||
| -rw-r--r-- | src/Soat/SecondOrder/Signature/Lift.idr | 14 |
2 files changed, 15 insertions, 0 deletions
@@ -10,3 +10,4 @@ modules = Soat.Data.Product , Soat.Relation , Soat.SecondOrder.Algebra , Soat.SecondOrder.Signature + , Soat.SecondOrder.Signature.Lift 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) |