[Agda] Type and termination checking around with clauses

[Anton Setzer]

Peter Berry wrote:
> 2008/4/30 Ulf Norell <ulfn at cs.chalmers.se>:
>   
>> A possible work around might be to include the recursive calls in the with
>> clause (untested):
>>
>>  merge (x :: xs) (y :: ys) with x <= y | merge xs (y :: ys) | merge (x ::
>> xs) ys
>>  ... | true   | rec | _ = x :: rec
>>  ... | false | _ | rec = y :: rec
>>
>> This isn't very nice, but at least it should make the termination checker
>> happy. Of course, in this particular case an if_then_else_ would also work.
>>     
>
> Aha, I didn't know you could do that. And yes, doh, if_then_else_
> makes perfect sense.
>
>   

It sounds to me odd that this solution is accepted, but the direct solution
is not accepted.
It shouldn't make any difference whether I make a recursive call
to merge using a with clause or whether I use it directly.


Anton

-- 
---------------------------------------
Anton Setzer
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
UK

Telephone:
(national)        (01792) 513368
(international) +44 1792  513368
Fax:
(national)        (01792) 295708
(international) +44 1792  295708
Visiting address:
Faraday Building,
Computer Science Dept.
2nd floor, room 211.
Email: a.g.setzer at swan.ac.uk
WWW:
http://www.cs.swan.ac.uk/~csetzer/
---------------------------------------
 
                    
  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080430/f02c032e/attachment-0001.html