theories/algebra · 7363e2ccc1c19196e46755349e169ded7cf3fdf9 · Paolo G. Giarrusso / iris

Forked from Iris / Iris

2917 commits behind the upstream repository.

`list_lookup_singletonM_ne` is not sufficient when we need to
compare a singleton with another list, for example, to see if one
is included in the other.

7363e2cc

History

7363e2cc 5 years ago

History

Name	Last commit	Last update
..
lib
agree.v
auth.v
base.v
big_op.v
cmra.v
cmra_big_op.v
coPset.v
cofe_solver.v
csum.v
deprecated.v
dra.v
excl.v
frac.v
functions.v
gmap.v
gmultiset.v
gset.v
list.v
local_updates.v
monoid.v
namespace_map.v
ofe.v
proofmode_classes.v
sts.v
ufrac.v
updates.v
vector.v