`conv`

is the syntax category for a "conv tactic", where "conv" is short
for conversion. A conv tactic is a program which receives a target, printed as
`| a`

, and is tasked with coming up with some term `b`

and a proof of `a = b`

.
It is mainly used for doing targeted term transformations, for example rewriting
only on the left side of an equality.

## Equations

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

## Equations

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

The `*`

occurrence list means to apply to all occurrences of the pattern.

## Equations

- Lean.Parser.Tactic.Conv.occsWildcard = Lean.ParserDescr.nodeWithAntiquot "occsWildcard" `Lean.Parser.Tactic.Conv.occsWildcard (Lean.ParserDescr.symbol "*")

A list `1 2 4`

of occurrences means to apply to the first, second, and fourth
occurrence of the pattern.

## Equations

- Lean.Parser.Tactic.Conv.occsIndexed = Lean.ParserDescr.nodeWithAntiquot "occsIndexed" `Lean.Parser.Tactic.Conv.occsIndexed (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.const `num))

An occurrence specification, either `*`

or a list of numbers. The default is `[1]`

.

## Equations

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

`with_annotate_state stx t`

annotates the lexical range of `stx : Syntax`

with
the initial and final state of running tactic `t`

.

## Equations

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

`skip`

does nothing.

## Equations

- Lean.Parser.Tactic.Conv.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)

Traverses into the left subterm of a binary operator.
(In general, for an `n`

-ary operator, it traverses into the second to last argument.)

## Equations

- Lean.Parser.Tactic.Conv.lhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.lhs 1024 (Lean.ParserDescr.nonReservedSymbol "lhs" false)

Traverses into the right subterm of a binary operator.
(In general, for an `n`

-ary operator, it traverses into the last argument.)

## Equations

- Lean.Parser.Tactic.Conv.rhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rhs 1024 (Lean.ParserDescr.nonReservedSymbol "rhs" false)

Reduces the target to Weak Head Normal Form. This reduces definitions
in "head position" until a constructor is exposed. For example, `List.map f [a, b, c]`

weak head normalizes to `f a :: List.map f [b, c]`

.

## Equations

- Lean.Parser.Tactic.Conv.whnf = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.whnf 1024 (Lean.ParserDescr.nonReservedSymbol "whnf" false)

Expands let-declarations and let-variables.

## Equations

- Lean.Parser.Tactic.Conv.zeta = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.zeta 1024 (Lean.ParserDescr.nonReservedSymbol "zeta" false)

Puts term in normal form, this tactic is meant for debugging purposes only.

## Equations

- Lean.Parser.Tactic.Conv.reduce = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.reduce 1024 (Lean.ParserDescr.nonReservedSymbol "reduce" false)

Performs one step of "congruence", which takes a term and produces
subgoals for all the function arguments. For example, if the target is `f x y`

then
`congr`

produces two subgoals, one for `x`

and one for `y`

.

## Equations

- Lean.Parser.Tactic.Conv.congr = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.congr 1024 (Lean.ParserDescr.nonReservedSymbol "congr" false)

`arg i`

traverses into the`i`

'th argument of the target. For example if the target is`f a b c d`

then`arg 1`

traverses to`a`

and`arg 3`

traverses to`c`

.`arg @i`

is the same as`arg i`

but it counts all arguments instead of just the explicit arguments.

## Equations

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

`ext x`

traverses into a binder (a `fun x => e`

or `∀ x, e`

expression)
to target `e`

, introducing name `x`

in the process.

## Equations

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

`change t'`

replaces the target `t`

with `t'`

,
assuming `t`

and `t'`

are definitionally equal.

## Equations

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

`delta id1 id2 ...`

unfolds all occurrences of `id1`

, `id2`

, ... in the target.
Like the `delta`

tactic, this ignores any definitional equations and uses
primitive delta-reduction instead, which may result in leaking implementation details.
Users should prefer `unfold`

for unfolding definitions.

## Equations

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

`unfold foo`

unfolds all occurrences of`foo`

in the target.`unfold id1 id2 ...`

is equivalent to`unfold id1; unfold id2; ...`

. Like the`unfold`

tactic, this uses equational lemmas for the chosen definition to rewrite the target. For recursive definitions, only one layer of unfolding is performed.

## Equations

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

`pattern pat`

traverses to the first subterm of the target that matches`pat`

.`pattern (occs := *) pat`

traverses to every subterm of the target that matches`pat`

which is not contained in another match of`pat`

. It generates one subgoal for each matching subterm.`pattern (occs := 1 2 4) pat`

matches occurrences`1, 2, 4`

of`pat`

and produces three subgoals. Occurrences are numbered left to right from the outside in.

Note that skipping an occurrence of `pat`

will traverse inside that subexpression, which means
it may find more matches and this can affect the numbering of subsequent pattern matches.
For example, if we are searching for `f _`

in `f (f a) = f b`

:

`occs := 1 2`

(and`occs := *`

) returns`| f (f a)`

and`| f b`

`occs := 2`

returns`| f a`

`occs := 2 3`

returns`| f a`

and`| f b`

`occs := 1 3`

is an error, because after skipping`f b`

there is no third match.

## Equations

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

`rw [thm]`

rewrites the target using `thm`

. See the `rw`

tactic for more information.

## Equations

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

`simp_match`

simplifies match expressions. For example,

```
match [a, b] with
| [] => 0
| hd :: tl => hd
```

simplifies to `a`

.

## Equations

- Lean.Parser.Tactic.Conv.simpMatch = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.simpMatch 1024 (Lean.ParserDescr.nonReservedSymbol "simp_match" false)

Executes the given tactic block without converting `conv`

goal into a regular goal.

## Equations

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

Executes the given conv block without converting regular goal into a `conv`

goal.

## Equations

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

`{ convs }`

runs the list of `convs`

on the current target, and any subgoals that
remain are trivially closed by `skip`

.

## Equations

- Lean.Parser.Tactic.Conv.nestedConv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedConv 1022 Lean.Parser.Tactic.Conv.convSeqBracketed

`(convs)`

runs the `convs`

in sequence on the current list of targets.
This is pure grouping with no added effects.

## Equations

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

`rfl`

closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).

## Equations

- Lean.Parser.Tactic.Conv.convRfl = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRfl 1024 (Lean.ParserDescr.nonReservedSymbol "rfl" false)

`done`

succeeds iff there are no goals remaining.

## Equations

- Lean.Parser.Tactic.Conv.convDone = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convDone 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)

`trace_state`

prints the current goal state.

## Equations

- Lean.Parser.Tactic.Conv.convTrace_state = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convTrace_state 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)

`all_goals tac`

runs `tac`

on each goal, concatenating the resulting goals, if any.

## Equations

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

`any_goals tac`

applies the tactic `tac`

to every goal, and succeeds if at
least one application succeeds.

## Equations

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

`case tag => tac`

focuses on the goal with case name`tag`

and solves it using`tac`

, or else fails.`case tag x₁ ... xₙ => tac`

additionally renames the`n`

most recent hypotheses with inaccessible names to the given names.`case tag₁ | tag₂ => tac`

is equivalent to`(case tag₁ => tac); (case tag₂ => tac)`

.

## Equations

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

`case'`

is similar to the `case tag => tac`

tactic, but does not ensure the goal
has been solved after applying `tac`

, nor admits the goal if `tac`

failed.
Recall that `case`

closes the goal using `sorry`

when `tac`

fails, and
the tactic execution is not interrupted.

## Equations

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

`next => tac`

focuses on the next goal and solves it using `tac`

, or else fails.
`next x₁ ... xₙ => tac`

additionally renames the `n`

most recent hypotheses with
inaccessible names to the given names.

## Equations

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

`focus tac`

focuses on the main goal, suppressing all other goals, and runs `tac`

on it.
Usually `· tac`

, which enforces that the goal is closed by `tac`

, should be preferred.

## Equations

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

`conv => cs`

runs `cs`

in sequence on the target `t`

,
resulting in `t'`

, which becomes the new target subgoal.

## Equations

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

`· conv`

focuses on the main conv goal and tries to solve it using `s`

.

## Equations

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

`fail_if_success t`

fails if the tactic `t`

succeeds.

## Equations

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

`rw [rules]`

applies the given list of rewrite rules to the target.
See the `rw`

tactic for more information.

## Equations

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

`erw [rules]`

is a shorthand for `rw (config := { transparency := .default }) [rules]`

.
This does rewriting up to unfolding of regular definitions (by comparison to regular `rw`

which only unfolds `@[reducible]`

definitions).

## Equations

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

`args`

traverses into all arguments. Synonym for `congr`

.

## Equations

- Lean.Parser.Tactic.Conv.convArgs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convArgs 1024 (Lean.ParserDescr.nonReservedSymbol "args" false)

`left`

traverses into the left argument. Synonym for `lhs`

.

## Equations

- Lean.Parser.Tactic.Conv.convLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)

`right`

traverses into the right argument. Synonym for `rhs`

.

## Equations

- Lean.Parser.Tactic.Conv.convRight = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRight 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)

`intro`

traverses into binders. Synonym for `ext`

.

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

`enter [arg, ...]`

is a compact way to describe a path to a subterm.
It is a shorthand for other conv tactics as follows:

`enter [i]`

is equivalent to`arg i`

.`enter [@i]`

is equivalent to`arg @i`

.`enter [x]`

(where`x`

is an identifier) is equivalent to`ext x`

. For example, given the target`f (g a (fun x => x b))`

,`enter [1, 2, x, 1]`

will traverse to the subterm`b`

.

## Equations

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

The `apply thm`

conv tactic is the same as `apply thm`

the tactic.
There are no restrictions on `thm`

, but strange results may occur if `thm`

cannot be reasonably interpreted as proving one equality from a list of others.

## Equations

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

`try tac`

runs `tac`

and succeeds even if `tac`

failed.

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

`repeat convs`

runs the sequence `convs`

repeatedly until it fails to apply.

## Equations

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

`conv => ...`

allows the user to perform targeted rewriting on a goal or hypothesis,
by focusing on particular subexpressions.

See https://leanprover.github.io/theorem_proving_in_lean4/conv.html for more details.

Basic forms:

`conv => cs`

will rewrite the goal with conv tactics`cs`

.`conv at h => cs`

will rewrite hypothesis`h`

.`conv in pat => cs`

will rewrite the first subexpression matching`pat`

(see`pattern`

).

## Equations

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