Skip to content

More consistent names for `fill` lemmas of `LanguageCtx`.

Robbert Krebbers requested to merge robbert/fill into master

I now consistently use _inv for the reverse direction, as we already used to do at various places. For example:

Lemma reducible_fill `{!@LanguageCtx Λ K} e σ :
  reducible e σ  reducible (K e) σ.
Lemma reducible_fill_inv `{!@LanguageCtx Λ K} e σ :
  to_val e = None  reducible (K e) σ  reducible e σ.

Merge request reports