[Agda] Termination problems with "with" and recursion

[Jesper Cockx]

Welcome to the Agda mailing list!

The following code typechecks for me (with no highlighting):

open import Data.Nat using (ℕ; zero; suc)
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.List using (List; []; _∷_)

_<_ : ℕ → ℕ → Bool
x < zero = false
zero < suc _ = true
suc x < suc y = x < y

f : List ℕ → List ℕ → List ℕ
f (x ∷ xs) (y ∷ ys) with x < y
f (x ∷ xs) (y ∷ ys) | true = x ∷ f xs ys
f (x ∷ xs) (y ∷ ys) | false = y ∷ f xs ys
f _ _ = []

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?

Jesper


On Wed, Oct 30, 2013 at 10:45 AM, Jan Stolarek <jan.stolarek at p.lodz.pl>wrote:

> I'm new to Agda and I'm having a problem which might seem rather basic.
> Let's say I have defined
> Nat, Bool, List, if_then_else_ and < operator that takes two Nats and
> returns true or false. Now
> I have something like this:
>
> fun : List Nat -> List Nat -> List Nat
> fun (x :: xs) (y :: ys) with x < y
> fun (x :: xs) (y :: ys) | true  = ... (recursive call to fun)
> fun (x :: xs) (y :: ys) | false = ... (recursive call to fun)
>
> When I C-c C-l this code then name of the function in type signature as
> well as names of recursive
> calls are highlighted by Agda. No error is reported, just highlighting. If
> I however write
> something like this:
>
> fun (x :: xs) (y :: ys) =
>     if x < y
>     then ... (recursive call to fun)
>     else ... (recursive call to fun)
>
> then all works fine. According to Agda wiki this is related to termination
> checking, but I don't
> understand why the same code works perfectly with if-then-else but doesn't
> work with "with"
> construct. How can I use "with" and recursive calls together so that
> termination checker does not
> complain?
>
> Janek
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131030/ac98d69c/attachment.html