mathlib documentation

core / init.meta.expr_address

inductive expr.coord  :
Type

An enum representing a recursive argument in an expr constructor. Types of local and meta variables are not included because they are not consistently set and depend on context.

@[protected]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations

Use this to pick the subexpression of a given expression that cooresponds to the given coordinate.

def expr.address  :
Type

An address is a list of coordinates used to reference subterms of an expression. The first coordinate in the list corresponds to the root of the expression.

Equations
@[protected, instance]
@[protected, instance]

as_below x y is some z when it finds ∃ z, x = y ++ z

follow a e finds the subexpression of e at the given address a.