# Documentation

Lean.SubExpr

A position of a subexpression in an expression.

See docstring of SubExpr for more detail.

Equations
Equations

The coordinate 3 = maxChildren - 1 is reserved to denote the type of the expression.

Equations
Equations

The Pos representing the root subexpression.

Equations
Equations

The coordinate deepest in the Pos.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
partial def Lean.SubExpr.Pos.foldl {α : Type} (f : αNatα) (a : α) (p : Lean.SubExpr.Pos) :
α

Fold over the position starting at the root and heading to the leaf

partial def Lean.SubExpr.Pos.foldr {α : Type} (f : Natαα) (p : Lean.SubExpr.Pos) (a : α) :
α

Fold over the position starting at the leaf and heading to the root

partial def Lean.SubExpr.Pos.foldlM {α : Type} [inst : ] {M : TypeType u_1} [inst : ] (f : αNatM α) (a : α) (p : Lean.SubExpr.Pos) :
M α

monad-fold over the position starting at the root and heading to the leaf

partial def Lean.SubExpr.Pos.foldrM {α : Type} {M : TypeType u_1} [inst : ] (f : NatαM α) (p : Lean.SubExpr.Pos) (a : α) :
M α

monad-fold over the position starting at the leaf and finishing at the root.

Equations

Returns true if pred is true for each coordinate in p.

Equations

Creates a subexpression Pos from an array of 'coordinates'. Each coordinate is a number {0,1,2} expressing which child subexpression should be explored. The first coordinate in the array corresponds to the root of the expression tree.

Equations

Decodes a subexpression Pos as a sequence of coordinates cs : Array Nat. See Pos.fromArray for details. cs[0] is the coordinate for the root expression.

Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
structure Lean.SubExpr :

An expression and the position of a subexpression within this expression.

Subexpressions are encoded as the current subexpression e and a position p : Pos denoting e's position with respect to the root expression.

We use a simple encoding scheme for expression positions Pos: every Expr constructor has at most 3 direct expression children. Considering an expression's type to be one extra child as well, we can injectively map a path of childIdxs to a natural number by computing the value of the 4-ary representation 1 :: childIdxs, since n-ary representations without leading zeros are unique. Note that pos is initialized to 1 (case childIdxs == []).

Instances For
Equations
Equations

Returns true if the selected subexpression is the topmost one.

Equations
@[inline]
abbrev Lean.SubExpr.PosMap (α : Type u) :

Map from subexpr positions to values.

Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Equations
Equations
• One of the hypotheses.

hyp:
• A subexpression of the type of one of the hypotheses.

hypType:
• A subexpression of the value of one of the let-bound hypotheses.

hypValue:
• A subexpression of the goal type.

target:

A location within a goal.

Instances For
Equations
Equations

A location within a goal state. It identifies a specific goal together with a GoalLocation within it.

Instances For
Equations
def Lean.Expr.traverseAppWithPos {M : TypeType u_1} [inst : ] (visit : ) (p : Lean.SubExpr.Pos) (e : Lean.Expr) :

Same as Expr.traverseApp but also includes a SubExpr.Pos argument for tracking subexpression position.

Equations