(Created page with "Freetypes exist in Z and in the Rodin theory plugin and are supported by ProB. You can also define new freetypes in classical B by adding a FREETYPES clause with equations separated by semicolon. Here is a definition of an inductive type IntList for lists of integers constructed using inil and icons: <pre> FREETYPES IntList = inil, icons(INTEGER*IntList) </pre>") |
No edit summary |
||
| Line 1: | Line 1: | ||
=== Summary === | |||
You can also define new | Free types exist in Z and in the Rodin theory plugin and are supported by ProB. | ||
with | You can also define new free types in classical B by adding a ''FREETYPES'' clause with free type definitions separated by semicolon. | ||
Here is a definition of an inductive type IntList for lists of | |||
integers constructed using inil and icons: | Here is a definition of an inductive type ''IntList'' for lists of integers constructed using ''inil'' and ''icons'': | ||
<pre> | <pre> | ||
FREETYPES | FREETYPES | ||
IntList = inil, icons(INTEGER*IntList) | IntList = inil, icons(INTEGER*IntList) | ||
</pre> | </pre> | ||
=== What is a Free Type === | |||
Free types exist in Z and in the Rodin theory plugin and are supported by ProB. You can also define new free types in classical B by adding a FREETYPES clause with free type definitions separated by semicolon.
Here is a definition of an inductive type IntList for lists of integers constructed using inil and icons:
FREETYPES IntList = inil, icons(INTEGER*IntList)