blob: d3e9f059ca617a400f5485944c822643e345c6c1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
module Soat.SecondOrder.Signature
%default total
public export
record Signature where
constructor MkSignature
T : Type
0 O : T -> List (Pair (List T) T) -> Type
public export
record Op (0 sig : Signature) (0 t : sig.T) where
constructor MkOp
{arity : List (Pair (List sig.T) sig.T)}
op : sig.O t arity
|
