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):
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