diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Soat/SecondOrder/Signature/Lift.idr | 14 |
1 files changed, 14 insertions, 0 deletions
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) |