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

Equations

• Lean.Elab.instInhabitedDefKind = { default := Lean.Elab.DefKind.def }

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

Equations

• Lean.Elab.instBEqDefKind = { beq := Lean.Elab.beqDefKind✝ }

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

Equations

• Lean.Elab.DefKind.isTheorem x = match x with | Lean.Elab.DefKind.theorem => true | x => false

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

Equations

• Lean.Elab.DefKind.isDefOrAbbrevOrOpaque x = match x with | Lean.Elab.DefKind.def => true | Lean.Elab.DefKind.opaque => true | Lean.Elab.DefKind.abbrev => true | x => false

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

Equations

• Lean.Elab.DefKind.isExample x = match x with | Lean.Elab.DefKind.example => true | x => false

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

Equations

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

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

Equations

• Lean.Elab.DefView.isInstance view = Array.any view.modifiers.attrs (fun attr => attr.name == `instance) 0 (Array.size view.modifiers.attrs)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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