<br><br><div class="gmail_quote">On Sun, Jan 9, 2011 at 2:21 PM, 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;">

Am Samstag, den 08.01.2011, 12:42 -0500 schrieb Andrés Sicard-Ramírez:<br>
&gt; Hi Wolfgang,<br>
<div class="im">&gt;<br>
&gt; On Sat, Jan 8, 2011 at 11:47 AM, Wolfgang Jeltsch wrote:<br>
&gt;<br>
&gt;            map : ∀ {A A&#39; ℓ} → (A → A&#39;) → List A ℓ → List A&#39; ℓ<br>
&gt;            map f xs = {!-c!}<br>
&gt;<br>
&gt; It worked for me (on the development version of Agda) .<br>
&gt;<br>
&gt; Best,<br>
&gt; Andrés<br>
<br>
</div>Is it expected to also work with 2.2.6?<br>
<div><div></div><div class="h5"><br></div></div></blockquote><div><br>No. The auto command was added to Agda 2.2.8<br>
<br>
<a href="http://code.haskell.org/Agda/doc/release-notes/2-2-8.txt">http://code.haskell.org/Agda/doc/release-notes/2-2-8.txt</a><br>
<br>
(I have updated the Wiki with this information)<br> <br clear="all"></div></div>Best,<br><br>-- <br>Andrés<br>