[Agda] Induction when the argument is wrapped in a constructor?

[Nils Anders Danielsson]

On Wed, Mar 26, 2008 at 5:41 PM, Nils Anders Danielsson
<nils.anders.danielsson at gmail.com> wrote:
>
>  Note that this definition is rather inefficient, since the recursion
>  parameter "rec" above traverses the proofs. Perhaps one could hope
>  for the compiler to optimise away this inefficiency, though.

Indeed one can, as Conor informed me the other day. See "Inductive
Families Need Not Store Their Indices" (Brady, McBride, McKinna, TYPES
2003).

Note that this optimisation applies only to run-time execution (i.e.
execution in a closed context), not to evaluation during typechecking,
but this should suffice.

-- 
/NAD