<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 19 June 2014 11:24, Brent Yorgey <span dir="ltr">&lt;<a href="mailto:byorgey@seas.upenn.edu" target="_blank">byorgey@seas.upenn.edu</a>&gt;</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>