# Irreducible definitions #

This file defines an `irreducible_def`

command,
which works almost like the `def`

command
except that the introduced definition
does not reduce to the value.
Instead, the command
adds a `_def`

lemma
which can be used for rewriting.

```
irreducible_def frobnicate (a b : Nat) :=
a + b
example : frobnicate a 0 = a := by
simp [frobnicate_def]
```

`delta% t`

elaborates to a head-delta reduced version of `t`

.

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

Introduces an irreducible definition.
`irreducible_def foo := 42`

generates
a constant `foo : Nat`

as well as
a theorem `foo_def : foo = 42`

.

## Equations

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