Skip to content

Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming

Robbert Krebbers requested to merge ci/refactor_staging into master

!507 (closed) ballooned into this huge change. This contains the following two MRs:

There is more that could be done, but that is postponed (we should probably open an issue):

Edited by Ralf Jung

Merge request reports