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 ]
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
Original Copyright © Takahiro Seino, all rights reserved.