- Jun 03, 2021
-
-
Ralf Jung authored
-
- Jun 02, 2021
-
-
Robbert Krebbers authored
Thanks to @tchajed for pointing out the omission.
-
Robbert Krebbers authored
Various improvements to `Permutation` lemmas and instances See merge request iris/stdpp!270
-
- Jun 01, 2021
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r` and `Permutation_singleton_r`. Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.
-
Robbert Krebbers authored
Naming scheme: `operation_Permutation_{Proper,inj,inj_l,inj_r}`.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 31, 2021
-
-
Robbert Krebbers authored
-
- May 28, 2021
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Comment about `EqDecision` in `Countable`. See merge request !268
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- May 27, 2021
- May 26, 2021
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Thanks to @jules for pointing out these were missing.
-
- May 25, 2021
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
This reverts commit 267cc708. Thanks to @jung for spotting this was a NOP, see !263 (comment 67379)
-
Robbert Krebbers authored
list lookup lemmas: cons, singleton See merge request !264
-
-
- May 20, 2021