1.2.0

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 ≥

1.1.0

add classical logic (#14)

1.0.0

fix library name and repo (#11)

0.0.0

First release.