A sort is a set of classified elements.
Sorts are declared between
] 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
[ Node Edge ]
A partial order over sets of sorts can be defined. For example, consider Sorts
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 is called a supersort of
A sort cannot be a subsort of itself.
A partial order over sets of sorts is declared with the keyword
< as follows:
[ NzInt < Int ]
NzInt is subsort of Sort
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.