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

[Conor McBride]

On 15 Oct 2010, at 13:28, Thorsten Altenkirch wrote:

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

And drop eta, of course, otherwise that's

> somehow one would think that
>
> elim-EmptyRec y = elim-EmptyRec (EmptyRec.bla y)

in disguise.

>
> should work, but I think this can destroy normalisation.

Combining eta-expansion with strict constructor matching breaks
subject reduction.

Plus ça change

Conor