# Sorts

A sort is a set of classified elements.

Sorts are declared between `[` and `]` as follows:

`[ `<sort-name> ... <sort-name>` ]`

[Convention] The first letter of a sort name is capitalized, e.g. Nat, Int, String.

Plural sorts can be declared with space separation.

The following is a declaration of Sort `Node` and Sort `Edge`:

`[ Node Edge ]`

## Subsort

A partial order over sets of sorts can be defined. For example, consider Sorts `Nat` and `Int` for natural numbers and integers respectively. All elements belonging to `Nat` also belongs to `Int`. In this case, `Nat` is called a subsort of `Int`, and `Int` is called a supersort of `Nat`. A sort cannot be a subsort of itself.

A partial order over sets of sorts is declared with the keyword `<` as follows:

`[ `<subsort-name>` < `<supersort-name>` ]`

Example:

`[ NzInt < Int ]`

Sort `NzInt` is subsort of Sort `Int`, where `NzInt` stands for the set of all integers except zero. Subsorts are often used for defining partial functions. For example, multiplication `*` should be defined for all integers, but the domain of the second argument of division `/` should be the set of non-zero integers. Those operators can be defined as follows:

```  op _*_ : Int Int -> Int
op _/_ : Int NzInt -> Int```