src/Soat/FirstOrder/Signature.idr


1
2
3
4
5
6
7
8
9
10
11
12
13
14
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