From b3bec7d483839c44a70fd014244287b8cf662b84 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 22 Nov 2022 16:57:21 +0000
Subject: Define second-order signatures.

---
 src/Soat/SecondOrder/Signature.idr | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 src/Soat/SecondOrder/Signature.idr

(limited to 'src/Soat')

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
-- 
cgit v1.2.3