Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming
- Oct 20, 2023
-
-
Robbert Krebbers authored
Fix inconsistencies in `lookup` and `elem_of` lemmas for `list` See merge request !531
-
Robbert Krebbers authored07c4f0ee
-
Robbert Krebbers authoredfacb9097
-
Robbert Krebbers authoredd624ecd7
-
Robbert Krebbers authored9d2e6d60
-
- Oct 17, 2023
-
-
Robbert Krebbers authored44d3349c
-
Robbert Krebbers authoredd9a6e55e
-
Robbert Krebbers authored
Provide "lookup" and "commuting" lemmas that handle "eq" and "ne" case in a single statement. See merge request !526
-
Robbert Krebbers authored0a52e84c
-
- Oct 16, 2023
-
-
Robbert Krebbers authored211ee09d
-
Robbert Krebbers authoredf85c45f4
-
Robbert Krebbers authoredb7eaaf91
-
- Oct 15, 2023
-
-
Robbert Krebbers authoredec2d6bdd
-
