blob: 159cdb3fa94d9d729d72919cfcc16bb302d0481b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
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)
|
