Issues · Iris / stdpp · GitLab

solve_ndisj taking a long time

#47 · opened Dec 03, 2019 by Jonas Kastberg
- 1
updated Dec 04, 2019
Provide a proof of the vec_to_list correspondence.

#45 · opened Oct 27, 2019 by Tiago Campos
- 0
updated Oct 27, 2019
`Hint Mode` for `QuoteLookup` and `Quote`

#44 · opened Sep 16, 2019 by Dan Frumin
- 4
updated Sep 19, 2019
Provide a total version of `!!` for finite maps and lists

#43 · opened Sep 16, 2019 by Robbert
- 7
updated Nov 17, 2019
Provide a better `inversion` tactic

#40 · opened Aug 23, 2019 by Robbert
- 3
updated Aug 24, 2019
Create list of tactics provided by std++

#39 · opened Jul 04, 2019 by Robbert
- 1
updated Jul 04, 2019
Add a test for solve_proper on a unary function

#38 · opened Jul 02, 2019 by Ralf Jung
- 0
updated Jul 02, 2019
Extend `solve_proper` to better handle HO functions

#37 · opened Jul 02, 2019 by Robbert
- 1
updated Aug 22, 2019
Unify case_bool_decide / case_decide

#35 · opened Jun 22, 2019 by Ralf Jung
- 0
updated Jun 22, 2019
Map singleton notation overlaps with Coq record syntax

#32 · opened Jun 10, 2019 by Ralf Jung
- 0
updated Jun 10, 2019
Addition is only declared as `Commutative` in iris

#31 · opened Jun 04, 2019 by Paolo G. Giarrusso
- 1
updated Jun 14, 2019
More generic `FMap` type class that also supports collections

#21 · opened Oct 04, 2018 by Robbert wishlist
- 5
updated Nov 07, 2019
What about `Universe Minimization ToSet`?

#19 · opened Jun 09, 2018 by Ralf Jung
- 1
updated Jun 09, 2018
Notation for type class logic connectives as `TCAnd`, `TCOr`, ...

#11 · opened Feb 08, 2018 by Robbert
- 22
updated Feb 20, 2018
Inconsistent `RewriteRelation` instances

#10 · opened Jan 10, 2018 by Robbert
- 2
updated Jul 03, 2019
Make more consistent use of coqdoc for web doc

#9 · opened Dec 07, 2017 by Ralf Jung
- 14
updated Jun 17, 2019
`f_equiv` with different functions in head position produces a Leibniz equality

#8 · opened Dec 01, 2017 by Robbert
- 1
updated Aug 22, 2019
Improve support of simplify_option_eq (and simplify_map_eq?) for setoids

#7 · opened Nov 13, 2017 by Robbert wishlist
- 0
updated Feb 20, 2019
`done` loops because it repeatedly applies `split`

#6 · opened Oct 31, 2017 by Robbert
- 1
updated Nov 01, 2017
Something in std++ enables implicit generalization of instances

#5 · opened Oct 27, 2017 by Ralf Jung
- 14
updated Nov 14, 2017