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

tactic, and its variants.
Here is an example.

```
theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]
open Lean Meta Simp
simproc ↓ shortCircuitAnd (And _ _) := fun e => do
let_expr And p q := e | return .continue
let r ← simp p
let_expr False := r.expr | return .continue
let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
return .done { expr := r.expr, proof? := some proof }
```

The `simp`

tactic invokes `shortCircuitAnd`

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

.
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 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.
Simplification procedures can be also scoped or local.

## Equations

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

## Instances For

Similar to `simproc`

, but resulting expression must be definitionally equal to the input one.

## 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 user-defined defeq 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 defeq 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

A builtin defeq 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.