From 4c0094fc3a223746005ae52f74ff3e76d0dee1fe Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Tue, 22 Nov 2022 16:53:49 +0000
Subject: Define first-order signatures.

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

diff --git a/src/Soat/FirstOrder/Signature.idr b/src/Soat/FirstOrder/Signature.idr
new file mode 100644
index 0000000..01cfb2b
--- /dev/null
+++ b/src/Soat/FirstOrder/Signature.idr
@@ -0,0 +1,15 @@
+module Soat.FirstOrder.Signature
+
+%default total
+
+public export
+record Signature where
+  constructor MkSignature
+  T : Type
+  0 O : T -> List T -> Type
+
+public export
+record Op (0 sig : Signature) (0 t : sig.T) where
+  constructor MkOp
+  {arity : List sig.T}
+  op : sig.O t arity
-- 
cgit v1.2.3