def Lean.SubExpr.Pos : Type

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.

def Lean.SubExpr.Pos.maxChildren : Nat

def Lean.SubExpr.Pos.typeCoord : Nat

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

def Lean.SubExpr.Pos.asNat : Pos → Nat

def Lean.SubExpr.Pos.root : Pos

The Pos representing the root subexpression.

instance Lean.SubExpr.Pos.instInhabited : Inhabited Pos

def Lean.SubExpr.Pos.isRoot (p : Pos) : Bool

def Lean.SubExpr.Pos.head (p : Pos) : Nat

The coordinate deepest in the Pos.

def Lean.SubExpr.Pos.tail (p : Pos) : Pos

def Lean.SubExpr.Pos.push (p : Pos) (c : Nat) : Pos

partial def Lean.SubExpr.Pos.foldl {α : Type} (f : α → Nat → α) (init : α) (p : Pos) : α

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

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

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

partial def Lean.SubExpr.Pos.foldlM {α : Type} [Inhabited α] {M : Type → Type u_1} [Monad M] (f : α → Nat → M α) (init : α) (p : Pos) : M α

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

partial def Lean.SubExpr.Pos.foldrM {α : Type} {M : Type → Type u_1} [Monad M] (f : Nat → α → M α) (p : Pos) (init : α) : M α

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

def Lean.SubExpr.Pos.depth (p : Pos) : Nat

def Lean.SubExpr.Pos.all (pred : Nat → Bool) (p : Pos) : Bool

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

def Lean.SubExpr.Pos.append : Pos → Pos → Pos

def Lean.SubExpr.Pos.ofArray (ps : Array Nat) : Pos

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.

def Lean.SubExpr.Pos.toArray (p : Pos) : Array Nat

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.

def Lean.SubExpr.Pos.pushBindingDomain (p : Pos) : Pos

def Lean.SubExpr.Pos.pushBindingBody (p : Pos) : Pos

def Lean.SubExpr.Pos.pushLetVarType (p : Pos) : Pos

def Lean.SubExpr.Pos.pushLetValue (p : Pos) : Pos

def Lean.SubExpr.Pos.pushLetBody (p : Pos) : Pos

def Lean.SubExpr.Pos.pushAppFn (p : Pos) : Pos

def Lean.SubExpr.Pos.pushAppArg (p : Pos) : Pos

def Lean.SubExpr.Pos.pushProj (p : Pos) : Pos

def Lean.SubExpr.Pos.pushType (p : Pos) : Pos

def Lean.SubExpr.Pos.pushNaryFn (numArgs : Nat) (p : Pos) : Pos

def Lean.SubExpr.Pos.pushNaryArg (numArgs argIdx : Nat) (p : Pos) : Pos

def Lean.SubExpr.Pos.pushNthBindingDomain (binderIdx : Nat) : Pos → Pos

def Lean.SubExpr.Pos.pushNthBindingBody (numBinders : Nat) : Pos → Pos

def Lean.SubExpr.Pos.toString (p : Pos) : String

def Lean.SubExpr.Pos.fromString? : String → Except String Pos

def Lean.SubExpr.Pos.fromString! (s : String) : Pos

instance Lean.SubExpr.Pos.instOrd : Ord Pos

instance Lean.SubExpr.Pos.instDecidableEq : DecidableEq Pos

instance Lean.SubExpr.Pos.instToString : ToString Pos

instance Lean.SubExpr.Pos.instEmptyCollection : EmptyCollection Pos

instance Lean.SubExpr.Pos.instRepr : Repr Pos

instance Lean.SubExpr.Pos.instToJson : ToJson Pos

instance Lean.SubExpr.Pos.instFromJson : FromJson Pos

structure Lean.SubExpr : Type

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

• expr : Expr

  The subexpression.

• pos : Pos

  The position of the subexpression within the root expression.

instance Lean.instInhabitedSubExpr : Inhabited SubExpr

def Lean.SubExpr.mkRoot (e : Expr) : SubExpr

def Lean.SubExpr.isRoot (s : SubExpr) : Bool

Returns true if the selected subexpression is the topmost one.

@[reducible, inline]

abbrev Lean.SubExpr.PosMap (α : Type u) : Type u

Map from subexpr positions to values.

def Lean.SubExpr.bindingBody! : SubExpr → SubExpr

def Lean.SubExpr.bindingDomain! : SubExpr → SubExpr

instance Lean.SubExpr.instToJsonFVarId : ToJson FVarId

instance Lean.SubExpr.instToJsonMVarId : ToJson MVarId

instance Lean.SubExpr.instFromJsonFVarId : FromJson FVarId

instance Lean.SubExpr.instFromJsonMVarId : FromJson MVarId

inductive Lean.SubExpr.GoalLocation : Type

A location within a goal.

• hyp : FVarId → GoalLocation

  One of the hypotheses.

• hypType : FVarId → Pos → GoalLocation

  A subexpression of the type of one of the hypotheses.

• hypValue : FVarId → Pos → GoalLocation

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

• target : Pos → GoalLocation

  A subexpression of the goal type.

instance Lean.SubExpr.instFromJsonGoalLocation : FromJson GoalLocation

instance Lean.SubExpr.instToJsonGoalLocation : ToJson GoalLocation

structure Lean.SubExpr.GoalsLocation : Type

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

• mvarId : MVarId

  Which goal the location is in.

• loc : GoalLocation

instance Lean.SubExpr.instFromJsonGoalsLocation : FromJson GoalsLocation

instance Lean.SubExpr.instToJsonGoalsLocation : ToJson GoalsLocation

def Lean.Expr.traverseAppWithPos {M : Type → Type u_1} [Monad M] (visit : SubExpr.Pos → Expr → M Expr) (p : SubExpr.Pos) (e : Expr) : M Expr

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