Mathlib v3 is deprecated. Go to Mathlib v4

Def parser.numeral.from_one.of_fintype

Modification history

2021-03-16 19:18
src/data/buffer/parser/numeral.lean
feat(data/buffer/parser/*): expand parser properties (#6339) …
Modified parser.numeral.from_one.of_fintypeView on Github →
2021-02-19 12:23
src/data/buffer/parser/numeral.lean
chore(data/buffer/parser/numeral): derive mono for numeral (#5463) …
Modified parser.numeral.from_one.of_fintypeView on Github →
2021-01-19 17:22
src/data/buffer/parser/numeral.lean
feat(data/buffer/parser/numeral): numeral parser defs (#5462)
Added parser.numeral.from_one.of_fintypeView on Github →