Markus de Medeiros

[Heap.lean](https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/Std/Heap.lean) contains a general interface for heap and map types. Instantiate this for the Heap types in the Lean standard library (eg. [ExtTreeMap](https://leanprover-community.github.io/mathlib4_docs/Std/Data/ExtTreeMap/Lemmas.html)).

Better syntax for pm_terms

1

[Proofmode terms](https://github.com/leanprover-community/iris-lean/blob/db1455fc53d99480bc87698f60e0ba8992e391a3/src/Iris/ProofMode/Patterns/ProofModeTerm.lean#L13) currently use Iris syntax, which specializes terms using a clunky `with` and `$!` for Iris and Lean level variables separately. Is a cleaner syntax possible?

Co-authored-by: Zongyuan Liu

feat: View CMRA

1

Depends on #88

Depends on #90

Depends on #88

ispecialize terms of the form P ∗ Q -∗ R

4

Right now, I don't think we can specialize a hypothesis of the form ``` ∗H : P ∗ Q -∗ R ∗HP : P ∗HQ : Q ``` without exiting...

Most of our code is not documented. Adding docstrings would help new users get familiar with Iris.

iApply tactic

1

The current tactic suite does not include `iApply`. It is currently unclear to me how much from MoSEL needs to be ported to implement this, so this issue might make...

Views CMRA

1

Depends on frac and dfrac