# Find the positions of a pattern in an expression #

This file defines some tools for dealing with subexpressions 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 subexpression together with an optional occurrence number that would be required to find the subexpression 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 e : Expr) :
MetaM (Array 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 : Expr) (mctx : MetavarContext) (pHeadIdx : HeadIndex) (pNumArgs : Nat) (e : Expr) (pos : SubExpr.Pos) (positions : Array SubExpr.Pos) :
MetaM (Array SubExpr.Pos)

The main loop that loops through all subexpressions

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.viewKAbstractSubExpr (e : Expr) (pos : SubExpr.Pos) :
MetaM (Option (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 subExpr : Expr) (pos : SubExpr.Pos) :
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