old vs new structure cmd: docs

Stream: general

[Johan Commelin]

Is there any documentation of old vs new structure cmd that one can link to?

[Johan Commelin]

I couldn't find the difference explained in TPIL.

[Sebastian Ullrich]

Do you know about https://github.com/leanprover/lean/wiki/Refactoring-structures? Not completely up to date though.

[Johan Commelin]

@Sebastian Ullrich I think I've seen it before. But thanks.

[Johan Commelin]

Otoh, that's not really what I had in mind. I would like an explanation that shows how structures work in Lean 3. Written for people that don't know Lean. (You may assume the reader knows type theory.)

[Kevin Buzzard]

All I know is that old_structure_cmd should really be called other_structure_cmd (it's not deprecated, just historically an older idea)