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

source
def Lean.Elab.Command.irredDefLemma :
ParserDescr
Equations

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

Instances For

source
def Lean.Elab.Command.command_Irreducible_def____ :
ParserDescr

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.

Instances For