Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Marianna Rapoport
iris-coq
Commits
d9bae949
Commit
d9bae949
authored
Nov 17, 2015
by
Robbert Krebbers
Browse files
Inhabited now lives in Type rather than Prop.
parent
5651f58e
Changes
2
Hide whitespace changes
Inline
Side-by-side
prelude/base.v
View file @
d9bae949
...
...
@@ -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
().
...
...
prelude/finite.v
View file @
d9bae949
...
...
@@ -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
)
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment