Additional `conv`

tactics.

## Equations

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

## Instances For

## Equations

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

## Instances For

## Equations

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

## Instances For

`conv in pat => cs`

runs the `conv`

tactic sequence `cs`

on the first subexpression matching the pattern `pat`

in the target.
The converted expression becomes the new target subgoal, like `conv => cs`

.

The arguments `in`

are the same as those as the in `pattern`

.
In fact, `conv in pat => cs`

is a macro for `conv => pattern pat; cs`

.

The syntax also supports the `occs`

clause. Example:

```
conv in (occs := *) x + y => rw [add_comm]
```

## Equations

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

## Instances For

`discharge => tac`

is a conv tactic which rewrites target`p`

to`True`

if`tac`

is a tactic which proves the goal`⊢ p`

.`discharge`

without argument returns`⊢ p`

as a subgoal.

## Equations

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

## Instances For

Elaborator for the `discharge`

tactic.

## Equations

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

## Instances For

Use `refine`

in `conv`

mode.

## Equations

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

## Instances For

The command `#conv tac => e`

will run a conv tactic `tac`

on `e`

, and display the resulting
expression (discarding the proof).
For example, `#conv rw [true_and_iff] => True ∧ False`

displays `False`

.
There are also shorthand commands for several common conv tactics:

`#whnf e`

is short for`#conv whnf => e`

`#simp e`

is short for`#conv simp => e`

`#norm_num e`

is short for`#conv norm_num => e`

`#push_neg e`

is short for`#conv push_neg => e`

## Equations

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

## Instances For

`with_reducible tacs`

executes `tacs`

using the reducible transparency setting.
In this setting only definitions tagged as `[reducible]`

are unfolded.

## Equations

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

## Instances For

The command `#whnf e`

evaluates `e`

to Weak Head Normal Form, which means that the "head"
of the expression is reduced to a primitive - a lambda or forall, or an axiom or inductive type.
It is similar to `#reduce e`

, but it does not reduce the expression completely,
only until the first constructor is exposed. For example:

```
open Nat List
set_option pp.notation false
#whnf [1, 2, 3].map succ
-- cons (succ 1) (map succ (cons 2 (cons 3 nil)))
#reduce [1, 2, 3].map succ
-- cons 2 (cons 3 (cons 4 nil))
```

The head of this expression is the `List.cons`

constructor,
so we can see from this much that the list is not empty,
but the subterms `Nat.succ 1`

and `List.map Nat.succ (List.cons 2 (List.cons 3 List.nil))`

are
still unevaluated. `#reduce`

is equivalent to using `#whnf`

on every subexpression.

## Equations

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

## Instances For

The command `#whnfR e`

evaluates `e`

to Weak Head Normal Form with Reducible transparency,
that is, it uses `whnf`

but only unfolding reducible definitions.

## Equations

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

## Instances For

`#simp => e`

runs`simp`

on the expression`e`

and displays the resulting expression after simplification.`#simp only [lems] => e`

runs`simp only [lems]`

on`e`

.- The
`=>`

is optional, so`#simp e`

and`#simp only [lems] e`

have the same behavior. It is mostly useful for disambiguating the expression`e`

from the lemmas.

## Equations

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