A lens for zoming 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

app_fun : expr_lens → expr → expr_lens
app_arg : expr_lens → expr → expr_lens
entire : expr_lens

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

@[instance]

def expr_lens.dir.decidable_eq :

decidable_eq expr_lens.dir

source

@[instance]

def expr_lens.dir.inhabited :

inhabited expr_lens.dir

source

inductive expr_lens.dir :

Type

F : expr_lens.dir
A : expr_lens.dir

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 (not currently in mathlib).

source

def expr_lens.dir.to_string :

expr_lens.dir → string

String representation of dir.

Equations

expr_lens.dir.A.to_string = "A"
expr_lens.dir.F.to_string = "F"

source

@[instance]

def expr_lens.has_to_string :

has_to_string expr_lens.dir

Equations

expr_lens.has_to_string = {to_string := expr_lens.dir.to_string}

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 :

expr → expr → 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} :

(expr_lens → expr → tactic (list α)) → 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.

mathlib documentation

meta.expr_lens

A lens for zoming into nested `expr` applications

Tags

Declarations about `expr_lens`

General documentation

Additional documentation

Library

mathlib documentation

meta.​expr_lens

A lens for zoming into nested expr applications

Tags

Declarations about expr_lens

General documentation

Additional documentation

Library

meta.expr_lens

A lens for zoming into nested `expr` applications

Declarations about `expr_lens`