Merge requests · Iris / stdpp

Add `prod_swap` and some basic results for it.

!529 · created Oct 14, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 14, 2023
Missing `Params` instances for `prod_map` and `prod_zip`.

!528 · created Oct 14, 2023 by Robbert Krebbers
- Merged
updated Oct 14, 2023
add inv and oinv tactics that are basically a smarter and fixed inversion_clear

!525 · created Oct 14, 2023 by Ralf Jung
- Merged
- 15
updated Oct 14, 2023
Add lemmas for easy measure/size induction.

!519 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 31
updated Oct 14, 2023
remove 'wf' alias for the standard 'well_founded'

!524 · created Oct 14, 2023 by Ralf Jung
- Merged
- 7
updated Oct 14, 2023
solve_proper: add support for subrelation

!495 · created Aug 08, 2023 by Ralf Jung
- Merged
- 70
updated Oct 13, 2023
Add `TCSimpl` type class.

!521 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 12
updated Oct 13, 2023
Add `MThrow` and replace `MGuard`

!522 · created Oct 06, 2023 by Thibaut Pérami
- Merged
- 35
updated Oct 13, 2023
Use hint mode + more often

!435 · created Dec 15, 2022 by Robbert Krebbers
S-waiting-for-author
- Closed
- 3
updated Oct 13, 2023
Added some lemmas about [sublist]

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

!516 · created Oct 04, 2023 by Johannes Hostert
- Merged
- 24
updated Oct 11, 2023
Improve comment of `TCEq`.

!523 · created Oct 06, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 07, 2023
Change mode of `TCEq`.

!123 · created Mar 10, 2020 by Robbert Krebbers
- Merged
- 1
updated Oct 06, 2023
Add instance `cons_equiv_inj`.

!520 · created Oct 06, 2023 by Robbert Krebbers
- Merged
updated Oct 06, 2023
Replace `MGuard` with `MFail`

!488 · created Jul 26, 2023 by Adam
- Closed
- 25
updated Oct 06, 2023
Add MRaise typeclass

!501 · created Aug 30, 2023 by Thibaut Pérami
- Closed
- 22
updated Oct 06, 2023
prove general fmap_inj lemmas

!496 · created Aug 10, 2023 by Ralf Jung
- Merged
- 4
updated Oct 06, 2023
Rework lemmas for `take/drop` of an `++`:

!518 · created Oct 05, 2023 by Robbert Krebbers
- Merged
- 3
updated Oct 05, 2023
Add lemmas for `reverse` of `take`/`drop`.

!517 · created Oct 05, 2023 by Robbert Krebbers
- Merged
- 2
updated Oct 05, 2023
add odestruct and other "open term" tactics

!512 · created Sep 27, 2023 by Ralf Jung
- Merged
- 59
updated Oct 03, 2023