## Stream: general

### Topic: eta for records

#### Johan Commelin (Jan 09 2019 at 07:16):

(: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 (Jan 09 2019 at 08:08):

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 (Jan 09 2019 at 08:11):

Pros:

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


#### Sebastian Ullrich (Jan 09 2019 at 08:11):

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

Last updated: May 09 2021 at 19:11 UTC