12:0212:02, 22 April 2024diffhist+365 N
Free TypesCreated 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>"
