Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-09-25 10:07
2313602e
View on Github →
feat(order/bounded_lattice): custom recursors for with_bot/with_top (
#4245
)
Estimated changes
Modified
src/order/bounded_lattice.lean
added
def
with_bot.rec_bot_coe
added
def
with_top.rec_top_coe