Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-13 23:08 2967fae8

View on Github →

refactor(data/option/defs): Swap arguments to option.elim (#14681) Make option.elim a non-dependent version of option.rec rather than a non-dependent version of option.rec_on. Same for option.melim. This replaces option.cons, and brings option.elim in line with nat.elim, sum.elim, and iff.elim. It addresses the TODO comment added in 22c4291217925c6957c0f5a44551c9917b56c7cf.

Estimated changes

Modified src/algebra/big_operators/option.lean

Modified src/analysis/box_integral/partition/basic.lean

Modified src/analysis/calculus/lagrange_multipliers.lean

Modified src/category_theory/category/PartialFun.lean

modified def Pointed_to_PartialFun

Modified src/computability/tm_to_partrec.lean

Modified src/data/finset/basic.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/data/option/basic.lean

deleted def option.cons

deleted theorem option.cons_none_some

added theorem option.elim_none_some

Modified src/data/option/defs.lean

modified def option.melim

Modified src/logic/embedding.lean

Modified src/measure_theory/measure/outer_measure.lean

Modified src/number_theory/dioph.lean

Modified src/tactic/linarith/frontend.lean

Modified src/topology/paracompact.lean