Hi Wolfgang,<br><br><div class="gmail_quote">On Sat, Jan 8, 2011 at 11:47 AM, Wolfgang Jeltsch <span dir="ltr">&lt;<a href="mailto:g9ks157k@acme.softbase.org">g9ks157k@acme.softbase.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

<br>
    map : ∀ {A A&#39; ℓ} → (A → A&#39;) → List A ℓ → List A&#39; ℓ<br>
    map f xs = {!-c!}<br>
<br></blockquote><div><br>It worked for me (on the development version of Agda) .<br clear="all"></div></div><br>Best,<br><br>-- <br>Andrés<br>