Branches · Yixuan Chen / Iris · GitLab

Snippets Groups Projects

master default protected

5ae02407 · update dependencies · 1 year ago
iris/iris!1025
Download source code

zip
tar.gz
tar.bz2
tar
robbert/cmra_valid_elim

1f318399 · CHANGELOG. · 2 years ago

577

2
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/separable

6cca1517 · shorter proof · 2 years ago

664

2
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/mono_Z

ec688df0 · Update comments. · 2 years ago

622

4
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/Z

1e37031b · get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays · 2 years ago

663

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/bi-persistently-emp

1a072a4c · get everything else to build again · 2 years ago

664

3
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/mono_Z

56108f54 · add mono_Z base-logic library · 2 years ago

664

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ci/robbert/big_op_binder

0721fd0d · Document FIXME. · 2 years ago

711

0
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/no_native_compute

93d9ef74 · Avoid relying on native_compute. · 2 years ago

723

0
Download source code

zip
tar.gz
tar.bz2
tar
Compare
simon/parametric-index

64cd40ba · Merge branch 'master' into simon/parametric-index · 2 years ago

741

44
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ci/robbert/set_solver_eauto

336404e0 · update to std++ snapshot · 2 years ago

741

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/make

297edd7f · add QuickPersistent, QuickIntuitionistic classes · 2 years ago

769

2
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ci/msammler/nb_state

4a4b3d53 · Allow specifing states that are allowed to be stuck · 2 years ago

811

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/add_sub

e1f9c08b · Port to std++. · 2 years ago

811

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ci/general-contractive

70df718a · generalize definition of contractiveness · 2 years ago

857

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
ralf/has-lc

cdfa27c0 · track has_lc directly in invGS/irisGS/heapGS rather than via separate typeclass · 2 years ago

884

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/has_lc_if

1fe85887 · Add class `HasLcIf` so that it becomes easier to write generic adequacy lemmas. · 2 years ago

899

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/bi_cofe

00d2fb63 · Ensure that different `Cofe` proofs of `iProp` are convertible. · 3 years ago

997

0
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/bi_wand_notation

1859ff61 · Add ∗-∗ as notation in stdpp_scope similar to -∗. · 3 years ago

999+

1
Download source code

zip
tar.gz
tar.bz2
tar
Compare
robbert/level

9418cdd3 · Use priority levels for `iFrame`. There's no syntax yet, so the fixes to the... · 3 years ago

999+

2
Download source code

zip
tar.gz
tar.bz2
tar
Compare

Prev
1
2
3
4
5
Next