mathlib3 documentation

meta.expr_lens

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_funs and 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 expr.app_map on exprs which maps over applications.

This file is for non-tactics.

Tags #

expr, expr_lens, congr, environment, meta, metaprogramming, tactic

Declarations about expr_lens #

source
meta inductive expr_lens  :
Type

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. expr_lens.fill can fill this hole and turn your lens back into a real expr.

source
inductive expr_lens.dir  :
Type

Inductive type with two constructors F and A, 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 expr.

This type is used in the development of rewriting tactics such as nth_rewrite and rewrite_search.

Instances for expr_lens.dir
source
@[protected, instance]
def expr_lens.dir.decidable_eq  :
decidable_eq expr_lens.dir
source
@[protected, instance]
def expr_lens.dir.inhabited  :
inhabited expr_lens.dir
source
def expr_lens.dir.to_string  :
expr_lens.dir → string

String representation of dir.

Equations
source
@[protected, instance]
def expr_lens.dir.has_to_string  :
has_to_string expr_lens.dir
Equations
source
meta def expr_lens.fill  :
expr_lens → expr → expr

Fill the function or argument hole in this lens with the given expr.

source
meta def expr_lens.zoom  :
expr_lens → list expr_lens.dir → expr → option (expr_lens × expr)

Zoom into e : expr given the context of an expr_lens, popping out an expr and a new zoomed expr_lens, if this is possible (e has to be an application).

source
meta def expr_lens.to_dirs  :
expr_lens → list expr_lens.dir

Convert an expr_lens into a list of instructions needed to build it; repeatedly inspecting a function or its argument a finite number of times.

source
meta def expr_lens.mk_congr_arg_using_dsimp (G W : expr) (u : list name) :
tactic expr

Sometimes mk_congr_arg fails, when the function is 'superficially dependent'. Try to dsimp the function first before building the congr_arg expression.

source
meta def expr_lens.congr  :
expr_lens → expr → tactic expr

Turn an e : expr_lens and a proof that a = b into a series of congr_arg or congr_fun applications showing that the expressions obtained from e.fill a and e.fill b are equal.

source
meta def expr_lens.to_tactic_string  :
expr_lens → tactic string

Pretty print a lens.

source
meta def expr.app_map {α : Type u_1} (F : expr_lens → expr → tactic (list α)) (e : expr) :
tactic (list α)

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.