From 114f8ef87582bfc98aaad2acb211aa8c0b547964 Mon Sep 17 00:00:00 2001
From: Yakov Pechersky <ffxen158@gmail.com>
Date: Fri, 19 Feb 2021 12:23:01 +0000
Subject: [PATCH] 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.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
---
 src/data/buffer/parser/numeral.lean | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/data/buffer/parser/numeral.lean b/src/data/buffer/parser/numeral.lean
index ab7b0a4ea1ecc..0e8bd460a16f4 100644
--- a/src/data/buffer/parser/numeral.lean
+++ b/src/data/buffer/parser/numeral.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 -/
 import data.fintype.card
+import data.buffer.parser.basic
 
 /-!
 # Numeral parsers
@@ -43,7 +44,7 @@ variables (α : Type) [has_zero α] [has_one α] [has_add α]
 /--
 Parse a string of digits as a numeral while casting it to target type `α`.
 -/
-def numeral : parser α :=
+@[derive mono] def numeral : parser α :=
 nat.bin_cast <$> nat
 
 /--
@@ -51,7 +52,7 @@ Parse a string of digits as a numeral while casting it to target type `α`,
 which has a `[fintype α]` constraint. The parser ensures that the numeral parsed in
 is within the cardinality of the type `α`.
 -/
-def numeral.of_fintype [fintype α] : parser α :=
+@[derive mono] def numeral.of_fintype [fintype α] : parser α :=
 do
   c ← nat,
   decorate_error (sformat!"<numeral less than {to_string (fintype.card α)}>")
@@ -62,7 +63,7 @@ do
 Parse a string of digits as a numeral while casting it to target type `α`. The parsing starts
 at "1", so `"1"` is parsed in as `nat.cast 0`. Providing `"0"` to the parser causes a failure.
 -/
-def numeral.from_one : parser α :=
+@[derive mono] def numeral.from_one : parser α :=
 do
   c ← nat,
   decorate_error ("<positive numeral>")
@@ -75,7 +76,7 @@ which has a `[fintype α]` constraint. The parser ensures that the numeral parse
 is within the cardinality of the type `α`. The parsing starts
 at "1", so `"1"` is parsed in as `nat.cast 0`. Providing `"0"` to the parser causes a failure.
 -/
-def numeral.from_one.of_fintype [fintype α] : parser α :=
+@[derive mono] def numeral.from_one.of_fintype [fintype α] : parser α :=
 do
   c ← nat,
   decorate_error (sformat!"<positive numeral less than or equal to {to_string (fintype.card α)}>")
@@ -87,7 +88,7 @@ Parse a character as a numeral while casting it to target type `α`,
 The parser ensures that the character parsed in is within the bounds set by `fromc` and `toc`,
 and subtracts the value of `fromc` from the parsed in character.
 -/
-def numeral.char (fromc toc : char) : parser α :=
+@[derive mono] def numeral.char (fromc toc : char) : parser α :=
 do
   c ← decorate_error
     (sformat!"<char between '{fromc.to_string}' to '{toc.to_string}' inclusively>")
@@ -101,7 +102,7 @@ The parser ensures that the character parsed in is greater or equal to `fromc` a
 and subtracts the value of `fromc` from the parsed in character. There is also a check
 that the resulting value is within the cardinality of the type `α`.
 -/
-def numeral.char.of_fintype [fintype α] (fromc : char) : parser α :=
+@[derive mono] def numeral.char.of_fintype [fintype α] (fromc : char) : parser α :=
 do
   c ← decorate_error
     (sformat!"<char from '{fromc.to_string}' to '{