CafeOBJ supports many useful built-in modules. For example, in the built-in module `NAT`

for natural numbers, Arabic numerals like `16384`

can be used instead of `s(s(...(s(0))...))`

(*).

(*) `NAT`

is useful for describing and verifying a system which uses natural numbers as a data type, however, it is not suitable for describing and verifying some property of the natural number itself.

Following built-in modules are included in CafeOBJ:

`BOOL`

: Boolean algebra`NAT`

: Natural numbers (e.g.`26`

)`INT`

: Integers (e.g.`-1`

)`RAT`

: Rational numbers (e.g.`1/3`

)`FLOAT`

: Floating numbers (e.g.`3.14159`

)`CHARACTER`

: Characters (e.g.`'A'`

)`STRING`

: Strings (e.g.`"abc"`

)`QID`

: Quoted identifiers (`'abc`

)`2TUPLE`

: 2-tuple`3TUPLE`

: 3-tuple`4TUPLE`

: 4-tuple`TRIV`

: The trivial module, which includes only the sort`Elt`

and denotes a set.

Use the `show`

command to show the detail of each built-in module:

Original Copyright © Takahiro Seino, all rights reserved.