<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>_<_ : ℕ → ℕ → Bool<br>x < zero = false<br>zero < suc _ = true<br>suc x < suc y = x < y<br><br>f : List ℕ → List ℕ → List ℕ<br>f (x ∷ xs) (y ∷ ys) with x < 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 'with', but that there is something else wrong with your recursive calls. Maybe if you send us your complete definition of 'fun', 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"><<a href="mailto:jan.stolarek@p.lodz.pl" target="_blank">jan.stolarek@p.lodz.pl</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm new to Agda and I'm having a problem which might seem rather basic. Let's say I have defined<br>
Nat, Bool, List, if_then_else_ and < operator that takes two Nats and returns true or false. Now<br>
I have something like this:<br>
<br>
fun : List Nat -> List Nat -> List Nat<br>
fun (x :: xs) (y :: ys) with x < 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 < 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't<br>
understand why the same code works perfectly with if-then-else but doesn't work with "with"<br>
construct. How can I use "with" 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>