not compatible with lambdapi < 2.6.0
Added
- HOL: Set constructor ⤳ for quantifying over function types
- Impred: Set constructor o for quantifying over propositions
- Epsilon: Hilbert's ε operator
- List: add iota and indexes
- Set: add ι:Set and an axiom el:Π a,τ a saying that every set is non-empty
- Pos, Z: add printing to decimal notation
Changed
- Z: rename × into *, and ~ into —
- Z: add parsing from decimal notation
- Nat: rename 0 into _0, and -1 into ∸1
- Bool: declare istrue as injective
Fixed
- Z: missing notation for ≥