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

[Nicolas Pouillard]

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

I mean, the darcs version.

However, here is a again the dumb trick of the Box data type:

  data Box (A : Set) : Set where
    box : A → Box A

  record EmptyRecBox : Set where
    constructor blub
    field
      bla : Box EmptyRecBox

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

This version is accepted by the same version of Agda. Moreover 
I don't see any issue with η-expansion with this version.

BTW in another email you mentioned using ∞, did you meant:

  record NotMuchEmptyRec : Set where
    constructor blub
    field
      bla : ∞ NotMuchEmptyRec

I hope not, because this one is not empty:

  notMuchEmptyRec : NotMuchEmptyRec
  notMuchEmptyRec = blub (♯ notMuchEmptyRec)

Regards,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr