Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-02 16:24 3e9e4b68

View on Github →

refactor(*): move theorems and do minor polishing

Estimated changes

Modified data/bool.lean

Modified data/list/basic.lean

modified theorem list.concat_cons

Modified data/list/sort.lean

deleted theorem nat.add_pos_iff_pos_or_pos

deleted theorem nat.add_pos_left

deleted theorem nat.add_pos_right

deleted theorem nat.lt_succ_iff_le

deleted theorem nat.succ_le_succ_iff

Modified data/nat/basic.lean

added theorem nat.add_pos_iff_pos_or_pos

added theorem nat.add_pos_left

added theorem nat.add_pos_right

added theorem nat.lt_succ_iff_le

added theorem nat.succ_le_succ_iff

Modified logic/basic.lean

added theorem and_implies_iff

added theorem bexists_def

added theorem iff_def

added theorem implies_and_iff

Modified tactic/finish.lean

deleted theorem curry_iff

deleted theorem iff_def

deleted theorem implies_and_iff

deleted theorem {u}