A lens for zooming into nested
expr applications #
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 defines the
expr_lens inductive type, defines basic operations this type, and defines a
useful map-like function
exprs which maps over applications.
This file is for non-tactics.
expr, expr_lens, congr, environment, meta, metaprogramming, tactic
- F : expr_lens.dir
- A : expr_lens.dir
Inductive type with two constructors
that represent the function-part
f and arg-part
a of an application
f a. They specify the
directions in which an
expr_lens should zoom into an
This type is used in the development of rewriting tactics such as
String representation of
- expr_lens.dir.A.to_string = "A"
- expr_lens.dir.F.to_string = "F"