mathlib3
43514e1e - feat(data/option/n_ary): Binary map of options (#16763)

Commit
3 years ago
feat(data/option/n_ary): Binary map of options (#16763) Define `option.mapâ‚‚`, the binary map of options.
Author
Parents
Loading