Issues · Iris / Iris · GitLab

`big_op*_forall` that relate traversals over different structures

#262 · opened Aug 28, 2019 by Dmitry Khalanskiy A-coq C-enhancement Good First Issue T-algebra
- 6
updated Jan 21, 2020
Constructing CMRAs by giving isomorphism to CMRAs

#253 · opened Jul 09, 2019 by Paolo G. Giarrusso A-coq C-enhancement Good First Issue T-algebra
- 1
- 1
- 4
updated Sep 08, 2020
"Exponentiation" for separating conjunctions

#252 · opened Jul 09, 2019 by Dmitry Khalanskiy A-coq C-enhancement Good First Issue T-bi
- 3
updated Nov 01, 2019
Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent

#202 · opened Jun 18, 2018 by Robbert A-coq C-enhancement Good First Issue T-proofmode T-style
- 0
updated Nov 01, 2019
Make clear which arguments of tactics are optional in `ProofMode.md`

#158 · opened Feb 23, 2018 by Robbert A-docs C-enhancement Good First Issue T-proofmode
- 0
updated Mar 18, 2020