Mathlib v3 is deprecated. Go to Mathlib v4

Theorem option.get_or_else_coe

Modification history

2020-10-26 05:21
src/data/option/basic.lean
chore(order/galois_connection): define `with_bot.gi_get_or_else_bot` (#4781) …
Added option.get_or_else_coeView on Github →