Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Tej Chajed
stdpp
Commits
a05d1085
Commit
a05d1085
authored
Jun 29, 2018
by
Janno
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add `Countable` instance for `mapset`.
parent
25bdb78f
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
4 additions
and
1 deletion
+4
-1
theories/mapset.v
theories/mapset.v
+4
-1
No files found.
theories/mapset.v
View file @
a05d1085
...
...
@@ -3,7 +3,7 @@
(** This files gives an implementation of finite sets using finite maps with
elements of the unit type. Since maps enjoy extensional equality, the
constructed finite sets do so as well. *)
From
stdpp
Require
Export
fin_map_dom
.
From
stdpp
Require
Export
countable
fin_map_dom
.
(* FIXME: This file needs a 'Proof Using' hint. *)
Record
mapset
(
M
:
Type
→
Type
)
:
Type
:
=
...
...
@@ -76,6 +76,9 @@ Section deciders.
match
X1
,
X2
with
Mapset
m1
,
Mapset
m2
=>
cast_if
(
decide
(
m1
=
m2
))
end
)
;
abstract
congruence
.
Defined
.
Program
Instance
mapset_countable
`
{
Countable
(
M
())}
:
Countable
(
mapset
M
)
:
=
inj_countable
mapset_car
(
Some
∘
Mapset
)
_
.
Next
Obligation
.
by
intros
?
?
[].
Qed
.
Global
Instance
mapset_equiv_dec
:
RelDecision
(
≡
@{
mapset
M
})
|
1
.
Proof
.
refine
(
λ
X1
X2
,
cast_if
(
decide
(
X1
=
X2
)))
;
abstract
(
by
fold_leibniz
).
Defined
.
Global
Instance
mapset_elem_of_dec
:
RelDecision
(
∈
@{
mapset
M
})
|
1
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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