Merge Requests · Iris

Add more lemmas for gmap uncurry

stdpp!9 · opened Oct 20, 2017 by Hai Dang
- MERGED
- 9
updated Oct 27, 2017
Add more properties of intersection_with for fin_maps

stdpp!7 · opened Oct 06, 2017 by Hai Dang
- MERGED
- 1
updated Oct 27, 2017
Add lemma lookup_gmap_uncurry_empty

stdpp!8 · opened Oct 13, 2017 by Jacques-Henri Jourdan
- MERGED
- 4
updated Oct 17, 2017
Introduce a connective `ilocked` to stop `iNext` and `iFrame`. 3 of 3 tasks completed

iris!67 · opened Sep 28, 2017 by Robbert
- MERGED
- 23
updated Oct 10, 2017
use primitive projections for our mixins

iris!69 · opened Oct 10, 2017 by Ralf Jung
- MERGED
- 9
updated Oct 10, 2017
Remove an unused argument for `newcounter_mono_spec`.

iris!70 · opened Oct 10, 2017 by Dan Frumin
- MERGED
- 1
updated Oct 10, 2017
update stdpp

iris!68 · opened Oct 05, 2017 by Hai Dang
- MERGED
- 1
updated Oct 05, 2017
Add CI and update build system

gpfsl!1 · opened Sep 28, 2017 by Ralf Jung
- MERGED
- 0
updated Sep 28, 2017
Use `ε` for CMRA unit

iris!62 · opened Sep 17, 2017 by Robbert
- MERGED
- 10
updated Sep 25, 2017
Fix typo in is_lock_proper for heap_lang.

iris!57 · opened Jul 14, 2017 by Joshua Yanovski
- MERGED
- 5
updated Sep 15, 2017
Implement greatest fixed point inside the logic

iris!60 · opened Aug 22, 2017 by Ralf Jung
- MERGED
- 19
updated Aug 31, 2017
get rid of the empty-unicode-space hacks

iris!59 · opened Aug 22, 2017 by Ralf Jung
- MERGED
- 2
updated Aug 24, 2017
Refactor the resources for ticket lock

iris!55 · opened Mar 24, 2017 by Jeehoon Kang
- MERGED
- 2
updated Aug 23, 2017
Add countability for Q, Qc, and Qp

stdpp!4 · opened Jul 05, 2017 by Hai Dang
- MERGED
- 3
updated Aug 05, 2017
Some map_zip/map_zip_with properties.

stdpp!3 · opened May 29, 2017 by Dan Frumin
- MERGED
- 7
updated Jun 26, 2017
Generic big operators that are computational for lists

iris!54 · opened Mar 21, 2017 by Robbert
- MERGED
- 13
updated Mar 24, 2017
Updating the ProofMode.md docs

iris!53 · opened Mar 16, 2017 by Dan Frumin
- MERGED
- 3
updated Mar 16, 2017
Define `fill` in terms of a `foldl` over `fill_item`.

iris!52 · opened Mar 13, 2017 by Robbert
- MERGED
- 1
updated Mar 14, 2017
Done, auto frame, and persistent frame specialization patterns

iris!51 · opened Mar 08, 2017 by Robbert
- MERGED
- 3
updated Mar 14, 2017
Make [ELCtx_Alive] a coercion

lambda-rust!6 · opened Mar 05, 2017 by Jacques-Henri Jourdan
- MERGED
- 5
updated Mar 06, 2017