inductive Lean.Elab.DefKind : Type

• def: Lean.Elab.DefKind
• theorem: Lean.Elab.DefKind
• example: Lean.Elab.DefKind
• opaque: Lean.Elab.DefKind
• abbrev: Lean.Elab.DefKind

instance Lean.Elab.instInhabitedDefKind : Inhabited Lean.Elab.DefKind

instance Lean.Elab.instBEqDefKind : BEq Lean.Elab.DefKind

def Lean.Elab.DefKind.isTheorem : Lean.Elab.DefKind → Bool

def Lean.Elab.DefKind.isDefOrAbbrevOrOpaque : Lean.Elab.DefKind → Bool

def Lean.Elab.DefKind.isExample : Lean.Elab.DefKind → Bool

structure Lean.Elab.DefView : Type

• kind : Lean.Elab.DefKind
• ref : Lean.Syntax
• modifiers : Lean.Elab.Modifiers
• declId : Lean.Syntax
• binders : Lean.Syntax
• type? : Option Lean.Syntax
• value : Lean.Syntax
• deriving? : Option (Array Lean.Syntax)

instance Lean.Elab.instInhabitedDefView : Inhabited Lean.Elab.DefView

def Lean.Elab.DefView.isInstance (view : Lean.Elab.DefView) : Bool

def Lean.Elab.Command.mkDefViewOfAbbrev (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.DefView

def Lean.Elab.Command.mkDefViewOfDef (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.DefView

def Lean.Elab.Command.mkDefViewOfTheorem (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.DefView

def Lean.Elab.Command.mkFreshInstanceName : Lean.Elab.Command.CommandElabM Lake.Name

def Lean.Elab.Command.mkInstanceName (binders : Array Lean.Syntax) (type : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lake.Name

Generate a name for an instance with the given type. Note that we elaborate the type twice. Once for producing the name, and another when elaborating the declaration.

def Lean.Elab.Command.mkDefViewOfInstance (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Elab.DefView

def Lean.Elab.Command.mkDefViewOfOpaque (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Elab.DefView

def Lean.Elab.Command.mkDefViewOfExample (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.DefView

def Lean.Elab.Command.isDefLike (stx : Lean.Syntax) : Bool

def Lean.Elab.Command.mkDefView (modifiers : Lean.Elab.Modifiers) (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Lean.Elab.DefView