A user-defined simplification procedure used by the `simp`

tactic, and its variants.
Here is an example.

```
simproc reduce_add (_ + _) := fun e => do
unless (e.isAppOfArity ``HAdd.hAdd 6) do return none
let some n ← getNatValue? (e.getArg! 4) | return none
let some m ← getNatValue? (e.getArg! 5) | return none
return some (.done { expr := mkNatLit (n+m) })
```

The `simp`

tactic invokes `reduce_add`

whenever it finds a term of the form `_ + _`

.
The simplification procedures are stored in an (imperfect) discrimination tree.
The procedure should **not** assume the term `e`

perfectly matches the given pattern.
The body of a simplification procedure must have type `Simproc`

, which is an alias for
`Expr → SimpM (Option Step)`

.
You can instruct the simplifier to apply the procedure before its sub-expressions
have been simplified by using the modifier `↓`

before the procedure name. Example.

```
simproc ↓ reduce_add (_ + _) := fun e => ...
```

Simplification procedures can be also scoped or local.

## Equations

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

## Instances For

A user-defined simplification procedure declaration. To activate this procedure in `simp`

tactic,
we must provide it as an argument, or use the command `attribute`

to set its `[simproc]`

attribute.

## Equations

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

## Instances For

A builtin simplification procedure.

## Equations

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

## Instances For

A builtin simplification procedure declaration.

## Equations

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

## Instances For

Auxiliary command for associating a pattern with a simplification procedure.

## Equations

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

## Instances For

Auxiliary command for associating a pattern with a builtin simplification procedure.

## Equations

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

## Instances For

Auxiliary attribute for simplification procedures.

## Equations

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

## Instances For

Auxiliary attribute for symbolic evaluation procedures.

## Equations

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

## Instances For

Auxiliary attribute for builtin simplification procedures.

## Equations

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

## Instances For

Auxiliary attribute for builtin symbolic evaluation procedures.

## Equations

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