Define second-order signatures.

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