Documentation

Lean.Elab.MutualDef

DefView plus header elaboration data and snapshot.

Instances For
    Equations
    @[reducible, inline]

    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
            @[reducible, inline]

            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