Recent changes

• LEGO now supports small impredicative -types.
• The syntax for records has changed.

• 16 February 1995 Bernhard Reus & Thomas Schreiber

  LEGO now supports small impredicative -types. To enable the alternative formation rule for small -types

  ,

  you need to initialise either

  • Init XCC_s where definitions are treated as -rules, or
  • Init XCC'_s where definitions are treated as macros.

  For a discussion on -types and existential types, see pages 41 - 43 in Computation and Reasoning. See pages 32 - 33 in Computation and Reasoning for more information about predicative universes and the reflection principle.

• 16 February 1995 Thomas Schreiber

  The syntax for Records has changed, Constructors are now called Fields e.g.,

  Record [person:Type] Fields [age:nat] [town:string]; will generate a new type person : Type(person) with a single constructor make_person : nat->string->person and the corresponding Martin Löf elimination and computation rules. Furthermore, LEGO derives the projections
  • age : person->nat
  • town : person->string.