Documentation

Mathlib.Lean.Meta.KAbstractPositions

Find the positions of a pattern in an expression #

This file defines some tools for dealing with sub expressions and occurrence numbers. This is used for creating a rw tactic call that rewrites a selected expression.

viewKAbstractSubExpr takes an expression and a position in the expression, and returns the sub-expression together with an optional occurrence number that would be required to find the sub-expression using kabstract (which is what rw uses to find the position of the rewrite)

rw can fail if the motive is not type correct. kabstractIsTypeCorrect checks whether this is the case.

source
def Lean.Meta.kabstractPositions (p : Lean.Expr) (e : Lean.Expr) :
Lean.MetaM (Array Lean.SubExpr.Pos)

Return the positions that kabstract would abstract for pattern p in expression e. i.e. the positions that unify with p.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.kabstractPositions.visit (p : Lean.Expr) (mctx : Lean.MetavarContext) (pHeadIdx : Lean.HeadIndex) (pNumArgs : Nat) (e : Lean.Expr) (pos : Lean.SubExpr.Pos) (positions : Array Lean.SubExpr.Pos) :
    Lean.MetaM (Array Lean.SubExpr.Pos)

    The main loop that loops through all subexpressions

    Instances For
      source
      def Lean.Meta.viewKAbstractSubExpr (e : Lean.Expr) (pos : Lean.SubExpr.Pos) :
      Lean.MetaM (Option (Lean.Expr × Option Nat))

      Return the subexpression at position pos in e together with an occurrence number that allows the expression to be found by kabstract. Return none when the subexpression contains loose bound variables.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Lean.Meta.kabstractIsTypeCorrect (e : Lean.Expr) (subExpr : Lean.Expr) (pos : Lean.SubExpr.Pos) :
        Lean.MetaM Bool

        Determine whether the result of abstracting subExpr from e at position pos results in a well typed expression. This is important if you want to rewrite at this position.

        Here is an example of what goes wrong with an ill-typed kabstract result:

        example (h : [5] ≠ []) : List.getLast [5] h = 5 := by
  rw [show [5] = [5] from rfl] -- tactic 'rewrite' failed, motive is not type correct
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For