Documentation

Lean.Elab.DefView

Header elaboration data of a DefView.

  • shortDeclName : Lean.Name

    Short name. Recall that all declarations in Lean 4 are potentially recursive. We use shortDeclName to refer to them at valueStx, and other declarations in the same mutual block.

  • declName : Lean.Name

    Full name for this declaration. This is the name that will be added to the Environment.

  • levelNames : List Lean.Name

    Universe level parameter names explicitly provided by the user.

  • binderIds : Array Lean.Syntax

    Syntax objects for the binders occurring before :, we use them to populate the InfoTree when elaborating valueStx.

  • numParams : Nat

    Number of parameters before :, it also includes auto-implicit parameters automatically added by Lean.

  • type : Lean.Expr

    Type including parameters.

Instances For

Snapshot after elaboration of a definition header.

Instances For

State before elaboration of a mutual definition.

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