Commit f13fcc91 authored by Robbert Krebbers's avatar Robbert Krebbers

Inhabited now lives in Type rather than Prop.

parent 44722ee1
......@@ -129,7 +129,7 @@ Arguments decide _ {_}.
(** ** Inhabited types *)
(** This type class collects types that are inhabited. *)
Class Inhabited (A : Type) : Prop := populate { _ : A }.
Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
Arguments populate {_} _.
Instance unit_inhabited: Inhabited unit := populate ().
......
......@@ -69,7 +69,7 @@ Proof.
Qed.
Lemma finite_inhabited A `{finA: Finite A} : 0 < card A Inhabited A.
Proof.
unfold card. destruct finA as [[|x ?] ??]; simpl; auto with lia.
unfold card; intros. destruct finA as [[|x ?] ??]; simpl in *; [exfalso;lia|].
constructor; exact x.
Qed.
Lemma finite_injective_contains `{finA: Finite A} `{finB: Finite B} (f: A B)
......
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