<div dir="ltr">Thank you!</div><div class="gmail_extra"><br><div class="gmail_quote">2015-05-31 21:39 GMT+08:00 Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks for reporting this issue. I fixed the problem:<br>
<br>
<a href="https://code.google.com/p/agda/issues/detail?id=1530" target="_blank">https://code.google.com/p/agda/issues/detail?id=1530</a><div class="HOEnZb"><div class="h5"><br>
<br>
On 30.05.2015 17:15, Bruno Bianchi wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;padding-left:1ex;border-left-color:rgb(204,204,204);border-left-width:1px;border-left-style:solid">
Hi,<br>
I'm trying to compile the following two modules in 2.4.2.3, but for some<br>
reason the second one does not pass the termination checker due to the<br>
recursive call in olist-sorted. If I include the content of the first<br>
module instead of importing it, then it does pass the termination<br>
checker. If I remove the parameters from both modules and I postulate<br>
them in a third one (which would be imported by both modules), then I'm<br>
also able to pass the termination checker.<br>
Is there any way to make such parameterized modules pass the termination<br>
checker in 2.4.2.3? It used to work in 2.3.2.2.<br>
Thanks in advance,<br>
Bruno<br>
Bound.agda<br>
----------------<br>
module Bound {A : Set}(_<=_ : A -> A -> Set) where<br>
data Bound : Set where<br>
bot : Bound<br>
val : A -> Bound<br>
data LeB : Bound -> Bound -> Set where<br>
lebx : {b : Bound} -> LeB bot b<br>
lexy : {a b : A} -> a <= b -> LeB (val a) (val b)<br>
OList.agda<br>
---------------<br>
module OList {A : Set}(_<=_ : A -> A -> Set) where<br>
open import Data.List<br>
open import Bound _<=_<br>
data OList : Bound -> Set where<br>
nil : {b : Bound} -> OList b<br>
cons : {b : Bound}{x : A} -> LeB b (val x) -> OList (val x) -> OList b<br>
forget : {b : Bound} -> OList b -> List A<br>
forget nil = []<br>
forget (cons {x = x} _ xs) = x :: forget xs<br>
data Sorted : List A -> Set where<br>
empty : Sorted []<br>
single : (x : A) -> Sorted (x :: [])<br>
step : {x y : A}{ys : List A} -> x <= y -> Sorted (y :: ys) -> Sorted<br>
(x :: y :: ys)<br>
olist-sorted : {b : Bound}(xs : OList b) -> Sorted (forget xs)<br>
olist-sorted nil = empty<br>
olist-sorted (cons {x = x} _ nil) = single x<br>
olist-sorted (cons b<=x (cons (lexy x<=y) ys)) = step x<=y (olist-sorted<br>
(cons (lexy x<=y) ys))<br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</font></span></blockquote></div><br></div>