Documentation

Lean.Elab.DefView

inductive Lean.Elab.DefKind:

Type

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 := [anonymous] }

def Lean.Elab.DefKind.isTheorem:

Lean.Elab.DefKind → Bool

Equations

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

def Lean.Elab.DefKind.isDefOrAbbrevOrOpaque:

Lean.Elab.DefKind → Bool

Equations

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

def Lean.Elab.DefKind.isExample:

Lean.Elab.DefKind → Bool

Equations

Lean.Elab.DefKind.isExample _fun_discr = match _fun_discr 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.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 Lean.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 Lean.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) :

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.