Zulip Chat Archive

Stream: general

Topic: eta for records


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Gabriel Ebner (Jan 09 2019 at 08:11):

Pros:

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

view this post on Zulip 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