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.

Instances For

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

    Instances For

      The Pos representing the root subexpression.

      Instances For

        The coordinate deepest in the Pos.

        Instances For
          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} [Inhabited α] {M : TypeType u_1} [Monad M] (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} [Monad M] (f : NatαM α) (p : Lean.SubExpr.Pos) (a : α) :
          M α

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

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

          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.

            Instances For

              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.

              Instances For
                Instances For
                  structure Lean.SubExpr :

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

                  Instances For

                    Returns true if the selected subexpression is the topmost one.

                    Instances For
                      @[inline, reducible]
                      abbrev Lean.SubExpr.PosMap (α : Type u) :

                      Map from subexpr positions to values.

                      Instances For

                        A location within a goal.

                        Instances For

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

                          Instances For

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

                            Equations
                            Instances For