Documentation

Lean.Elab.StructInst

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

Instances For
    Instances For
      @[inline, reducible]
      Instances For

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

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

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