mathlib documentation

core / init.meta.expr_address

inductive expr.coord  :

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.



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

def expr.address  :

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.


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.