structure cmd

Stream: mathlib4

[Daniel Selsam]

Leo implemented a solution to https://github.com/dselsam/mathport/issues/9, here is an example going all the way up to Field: https://github.com/leanprover/lean4/blob/master/tests/lean/diamond7.lean The generated coercions are much more compact than the ones in Lean3 and it could be a lot of faster. It would be great if someone could stress-test this (for the use-cases important to porting mathlib).

[David Renshaw]

So we don't even need to set a flag like set_option old_structure_cmd true?

[Daniel Selsam]

No, there is only one structure command now. If there are clashes/diamonds it looks for common ancestors rather than flattening everything like old_structure_cmd does in Lean3.

[Eric Wieser]

Presumably the effect is that the first parent is the "true" parent (such that derived_A.to_first_parent = derived_B.to_first_parent is true by refl) and the second parent is inserted as an automatic definition (such that derived_A.to_second_parent = derived_B.to_second_parent requires invoking a recursor)?

[Eric Wieser]

Hmm, that's not the discriminator I thought it was. There's some observable difference between first and second parents though, right?

[Mario Carneiro]

If you look at the constructor of the structure, the flattened parents will be passed as a bunch of fields instead of a structure argument

[Mario Carneiro]

it also has consequences for whether (foo.mk instA otherStuff).to_A = instA is defeq or not