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