Commit c02c0693 authored by Robbert Krebbers's avatar Robbert Krebbers

Notation for max and min.

parent c24ab2ee
......@@ -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