LP, the Larch Prover -- Signatures

The signature of an operator specifies its domain and range sorts.

Syntax

<signature> ::= <domain> -> <range>
<domain>    ::= <sort>*,
<range>     ::= <sort>

Examples

->Nat
Signature for a nullary operator (constant) of sort Nat

Bool->Bool
Signature for a unary operator from sort Bool to sort Bool

Nat,Nat->Nat
Signature for a binary operator from sort Nat to sort Nat

Element,Set->Set
Signature for a binary operator from sorts Element and Set to sort Set

Usage

Signatures appear in declarations and qualifications for operators.