LP, the Larch Prover -- The declare command

Except for certain predefined logical, equality, and conditional operators, all identifiers for sorts, variables, and operators must be declared in a declare command before any other use.

Syntax

<declare-command> ::= declare ( <sortDecs> | <varDecs> | <opDecs> )
<sortDecs>        ::= sorts <sort>+,
<varDecs>         ::= variables <varDec>+[,]
<varDec>          ::= <variableId>+, : <sort>
<opDecs>          ::= operators <opDec>+[,]
<opDec>           ::= <opForm>+, : <signature>

Restrictions: There must be at least one marker in each <opForm> that contains a <simpleOpForm>. The number of marker symbols in any <opForm> not containing a <functionId> must equal the number of sorts in the domain of the operator's signature. A period (.) can be declared as an infix operator, but not as a prefix or a postfix operator. The predefined operators cannot be overloaded with user-defined signatures.

Notes: The words sorts, operators, and variables can be abbreviated by any prefix, as well as by ops and vars.

Examples

declare sorts Nat, Set
declare variables i, j: Nat, s: Set
declare operators
  0:                     -> Nat
  s, __!:       Nat      -> Nat
  __+__, __*__: Nat, Nat -> Nat
  {}:                    -> Set
  {__}:         Nat      -> Set
  __\U__:       Set, Set -> Set
  ~__:          Set      -> Set
  ..

Usage

The declare sorts command introduces identifiers for use as sorts.

The declare variables command introduces variables with the indicated sorts.

The declare operators commands introduces operators with the indicated signatures. Marker symbols (__) in an <opForm> indicate where the arguments of the operator are placed when it is used in a term.

LP at times creates variables and operators in response to user commands. To avoid problems, it is a good idea for users to declare the identifiers they need before issuing commands (such as prove) that may cause LP to appropriate an identifier for its own use (e.g., by creating a variable s1 of sort Set and thereby preventing the user from later using s1 as a constant of sort Set).

The display symbols command produces a list of all declared identifiers.