Closed
Description
consider the following program
open import Level
open import Relation.Binary.PropositionalEquality
record single : Set (suc 0ℓ) where
-- eta-equality needs to enable to make the following proof work
field
A : Set
pack : single
pack = record { A = A }
lem : (x : single) → x ≡ single.pack x
lem x = {!refl!}to make the proof to work, either
- turn on
eta-equalityin the definition ofsingle, or - case split on
x.
however, the doc seems to indicate that eta-equality is on by default. so why this program doesn't work? is this a bug or just some subtlety?