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

[Thorsten Altenkirch]

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

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

What is the HEAD version of Agda?

> 
> -- 
> Nicolas Pouillard
> http://nicolaspouillard.fr