theories · 9b0f7c75a2387e0ad9fe5d16ec1083a0ece2bea3 · Maxime Dénès / stdpp · GitLab

Snippets Groups Projects

Forked from Iris / stdpp

2267 commits behind the upstream repository.

Put `Dom` as first argument of `FinMapDom`.

Robbert Krebbers authored 7 years ago

This way, type class search will fail immediately on first type
class constraint of any of the `fin_map_dom` lemmas if no `Dom`
can be found.

9b0f7c75

9b0f7c75 7 years ago

Name	Last commit	Last update
..
base.v
bset.v
coPset.v
collections.v
countable.v
decidable.v
fin.v
fin_collections.v
fin_map_dom.v
fin_maps.v
finite.v
functions.v
gmap.v
gmultiset.v
hashset.v
hlist.v
lexico.v
list.v
listset.v
listset_nodup.v
mapset.v
natmap.v
nmap.v
numbers.v
option.v
orders.v
pmap.v
prelude.v
pretty.v
proof_irrel.v
relations.v
set.v
sorting.v
streams.v
stringmap.v
strings.v
tactics.v
vector.v
zmap.v