Merge Requests · Iris

WIP: Type-level Quantifiers

actris!4 · opened Apr 06, 2020 by Jonas Kastberg
- CLOSED
- 7
updated May 06, 2020
WIP: rework of naive_solver after discussion with Robbert

stdpp!150 · opened Apr 22, 2020 by Michael Sammler
- CLOSED
- 8
updated May 01, 2020
Added strings to prelude to fix printing of strings.length

stdpp!139 · opened Apr 06, 2020 by Michael Sammler
- CLOSED
- 5
updated Apr 08, 2020
Random collection of lemmas

stdpp!130 · opened Mar 24, 2020 by Michael Sammler
- CLOSED
- 0
updated Mar 24, 2020
WIP: Some lemmas about `list_lookup_total`

stdpp!109 · opened Feb 12, 2020 by Dan Frumin
- CLOSED
- 3
updated Mar 17, 2020
Generalize (e)feed pose proof to intro patterns

stdpp!118 · opened Feb 25, 2020 by Paolo G. Giarrusso
- CLOSED
- 1
- 3
updated Mar 05, 2020
Add a weakening lemma for goals: "is_Some (<[i:=x]>m !! j)"

stdpp!119 · opened Feb 26, 2020 by Armaël Guéneau
- CLOSED
- 3
updated Feb 26, 2020
Add Countable instance for vec

stdpp!114 · opened Feb 23, 2020 by Tej Chajed
- CLOSED
- 2
updated Feb 24, 2020
when the goal is an evar, pick emp when possible

iris!139 · opened Apr 20, 2018 by Ralf Jung gen_proofmode
- CLOSED
- 2
updated Jan 31, 2020
Make fupd_proper more convenient to use (fix #284)

iris!353 · opened Jan 04, 2020 by Paolo G. Giarrusso
- CLOSED
- 1
updated Jan 04, 2020
Use `class_apply` instead of `refine` to avoid unwanted evars

iris!342 · opened Dec 12, 2019 by Maxime Dénès
- CLOSED
- 4
updated Dec 12, 2019
Adapting to Coq PR#10832: formats associated to a given interpretation not taken into account

iris!335 · opened Nov 12, 2019 by Hugo Herbelin
- CLOSED
- 7
updated Nov 13, 2019
WIP: Strong framing

iris!50 · opened Feb 18, 2017 by Robbert Krebbers T-proofmode
- CLOSED
- 31
updated Nov 01, 2019
Persistently: Get rid of mono and idemp in favor of intro

iris!102 · opened Dec 19, 2017 by Ralf Jung
- CLOSED
- 22
updated Nov 01, 2019
Semantic Invariants

iris!290 · opened Jul 12, 2019 by Simon Spies
- CLOSED
- 19
updated Nov 01, 2019
Avoid relying on `Export` bugs

lambda-rust!14 · opened Sep 10, 2019 by Maxime Dénès
- CLOSED
- 2
updated Sep 15, 2019
Avoid relying on `Export` bugs

iris!312 · opened Sep 10, 2019 by Maxime Dénès
- CLOSED
- 7
updated Sep 13, 2019
Avoid relying on `Export` bugs

stdpp!92 · opened Sep 05, 2019 by Maxime Dénès
- CLOSED
- 3
updated Sep 05, 2019
Fix direction of CONSTRUCTOR_NAME_op lemmas (fix #256)

iris!295 · opened Jul 22, 2019 by Paolo G. Giarrusso
- CLOSED
- 20
updated Aug 13, 2019
introduce notation for value comparison

iris!279 · opened Jun 21, 2019 by Ralf Jung Iris 3.2
- CLOSED
- 8
updated Jun 29, 2019