mathlib3

62a613fa - feat(data/option): add `option.mmap` and `option.maybe` (#2484)

feat(data/option): add `option.mmap` and `option.maybe` (#2484) Please let me know if something like this exists already! Over the last few days I've wanted it multiple times, and it is used in #2485. <br> <br> <br>