Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-07-21 12:10 e7321bbd

View on Github →

fix(data/option): fix universe levels in option.map_some etc.

Estimated changes

modified theorem option.bind_eq_some
modified theorem option.map_eq_some
modified theorem option.map_none
modified theorem option.map_some
modified theorem option.none_bind
modified inductive option.rel
modified theorem option.seq_some
modified theorem option.some_bind