Documentation

Lean.Elab.MutualDef

DefView plus header elaboration data and snapshot.

Instances For
    Equations
    Equations
    Instances For
      @[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
                            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