# 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.
`<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`).