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

new line

parent 1af28e21
Branches
Tags
1 merge request!572numbers.v: Don't Qed Decision instances
Pipeline #106723 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 1 deletion
stdpp/numbers.v
+ 2
− 1
View file @ ffb2184e
...@@ -165,7 +165,8 @@ Module Nat. ...@@ -165,7 +165,8 @@ Module Nat.
Global Instance divide_dec : RelDecision Nat.divide. Global Instance divide_dec : RelDecision Nat.divide.
Proof. Proof.
refine (λ x y, cast_if (decide (lcm x y = y))); abstract (by rewrite Nat.divide_lcm_iff). refine (λ x y, cast_if (decide (lcm x y = y)));
abstract (by rewrite Nat.divide_lcm_iff).
Defined. Defined.
Global Instance divide_po : PartialOrder divide. Global Instance divide_po : PartialOrder divide.
Proof. Proof.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment