[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Thorsten Altenkirch]

On 15 Oct 2010, at 14:15, Nicolas Pouillard wrote:

> elim-EmptyRec : ∀ {A : Set} → EmptyRec → A
> elim-EmptyRec x = ?

Good point. What about

record EmptyRec : Set where
 constructor blub
 field
   bla : EmptyRec

elim-EmptyRec : ∀ {A : Set} → EmptyRec → A
elim-EmptyRec (blub y) = elim-EmptyRec y

somehow one would think that

elim-EmptyRec y = elim-EmptyRec (EmptyRec.bla y)

should work, but I think this can destroy normalisation.

Thorsten