Commit 02e61349 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'countable_sig' into 'master'

add Countable instance for decidable Sigma types

See merge request !255
parents f7c9c556 1fb8aa47
Pipeline #46248 passed with stage
in 9 minutes and 43 seconds
......@@ -340,3 +340,12 @@ Next Obligation.
intros T ?? t.
by rewrite <-(right_id_L [] _ (gen_tree_to_list _)), gen_tree_of_to_list.
Qed.
(** ** Sigma *)
Program Instance countable_sig `{Countable A} (P : A Prop)
`{! x, Decision (P x), ! x, ProofIrrel (P x)} :
Countable { x : A | P x } :=
inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x Hx)) _.
Next Obligation.
intros A ?? P ?? [x Hx]. by erewrite (option_guard_True_pi (P x)).
Qed.
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