Merge Requests · Iris

Add `head_prim_fill_reducible_no_obs`

iris!306 · opened Aug 22, 2019 by Dan Frumin
- MERGED
- 1
- 4
updated Aug 24, 2019
Lemmas for big ops commuting with updates

iris!305 · opened Aug 22, 2019 by Robbert Krebbers
- MERGED
- 1
- 9
updated Aug 24, 2019
comparison: treat prophecies like unit and make all closures equal

iris!270 · opened Jun 14, 2019 by Ralf Jung
- MERGED
- 1
- 17
updated Nov 24, 2020
Turn the arguments of functors into COFEs + write some docs

iris!257 · opened May 30, 2019 by Robbert Krebbers
- MERGED
- 1
- 37
updated Apr 01, 2020
Additionally lemmas for insert, nth, take, and list_find

stdpp!55 · opened Feb 08, 2019 by Hai Dang
- MERGED
- 1
- 15
updated Feb 21, 2019
Lemmas about subst_map on closed expressions

iris!194 · opened Dec 20, 2018 by Dan Frumin
- MERGED
- 1
- 6
updated Dec 21, 2018
Derive löb induction from later introduction and guarded fixpoints

iris!145 · opened May 03, 2018 by Ralf Jung gen_proofmode
- MERGED
- 1
- 13
updated May 08, 2018
Repair the plainly modality

iris!122 · opened Feb 23, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 1
- 32
updated Feb 26, 2018
Use symbol ∗ for separating conjunction.

iris!21 · opened Nov 01, 2016 by Robbert Krebbers
- MERGED
- 1
- 11
updated Nov 03, 2016
coPset: some lemmas about infinity

stdpp!230 · opened Mar 05, 2021 by Ralf Jung
- MERGED
- 3
updated Mar 05, 2021
Fix typos

iris!644 · opened Mar 03, 2021 by Yusuke Matsushita
- MERGED
- 6
updated Mar 03, 2021
Error improvements

refinedc!49 · opened Mar 02, 2021 by Michael Sammler
- MERGED
- 0
updated Mar 02, 2021
semantics and typing rule for NotIntOp

refinedc!48 · opened Mar 02, 2021 by Fengmin Zhu
- MERGED
- 5
updated Mar 04, 2021
prove model for own_ptr

lambda-rust!18 · opened Mar 01, 2021 by Xavier Denis rusthornbelt
- MERGED
- 3
updated Mar 02, 2021
avoid relying on rewrite's implicit revert

iris!643 · opened Mar 01, 2021 by Ralf Jung
- MERGED
- 1
updated Mar 01, 2021
Cleaning up around [lang.v]

refinedc!47 · opened Feb 26, 2021 by Rodolphe Lepigre
- MERGED
- 0
updated Mar 02, 2021
Tactic based on lia and autorewrite to solve location equality

refinedc!46 · opened Feb 22, 2021 by Rodolphe Lepigre
- MERGED
- 15
updated Feb 24, 2021
Find hypothesis by semantic equality

refinedc!45 · opened Feb 22, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 23, 2021
move normalize_and_simpl_goal to the beginning of unprepared_solve_goal

refinedc!44 · opened Feb 22, 2021 by Michael Sammler
- MERGED
- 0
updated Feb 22, 2021
Finished [early_alloc.c].

refinedc!43 · opened Feb 19, 2021 by Rodolphe Lepigre
- MERGED
- Approved
- 10
updated Feb 22, 2021