LP, the Larch Prover — Sorts

A sort is a symbol that represents a non-empty set of objects. In LP, distinct sorts represent disjoint sets of objects. Sorts can be simple or compound. At present, LP accords no special treatment to compound sorts.

Syntax

<sort>          ::= <simple-sort> | <compound-sort>
<simple-sort>   ::= <simpleId>
<compound-sort> ::= <simpleId> "[" <sort>+, "]"

Examples

Nat
Set[Nat]
Map[Set[A],A]

Usage

LP automatically declares the sort Bool and treats it as representing a set containing two objects, true and false. LP also automatically declares several logical operators for this sort.

All sorts other than Bool must be declared in a declare sorts command. Except for Bool and bool, which denote the same sort, case is significant in sort identifiers. Thus Nat and nat are different sorts.

Since distinct sorts represent disjoint sets of objects, users who want to consider one ``sort'' (e.g., Nat) as a subset of another (e.g., Int) must resort to one of two devices. They can define the larger as a sort and the smaller by means of a unary predicate (e.g., isNat:Int->Bool). Alternatively, they can define both as sorts and introduce a mapping from one into the other (e.g., asInt:Nat->Int).