Free Types

Revision as of 12:11, 22 April 2024 by Vella (talk | contribs) (Vella moved page Freetypes to Free Types)

Summary

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)

What is a Free Type