• Stores whether this is the header of a definition, theorem, ...

  • shortDeclName : Lake.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 : Lake.Name

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

  • levelNames : List Lake.Name

    Universe level parameter names explicitly provided by the user.

  • binderIds : Array Lean.Syntax

    Syntax objects for the binders occurring befor :, 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.

  • valueStx : Lean.Syntax

    Syntax object the body/value of the definition.

DefView after elaborating the header.

Instances For
    @[inline, reducible]

    A mapping from FVarId to Set of FVarIds.

    Instances For

      The let-recs may invoke each other. Example:

      let rec
        f (x : Nat) := g x + y
        g : NatNat
          | 0   => 1
          | x+1 => f x + z

      y is free variable in f, and z is a free variable in g. To close f and g, y and z must be in the closure of both. That is, we need to generate the top-level definitions.

      def f (y z x : Nat) := g y z x + y
      def g (y z : Nat) : NatNat
        | 0 => 1
        | x+1 => f y z x + z
      @[inline, reducible]
      Instances For
        @[inline, reducible]
        Instances For
          Instances For
            Instances For
              @[inline, reducible]

              Mapping from FVarId of mutually recursive functions being defined to "closure" expression.

              Instances For
                • sectionVars: The section variables used in the mutual block.
                • mainHeaders: The elaborated header of the top-level definitions being defined by the mutual block.
                • mainFVars: The auxiliary variables used to represent the top-level definitions being defined by the mutual block.
                • mainVals: The elaborated value for the top-level definitions
                • letRecsToLift: The let-rec's definitions that need to be lifted
                Instances For