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

[Jean-Philippe Bernardy]

On Wed, Oct 13, 2010 at 2:33 AM, Dan Doel <dan.doel at gmail.com> wrote:

> Actually, I suspect the reason (and it's the best one) is eta expansion.

Another consequence of eta-expansion is that Agda can infer values of
type True;
it would not if True was defined using data.

Cheers,
JP.