Skip to content
Snippets Groups Projects
Commit 59c3f672 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

`Add Printing Constructor` for `max_nat` and `min_nat`.

parent 442de845
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/algebra/numbers.v
+ 2
− 0
View file @ 59c3f672
...@@ -46,6 +46,7 @@ End nat. ...@@ -46,6 +46,7 @@ End nat.
(** ** Natural numbers with [max] as the operation. *) (** ** Natural numbers with [max] as the operation. *)
Record max_nat := MaxNat { max_nat_car : nat }. Record max_nat := MaxNat { max_nat_car : nat }.
Add Printing Constructor max_nat.
Canonical Structure max_natO := leibnizO max_nat. Canonical Structure max_natO := leibnizO max_nat.
...@@ -101,6 +102,7 @@ End max_nat. ...@@ -101,6 +102,7 @@ End max_nat.
(** ** Natural numbers with [min] as the operation. *) (** ** Natural numbers with [min] as the operation. *)
Record min_nat := MinNat { min_nat_car : nat }. Record min_nat := MinNat { min_nat_car : nat }.
Add Printing Constructor min_nat.
Canonical Structure min_natO := leibnizO min_nat. Canonical Structure min_natO := leibnizO min_nat.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment