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

[Nicolas Pouillard]

On Fri, 15 Oct 2010 14:28:17 +0200, Thorsten Altenkirch <txa at Cs.Nott.AC.UK> 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

With the HEAD version of Agda this is no longer accepted.

-- 
Nicolas Pouillard
http://nicolaspouillard.fr