Merge requests · Iris / stdpp · GitLab

Add lemma `StronglySorted_app_iff`

!584 · created Jan 27, 2025 by Marijn van Wezel
updated Jan 27, 2025
add some zip lemmas

!582 · created Jan 14, 2025 by Kimaya Bedarkar
- 12
updated Jan 24, 2025
add 'notypeclasses apply' tactic

!581 · created Dec 13, 2024 by Ralf Jung
- 8
updated Jan 24, 2025
Draft: Use `RelDecision` when possible.

!571 · created Sep 06, 2024 by Robbert Krebbers
S-waiting-for-author
updated Sep 08, 2024
Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses

!555 · created Jun 05, 2024 by Michael Sammler
S-waiting-for-author
- 42
updated Jan 17, 2025
Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming 2 of 4 checklist items completed

!532 · created Oct 16, 2023 by Robbert Krebbers
S-waiting-for-author
- 2
updated Jan 17, 2025
Add a comment about `cancel_inj` and `cancel_surj`.

!527 · created Oct 14, 2023 by Robbert Krebbers
- 7
updated Oct 14, 2023
add basic list functionality with Z-based indexing

!439 · created Jan 09, 2023 by Ralf Jung
- 16
updated Jan 17, 2025
Add some _1, _2 lemmas for map_filter

!394 · created Jul 26, 2022 by Michael Sammler
S-waiting-for-author
- 11
updated Jan 17, 2025
Draft: Very preliminary version of a quick start guide for sets.

!372 · created Apr 08, 2022 by Robbert Krebbers
S-waiting-for-author
- 17
updated Feb 06, 2023
Added some lemmas about [sublist]

!357 · created Jan 12, 2022 by Jonas Kastberg
S-waiting-for-review
- 9
updated Oct 13, 2023