Documentation

Lean.Elab.StructInst

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

    Expand field abbreviations. Example: { x, y := 0 } expands to { x := x, y := 0 }

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Equations
        Equations
        • Lean.Elab.Term.StructInst.instInhabitedField = { default := { ref := default, lhs := default, val := default, expr? := default } }
        Equations
        Instances For
          Instances For

            true iff all fields of the given structure are marked as default

            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
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            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
                                  • allStructNames : Array Lake.Name
                                  • maxDistance : Nat

                                    Consider the following example:

                                    structure A where
                                      x : Nat := 1
                                    
                                    structure B extends A where
                                      y : Nat := x + 1
                                      x := y + 1
                                    
                                    structure C extends B where
                                      z : Nat := 2*y
                                      x := z + 3
                                    

                                    And we are trying to elaborate a structure instance for C. There are default values for x at A, B, and C. We say the default value at C has distance 0, the one at B distance 1, and the one at A distance 2. The field maxDistance specifies the maximum distance considered in a round of Default field computation. Remark: since C does not set a default value of y, the default value at B is at distance 0.

                                    The fixpoint for setting default values works in the following way.

                                    • Keep computing default values using maxDistance == 0.
                                    • We increase maxDistance whenever we failed to compute a new default value in a round.
                                    • If maxDistance > 0, then we interrupt a round as soon as we compute some default value. We use depth-first search.
                                    • We sign an error if no progress is made when maxDistance == structure hierarchy depth (2 in the example above).
                                  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
                                        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

                                              Reduce default value. It performs beta reduction and projections of the given structures.

                                              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