Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-19 17:22 da6e3c36

View on Github →

feat(data/buffer/parser/numeral): numeral parser defs (#5462)

Estimated changes

Created src/data/buffer/parser/numeral.lean

added def parser.numeral.char.of_fintype

added def parser.numeral.char

added def parser.numeral.from_one.of_fintype

added def parser.numeral.from_one

added def parser.numeral.of_fintype

added def parser.numeral