03f344a35f
Modifies the structure instance elaborator to
1. Fill in missing fields from sources in strict left-to-right order. In
`{a, b with}`, sometimes the elaborator
would ignore `a` even if both `a` and `b` provided the same field,
depending on what subobject fields they had.
2. Use the sources, or subobjects of the sources, to fill in entire
subobjects of the target structure as much as possible.
Currently, a field cannot be filled directly by a source itself
resulting in the term being eta expanded.
This change avoids this unnecessary and surprisingly costly extra eta
expansion.
Adds two new tests to illustrate the performance benefit (one courtesy
@semorrison). These are currently failing on master and succeed on this
branch.
There is one additional test to exercise the changes to the elaboration
of structure instances.
Changes to make mathlib build are in leanprover-community/mathlib4#9843
Closes #2451
12 lines
376 B
Text
12 lines
376 B
Text
def foo : A → B → B :=
|
|
fun a b => { x := a.x, y := b.y }
|
|
def boo : A → B → B :=
|
|
fun a b => { x := b.x, y := b.y }
|
|
def baz : A → B → C :=
|
|
fun a b => { toB := { x := a.x, y := b.y } }
|
|
def biz : A → B → C :=
|
|
fun a b => { toB := b }
|
|
def faz : A → C → C :=
|
|
fun a c => { toB := { x := a.x, y := c.toB.y } }
|
|
def fiz : A → C → C :=
|
|
fun a c => { toB := c.toB }
|