# mathlibdocumentation

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.

def expr.coord.code  :

Convert the coord enum to its index number.

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

@[instance]

@[instance]

Equations

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

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
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

@[instance]

Equations

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.