<div dir="ltr"><div><div>Welcome to the Agda mailing list!<br><br></div>The following code typechecks for me (with no highlighting):<br><br><div style="margin-left:40px">open import Data.Nat using (ℕ; zero; suc)<br>open import Data.Bool using (Bool; true; false; if_then_else_)<br>

open import Data.List using (List; []; _∷_)<br><br>_&lt;_ : ℕ → ℕ → Bool<br>x &lt; zero = false<br>zero &lt; suc _ = true<br>suc x &lt; suc y = x &lt; y<br><br>f : List ℕ → List ℕ → List ℕ<br>f (x ∷ xs) (y ∷ ys) with x &lt; y<br>

f (x ∷ xs) (y ∷ ys) | true = x ∷ f xs ys<br>f (x ∷ xs) (y ∷ ys) | false = y ∷ f xs ys<br>f _ _ = []<br><br></div>so I guess your problem is not the fact that you use &#39;with&#39;, but that there is something else wrong with your recursive calls. Maybe if you send us your complete definition of &#39;fun&#39;, we can find out what is wrong?<br>

<br></div><div>Jesper<br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Wed, Oct 30, 2013 at 10:45 AM, Jan Stolarek <span dir="ltr">&lt;<a href="mailto:jan.stolarek@p.lodz.pl" target="_blank">jan.stolarek@p.lodz.pl</a>&gt;</span> wrote:<br>

<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I&#39;m new to Agda and I&#39;m having a problem which might seem rather basic. Let&#39;s say I have defined<br>
Nat, Bool, List, if_then_else_ and &lt; operator that takes two Nats and returns true or false. Now<br>
I have something like this:<br>
<br>
fun : List Nat -&gt; List Nat -&gt; List Nat<br>
fun (x :: xs) (y :: ys) with x &lt; y<br>
fun (x :: xs) (y :: ys) | true  = ... (recursive call to fun)<br>
fun (x :: xs) (y :: ys) | false = ... (recursive call to fun)<br>
<br>
When I C-c C-l this code then name of the function in type signature as well as names of recursive<br>
calls are highlighted by Agda. No error is reported, just highlighting. If I however write<br>
something like this:<br>
<br>
fun (x :: xs) (y :: ys) =<br>
    if x &lt; y<br>
    then ... (recursive call to fun)<br>
    else ... (recursive call to fun)<br>
<br>
then all works fine. According to Agda wiki this is related to termination checking, but I don&#39;t<br>
understand why the same code works perfectly with if-then-else but doesn&#39;t work with &quot;with&quot;<br>
construct. How can I use &quot;with&quot; and recursive calls together so that termination checker does not<br>
complain?<br>
<br>
Janek<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>