Commit 2022-01-17 11:03 c4c15e05

View on Github →

chore: bump to nightly-2022-01-17 (#160)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/BinaryHeap.lean

Modified Mathlib/Data/ByteArray.lean

Deleted Mathlib/Init/WF.lean

Created Mathlib/Logic/Nonempty.lean

added theorem Classical.nonempty_pi

added theorem Nonempty.elim_to_inhabited

added theorem Nonempty.exists

added theorem Nonempty.forall

added theorem Nonempty.map

added theorem exists_true_iff_nonempty

added theorem nonempty_Prop

added theorem nonempty_empty

added theorem nonempty_plift

added theorem nonempty_pprod

added theorem nonempty_prod

added theorem nonempty_psigma

added theorem nonempty_psum

added theorem nonempty_sigma

added theorem nonempty_subtype

added theorem nonempty_sum

added theorem nonempty_ulift

added theorem not_nonempty_iff_imp_false

added theorem subsingleton_of_not_nonempty

Modified Mathlib/Tactic/Cache.lean

Modified Mathlib/Tactic/Ext.lean

Modified Mathlib/Tactic/NormCast.lean

Modified Mathlib/Util/Export.lean

modified def Lean.Export.runExportM

Modified Mathlib/Util/TermUnsafe.lean

Modified lean-toolchain

Modified test/irreducibleDef.lean