command_Irreducible_def____ — Mathlib

Lean4
/-- Introduces an irreducible definition.
`irreducible_def foo := 42` generates
a constant `foo : Nat` as well as
a theorem `foo_def : foo = 42`.
-/
@[command_parser 1000]
public meta def command_Irreducible_def____ : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Lean.Elab.Command.command_Irreducible_def____ 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `declModifiers) (ParserDescr.symbol✝ "irreducible_def"))
            (ParserDescr.const✝ `declId))
          (ParserDescr.unary✝ `optional Lean.Elab.Command.irredDefLemma))
        (ParserDescr.unary✝ `ppIndent (ParserDescr.const✝ `optDeclSig)))
      (ParserDescr.const✝ `declVal))
Похожие утверждения