Documentation

Mathlib.Tactic.IrreducibleDef

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
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.
      Instances For