# Documentation

## Lean.SubExpr

A position of a subexpression in an 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 == []).

See also SubExpr.

Equations
Instances For
Equations
Instances For

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

Equations
Instances For
Equations
Instances For

The Pos representing the root subexpression.

Equations
Instances For
Equations
Instances For

The coordinate deepest in the Pos.

Equations
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
partial def Lean.SubExpr.Pos.foldl {α : Type} (f : αNatα) (init : α) (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) (init : α) :
α

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

partial def Lean.SubExpr.Pos.foldlM {α : Type} [] {M : TypeType u_1} [] (f : αNatM α) (init : α) (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} [] (f : NatαM α) (p : Lean.SubExpr.Pos) (init : α) :
M α

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

Equations
Instances For

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

Equations
Instances For
Equations
Instances For

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
Instances For

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

Equations
Instances For
Equations
• p.pushBindingDomain = p.push 0
Instances For
Equations
• p.pushBindingBody = p.push 1
Instances For
Equations
• p.pushLetVarType = p.push 0
Instances For
Equations
• p.pushLetValue = p.push 1
Instances For
Equations
• p.pushLetBody = p.push 2
Instances For
Equations
• p.pushAppFn = p.push 0
Instances For
Equations
• p.pushAppArg = p.push 1
Instances For
Equations
• p.pushProj = p.push 0
Instances For
Equations
• p.pushType =
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
• p.toString = (fun (x : String) => "/" ++ x) ("/".intercalate (List.map toString p.toArray.toList))
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Equations
Equations
Equations
structure Lean.SubExpr :

A subexpression of some root expression. Both its value and its position within the root are stored.

Instances For
Equations
Equations
Instances For

Returns true if the selected subexpression is the topmost one.

Equations
• s.isRoot = s.pos.isRoot
Instances For
@[reducible, inline]
abbrev Lean.SubExpr.PosMap (α : Type u) :

Map from subexpr positions to values.

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
Equations
Equations

A location within a goal.

• hyp:

One of the hypotheses.

• hypType:

A subexpression of the type of one of the hypotheses.

• hypValue:

A subexpression of the value of one of the let-bound hypotheses.

• target:

A subexpression of the goal type.

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} [] (visit : ) (p : Lean.SubExpr.Pos) (e : Lean.Expr) :

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

Equations
Instances For