A lens for zoming into nested
A "lens" for looking into the subterms of an expression, tracking where we've been, so that
when we "zoom out" after making a change we know exactly which order of
congr_args we need to make things work.
This file is for non-tactics.
expr, expr_lens, congr, environment, meta, metaprogramming, tactic
You're supposed to think of an
expr_lens as a big set of nested applications with a single
hole which needs to be filled, either in a function spot or argument spot.
fill this hole and turn your lens back into a real
This type is used in the development of rewriting tactics such as
rewrite_search (not currently in mathlib).
app_map F e maps a function
F which understands
expr_lenses over the given
e : expr in the natural way;
that is, make holes in
e everywhere where that is possible (generating
expr_lenses in the
process), and at each stage call the function
F passing both the
expr_lens generated and the
expr which was removed to make the hole.
At each stage
F returns a list of some type, and
app_map collects these lists together and
returns a concatenation of them all.