Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-29 14:16 fd4628f1

View on Github →

chore(*): bump to lean 3.19.0c, fin is now a subtype (#3955)

  • Some decidable.* order theorems have been moved to core.
  • fin is now a subtype. This means that the whnf of fin n is now {i // i < n}. Also, the coercion fin n → nat is now preferred over subtype.val. The entire library has been refactored accordingly. (Although I probably missed some cases.)
  • in_current_file' was removed since the bug in in_current_file was fixed in core.
  • The syntax of guard_hyp in core was changed from guard_hyp h := t to guard_hyp h : t, so the syntax for the related guard_hyp', match_hyp and guard_hyp_strict tactics in tactic.interactive was changed as well.

Estimated changes

deleted theorem decidable.eq_or_lt_of_le
deleted theorem decidable.le_iff_lt_or_eq
deleted theorem decidable.le_of_not_lt
deleted theorem decidable.le_or_lt
deleted theorem decidable.lt_or_eq_of_le
deleted theorem decidable.lt_or_gt_of_ne
deleted theorem decidable.lt_or_le
deleted theorem decidable.lt_trichotomy
deleted theorem decidable.ne_iff_lt_or_gt
deleted theorem decidable.not_lt
deleted theorem not_le
deleted theorem not_lt
modified theorem primrec.fin_val
modified theorem array.write_to_list
modified theorem bitvec.to_fin_val
deleted theorem fin.add_nat_val
deleted theorem fin.cast_add_val
deleted theorem fin.cast_le_val
modified theorem fin.cast_lt_cast_succ
deleted theorem fin.cast_lt_val
modified theorem fin.cast_succ_cast_lt
modified theorem fin.cast_succ_lt_last
deleted theorem fin.cast_succ_val
deleted theorem fin.cast_val
modified def fin.clamp
deleted theorem fin.clamp_val
added theorem fin.coe_add
added theorem fin.coe_add_nat
added theorem fin.coe_cast
added theorem fin.coe_cast_add
added theorem fin.coe_cast_le
added theorem fin.coe_cast_lt
added theorem fin.coe_cast_succ
added theorem fin.coe_clamp
added theorem fin.coe_injective
added theorem fin.coe_mul
added theorem fin.coe_of_nat_eq_mod'
added theorem fin.coe_of_nat_eq_mod
added theorem fin.coe_one'
added theorem fin.coe_pred
added theorem fin.coe_sub_nat
added theorem fin.coe_succ
modified theorem fin.coe_val_eq_self
modified theorem fin.eq_last_of_not_lt
added theorem fin.ext
added theorem fin.ext_iff
added theorem fin.is_lt
modified theorem fin.last_val
added theorem fin.le_iff_coe_le_coe
deleted theorem fin.le_iff_val_le_val
added theorem fin.lt_iff_coe_lt_coe
deleted theorem fin.lt_iff_val_lt_val
added theorem fin.mk_coe
modified theorem fin.mk_one
modified theorem fin.mk_zero
deleted theorem fin.pred_val
modified def fin.sub_nat
deleted theorem fin.sub_nat_val
modified theorem fin.succ_pos
deleted theorem fin.succ_val
added theorem fin.val_eq_coe
deleted theorem fin.val_injective
deleted theorem fin.val_of_nat_eq_mod'
deleted theorem fin.val_of_nat_eq_mod
modified theorem list.of_fn_nth_le