All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
- Conj: theorems for structural operations on the level of nary conjunctions
- Disj: theorems for structural operations on the level of nary disjunctions
- List: ⊆, rem_nth, undup_first, and related theorems
- definition of Pos.mul
- declare theorems as opaque symbols
- FunExt: axiom for functional extensionality
- PropExt: axiom for propositional extensionality and related theorems
- Prod: Cartesian product (extracted from Set)
- Option: polymorphic option type
- String: builtin string type
- Tactic: tactic type for the eval tactic
- Comp: isLe and isGe
- List: mem_tail, nths and related properties
- Bool: istrue=true
- Set: moved Cartesian product to separate Prod file, pairing constructor renamed as "‚"
- 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
- 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
- Z: missing notation for ≥
- Classic: classical logic
- Prop: rename top into ⊤ᵢ
- FOL: declare more arguments of ∃ᵢ and ∃ₑ implicit
- Z: integers (Quentin Garchery)
- Nat, List: natural numbers and lists (Quentin Buzet)