Merged requested to merge robbert/kill_locked_value_lambdas into master
I noticed that various people (including yours truly) often get confused by the fact the parsing of
(λ: x, e)%V adds a
locked, while both
LamV x e and
locked (LamV x e) are pretty printed as
λ: x, e. As a result of these sneaky occurrences of
locked, it is often the case that lemmas or hypotheses that appear to be the same do not actually match. This MR repairs this situation by getting rid of
The main point of the
locked trick was to avoid
wp_pures to unfold lambdas/recs that are hidden behind a definition. E.g.,
wp_pures should not unfold
foo v with:
Definition foo := λ: "x", ...
In this MR I propose another approach:
- Use a
Hint Externto detect lambdas/recs. This will only work if they are not hidden behind a definition.
wp_lamadd an instance that recognizes lambdas/recs even if they are behind a definition.
- As a result of this MR I was able to remove some hacks, i.e. we no longer need to write
LamV ...in the
%Vnotations for e.g.
par; we can now just use the
- Iris-examples compile without any changes.