eta for records

Stream: general

[Johan Commelin]

(:warning: I'm a mathematician who is about to use some terminology he doesn't understand.)
What are the pros and cons of eta for records? Why does Lean not have eta for records?

[Gabriel Ebner]

Why does Lean not have eta for records?

Because records (structure) in Lean are just inductives with a single (non-recursive) constructor. And we don't have η for inductives either (I'm pretty sure that causes type-checking to be undecidable).

[Gabriel Ebner]

Pros:

example (p : ℕ × ℕ) : p = (p.1, p.2) := rfl
example (C) [𝓒 : category C] := opposite (opposite 𝓒) = 𝓒 := rfl

[Sebastian Ullrich]

Agda has (opt-out) eta for inductive, non-recursive records. Which at least terminates, but may still slow down unification.