summaryrefslogtreecommitdiff
path: root/src/Soat/FirstOrder/Signature.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Soat/FirstOrder/Signature.idr')
-rw-r--r--src/Soat/FirstOrder/Signature.idr15
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