Commit 2023-02-20 17:21 200a85b2

View on Github →

fix: add some missing type annotations and attrs (#2391)

  • Fix WithBot.le_coe_iff and WithTop.coe_le_iff.
  • Mark WithBot.some and WithTop.some as @[match_pattern].
  • Mark WithBot.coe_eq_coe, WithBot.coe_min, WithBot.coe_max, and WithTop.coe_eq_coe as @[simp]. Lean 3 used applied with_top/with_bot/option lemmas about coe to all three types; now we need to restate them.

Estimated changes

modified theorem WithBot.coe_eq_coe
modified theorem WithBot.le_coe_iff
modified def WithBot.some
modified theorem WithTop.coe_le_iff
modified theorem WithTop.coe_lt_top
modified def WithTop.some