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

Same for `Qp`.

parent 82068f29
No related branches found
No related tags found
No related merge requests found
......@@ -298,7 +298,7 @@ Global Program Instance Qp_countable : Countable Qp :=
(λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
Next Obligation.
intros [p Hp]. unfold mguard, option_guard; simpl.
case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
case_match; [|done]. f_equal. by apply Qp.to_Qc_inj_iff.
Qed.
Global Program Instance fin_countable n : Countable (fin n) :=
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment