# The `set`

tactic #

This file defines the `set`

tactic and its variant `set!`

.

`set a := t with h`

is a variant of `let a := t`

. It adds the hypothesis `h : a = t`

to
the local context and replaces `t`

with `a`

everywhere it can.
`set a := t with ← h`

will add `h : t = a`

instead.
`set! a := t with h`

does not do any replacing.

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