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]

def Lean.Elab.Command.«termDelta%_» : Lean.ParserDescr

delta% t elaborates to a head-delta reduced version of t.

Equations

• Lean.Elab.Command.«termDelta%_» = Lean.ParserDescr.node `Lean.Elab.Command.termDelta%_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "delta% ") (Lean.ParserDescr.cat `term 0))

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

Equations

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

def Lean.Elab.Command.command_Irreducible_def____ : Lean.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.