<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 19 June 2014 11:24, Brent Yorgey <span dir="ltr"><<a href="mailto:byorgey@seas.upenn.edu" target="_blank">byorgey@seas.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div id=":1ky" class="" style="overflow:hidden">I just upgraded to Agda 2.4.0.1 and now compiling the library generates the error<br>
<br></div></blockquote><div><br>Please note that Agda 2.4.0.1 is an unreleased version (but I know it<br>is in Hackage).<br> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div id=":1ky" class="" style="overflow:hidden">
Termination checking failed for the following functions:<br>
Decision-procedures.List.Dec._≟_<br>
Problematic calls:<br>
((x ∷ xs) ≟ (y ∷ ys)) (x ≟A₁ y)<br>
(at /home/brent/src/equality/Equality/Decision-procedures.agda:238,14-15)<br>
when scope checking the declaration<br>
import Equality.Decision-procedures as .#Equality.Decision-procedures-131098778<br>
</div></blockquote></div></div><div class="gmail_extra"><br></div><div class="gmail_extra">It is due to a change on the behaviour of the termination-checker when using the --without-K option (by removing this option, the function is accepted).<br>
</div><div class="gmail_extra"></div><br><div class="gmail_extra">-- <br><div dir="ltr">Andrés<br></div>
</div></div>