theories/algebra · ea353e5f79aa49ea8204064080043a11dceaee8e · Simcha van Collem / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

5190 commits behind the upstream repository.

Have dist_later not depend on an ofeT, but on an unbundled Dist.

Robbert Krebbers authored 7 years ago

That way, we can use Contractive as part of structure definitions in
which we do not have a bundled OFE yet.

ea353e5f

ea353e5f 7 years ago

Name	Last commit	Last update
..
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
frac_auth.v
gmap.v
gset.v
iprod.v
list.v
local_updates.v
monoid.v
ofe.v
sts.v
updates.v
vector.v