diff options
| -rw-r--r-- | src/Soat/SecondOrder/Signature.idr | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Soat/SecondOrder/Signature.idr b/src/Soat/SecondOrder/Signature.idr new file mode 100644 index 0000000..d3e9f05 --- /dev/null +++ b/src/Soat/SecondOrder/Signature.idr @@ -0,0 +1,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 |