Define first-order signatures.

1 files changed, 15 insertions, 0 deletions

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