# 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.

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

The main loop that loops through all subexpressions

## Instances For

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

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.