Irreducible definitions #
This file defines an
which works almost like the
except that the introduced definition
does not reduce to the value.
Instead, the command
which can be used for rewriting.
irreducible_def frobnicate (a b : Nat) := a + b example : frobnicate a 0 = a := by simp [frobnicate_def]