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
The coordinate 3 = maxChildren - 1 is
reserved to denote the type of the expression.
Equations
The Pos representing the root subexpression.
Equations
Equations
- Lean.SubExpr.Pos.instInhabitedPos = { default := Lean.SubExpr.Pos.root }
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.
Fold over the position starting at the root and heading to the leaf
Fold over the position starting at the leaf and heading to the root
monad-fold over the position starting at the root and heading to the leaf
monad-fold over the position starting at the leaf and finishing at the root.
Equations
- Lean.SubExpr.Pos.depth p = Lean.SubExpr.Pos.foldr (fun (x : Nat) => Nat.succ) p 0
Returns true if pred is true for each coordinate in p.
Equations
- Lean.SubExpr.Pos.all pred p = Option.isSome (OptionT.run (Lean.SubExpr.Pos.foldrM (fun (n : Nat) (a : Unit) => if pred n = true then pure a else failure) p ()))
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.ofArray for details.
cs[0] is the coordinate for the root expression.
Equations
- Lean.SubExpr.Pos.toArray p = Lean.SubExpr.Pos.foldl Array.push #[] p
Equations
Equations
Equations
Equations
Equations
Equations
- Lean.SubExpr.Pos.pushNaryFn numArgs p = Lean.SubExpr.Pos.asNat p * Lean.SubExpr.Pos.maxChildren ^ numArgs
Equations
- Lean.SubExpr.Pos.pushNaryArg numArgs argIdx p = let_fun this := Lean.SubExpr.Pos.asNat p * Lean.SubExpr.Pos.maxChildren ^ (numArgs - argIdx) + 1; this
Equations
- Lean.SubExpr.Pos.toString p = (fun (x : String) => "/" ++ x) (String.intercalate "/" (List.map toString (Array.toList (Lean.SubExpr.Pos.toArray p))))
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
- Lean.SubExpr.Pos.instOrdPos = let_fun this := inferInstance; this
Equations
- Lean.SubExpr.Pos.instDecidableEqPos = let_fun this := inferInstance; this
Equations
- Lean.SubExpr.Pos.instToStringPos = { toString := Lean.SubExpr.Pos.toString }
Equations
- Lean.SubExpr.Pos.instEmptyCollectionPos = { emptyCollection := Lean.SubExpr.Pos.root }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.SubExpr.Pos.instToJsonPos = { toJson := Lean.toJson ∘ Lean.SubExpr.Pos.toString }
Equations
- Lean.SubExpr.Pos.instFromJsonPos = { fromJson? := fun (j : Lean.Json) => Lean.fromJson? j >>= Lean.SubExpr.Pos.fromString? }
A subexpression of some root expression. Both its value and its position within the root are stored.
- expr : Lean.Expr
The subexpression.
- pos : Lean.SubExpr.Pos
The position of the subexpression within the root expression.
Instances For
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadReaderOfSubExprAnalyzeM
- Lean.PrettyPrinter.Delaborator.TopDownAnalyze.instMonadWithReaderOfSubExprAnalyzeM
- Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM
- Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM
- Lean.instInhabitedSubExpr
Equations
- Lean.instInhabitedSubExpr = { default := { expr := default, pos := default } }
Equations
- Lean.SubExpr.mkRoot e = { expr := e, pos := Lean.SubExpr.Pos.root }
Returns true if the selected subexpression is the topmost one.
Equations
Map from subexpr positions to values.
Equations
- Lean.SubExpr.PosMap α = Lean.RBMap Lean.SubExpr.Pos α compare
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
- Lean.SubExpr.instToJsonFVarId = { toJson := fun (f : Lean.FVarId) => Lean.toJson f.name }
Equations
- Lean.SubExpr.instToJsonMVarId = { toJson := fun (f : Lean.MVarId) => Lean.toJson f.name }
Equations
- Lean.SubExpr.instFromJsonFVarId = { fromJson? := fun (j : Lean.Json) => Lean.FVarId.mk <$> Lean.fromJson? j }
Equations
- Lean.SubExpr.instFromJsonMVarId = { fromJson? := fun (j : Lean.Json) => Lean.MVarId.mk <$> Lean.fromJson? j }
A location within a goal.
- hyp: Lean.FVarId → Lean.SubExpr.GoalLocation
One of the hypotheses.
- hypType: Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the type of one of the hypotheses.
- hypValue: Lean.FVarId → Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the value of one of the let-bound hypotheses.
- target: Lean.SubExpr.Pos → Lean.SubExpr.GoalLocation
A subexpression of the goal type.
Equations
- Lean.SubExpr.instFromJsonGoalLocation = { fromJson? := Lean.SubExpr.fromJsonGoalLocation✝ }
Equations
A location within a goal state. It identifies a specific goal together with a GoalLocation
within it.
- mvarId : Lean.MVarId
Which goal the location is in.
Equations
- Lean.SubExpr.instFromJsonGoalsLocation = { fromJson? := Lean.SubExpr.fromJsonGoalsLocation✝ }
Same as Expr.traverseApp but also includes a
SubExpr.Pos argument for tracking subexpression position.
Equations
- One or more equations did not get rendered due to their size.
- Lean.Expr.traverseAppWithPos visit p e = visit p e