<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">&lt;<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>&gt;</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&#39;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&#39;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}(_&lt;=_ : A -&gt; A -&gt; Set) where<br>
data Bound : Set where<br>
   bot : Bound<br>
   val : A -&gt; Bound<br>
data LeB : Bound -&gt; Bound -&gt; Set where<br>
   lebx : {b : Bound} -&gt; LeB bot b<br>
   lexy : {a b : A} -&gt; a &lt;= b -&gt; LeB (val a) (val b)<br>
OList.agda<br>
---------------<br>
module OList {A : Set}(_&lt;=_ : A -&gt; A -&gt; Set) where<br>
open import Data.List<br>
open import Bound _&lt;=_<br>
data OList : Bound -&gt; Set where<br>
   nil : {b : Bound} -&gt; OList b<br>
   cons : {b : Bound}{x : A} -&gt; LeB b (val x) -&gt; OList (val x) -&gt; OList b<br>
forget : {b : Bound} -&gt; OList b -&gt; List A<br>
forget nil = []<br>
forget (cons {x = x} _ xs) = x :: forget xs<br>
data Sorted : List A -&gt; Set where<br>
   empty : Sorted []<br>
   single : (x : A) -&gt; Sorted (x :: [])<br>
   step : {x y : A}{ys : List A} -&gt; x &lt;= y -&gt; Sorted (y :: ys) -&gt; Sorted<br>
(x :: y :: ys)<br>
olist-sorted : {b : Bound}(xs : OList b) -&gt; Sorted (forget xs)<br>
olist-sorted nil = empty<br>
olist-sorted (cons {x = x} _ nil) = single x<br>
olist-sorted (cons b&lt;=x (cons (lexy x&lt;=y) ys)) = step x&lt;=y (olist-sorted<br>
(cons (lexy x&lt;=y) ys))<br>
</blockquote>
<br>
<br></div></div><span class="HOEnZb"><font color="#888888">
-- <br>
Andreas Abel  &lt;&gt;&lt;      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>