Built-in modules

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:

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


Original Copyright © Takahiro Seino, all rights reserved.