Types

Alt-Ergo has built-in support for a number of built-in types, associated with theories for which it has decision procedures. It also natively supports prenex polymorphism.

This may be used to create used-defined types, through abstract types, algebraic datatypes, enums and records.

• Built-in types
  • Boolean types
  • Numeric types
  • Unit type
  • Bitvectors
  • Type variables
  • Polymorphic functional arrays
• Built-in operators
  • Logical operators
    • The bool/prop conflict
    • Examples
  • Numeric operators
  • Comparisons
  • Additional numeric primitives
    • Conversion between integers and reals
    • Square root
    • Internal primitives
  • Bitvectors
    • Examples
  • Type variables
  • Polymorphic functional arrays
    • Syntax
    • Examples
• User-defined
  • Abstract types
    • Syntax
    • Examples
  • Records
    • Syntax
    • Examples
  • Enums and Algebraic datatypes
    • Examples
    • Syntax