Commit 2021-02-19 12:23 114f8ef8

View on Github →

chore(data/buffer/parser/numeral): derive mono for numeral (#5463) Thanks to Rob Lewis, using classes, instances, and the delta_instance_handler, transferring over instances becomes very easy.

Estimated changes

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

modified def parser.numeral.char.of_fintype

modified def parser.numeral.char

modified def parser.numeral.from_one.of_fintype

modified def parser.numeral.from_one

modified def parser.numeral.of_fintype

modified def parser.numeral