basic): use `option.elim` and `sum.elim` (#12724)

Commit

3 years ago

chore(data/equiv/basic): use `option.elim` and `sum.elim` (#12724) We have these functions, why not use them?

Author

urkud

Parents