Commit 0f273374 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for max and min.

parent f70dd438
......@@ -791,8 +791,8 @@ Section mnat.
Instance mnat_valid : Valid mnat := λ x, True.
Instance mnat_validN : ValidN mnat := λ n x, True.
Instance mnat_pcore : PCore mnat := Some.
Instance mnat_op : Op mnat := max.
Definition mnat_op_max x y : x y = max x y := eq_refl.
Instance mnat_op : Op mnat := Nat.max.
Definition mnat_op_max x y : x y = x `max` y := eq_refl.
Lemma mnat_included (x y : mnat) : x y x y.
Proof.
split.
......
......@@ -32,6 +32,8 @@ Notation "(<)" := lt (only parsing) : nat_scope.
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
Infix "`max`" := Nat.max (at level 35) : nat_scope.
Infix "`min`" := Nat.min (at level 35) : nat_scope.
Instance nat_eq_dec: x y : nat, Decision (x = y) := eq_nat_dec.
Instance nat_le_dec: x y : nat, Decision (x y) := le_dec.
......
Markdown is supported
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