mathlib
f737ca11
- feat(data/option/basic): add `bind_some'` (#16641)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(data/option/basic): add `bind_some'` (#16641) We already have `some_bind` `bind_some` `some_bind'`, but there is no `bind_some'`.
Author
astrainfinita
Parents
94fc87ee
Loading