Documentation

Lean.Elab.MutualDef

  • 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
    Equations
    • One or more equations did not get rendered due to their size.
    @[inline, reducible]

    A mapping from FVarId to Set of FVarIds.

    Equations
    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
      
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        Instances For
          Instances For
            @[inline, reducible]

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

            Equations
            Instances For
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        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
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For