Issues · Iris / stdpp · GitLab

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 Jul 02, 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
- 1
updated Feb 20, 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
- 0
updated Dec 01, 2017
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
Big ops and lattices in stdpp?

#2 · opened Oct 10, 2017 by Hai Dang
- 1
- 2
updated Feb 17, 2019