<html><head><meta http-equiv="Content-Type" content="text/html charset=iso-8859-1"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">great! is there a way to explain what the restriction is? Has Coq fixed this bug yet, and if so, how does your solution compare to theirs?<div><br></div><div>-Dan</div><div><br><div><div>On Jun 27, 2014, at 12:26 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><meta http-equiv="Content-Type" content="text/html; charset=utf-8"><div dir="ltr"><div>Yes, this restriction is to address the incompatibility of the termination checker with univalence. As a side-effect, many functions on universes no longer pass the termination check, for example (by Andreas):<br>
<pre>T : Bool -> Set
T true = Nat
T false = List Nat
f : (x : Bool) -> T x -> Set
f true zero = Nat
f true (suc x) = f true x
f false nil = Nat
f false (x :: xs) = f false xs</pre></div>For the moment, such definitions have to be unfolded manually:<br><pre>f : (x : Bool) -> T x -> Set
f true = ftrue
where
ftrue : Nat -> Set
ftrue zero = Nat
ftrue (suc x) = ftrue x
f false = ffalse
where
ffalse : List Nat -> Set
ffalse nil = Nat
ffalse (x :: xs) = ffalse xs</pre><div><div>However, due to a mistake I made in the fix, the termination checker a complains much more than necessary when --without-K is enabled. This has now been fixed in the development version: <a href="https://code.google.com/p/agda/issues/detail?id=1214&can=1">https://code.google.com/p/agda/issues/detail?id=1214&can=1</a>. I'll check the other errors in Nils' library later. If you have any specific examples that you think should be accepted, please send them to me and I'll see what I can do.<br>
<br></div><div>Jesper<br></div></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jun 27, 2014 at 6:52 AM, Dan Licata <span dir="ltr"><<a href="mailto:dlicata@wesleyan.edu" target="_blank">dlicata@wesleyan.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">Is this restriction addressing the "termination checker + propositional univalence inconsistency" issue, or something else?<span class="HOEnZb"><font color="#888888"><div>
<br></div><div>-Dan</div></font></span><div><div class="h5"><br><div><div>On Jun 21, 2014, at 1:44 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:</div><br><blockquote type="cite">
<div dir="ltr"><div><div><div><div>I suppose by 'people working on this issue', you mean Andreas and me? I'm not currently working on this problem, but I could be convinced to if the current hack turns out to be too inconvenient. However, I have two problems before I can start working on a fix:<br>
<br></div>- The current theory of pattern matching doesn't allow induction on 'deep' arguments, i.e. ones that only get an inductive type after pattern matching on some other arguments. So the theory would have to be extended.<br>
<br></div>- I don't have a lot of experience with the termination checker, so I'm not confident to mess with it. It seems that in order to fix this problem, the termination checker would need some type information, as well as information about the substitutions performed by the previous case splits.<br>
<br></div>If anyone can help me with (one of) these problems, I'd like to work together on it. Otherwise I'll try to get a better understanding by myself, but then it might take a long time.<br><br></div>Jesper<br>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote"><div>On 20 June 2014 09:07, Brent Yorgey <span dir="ltr"><<a href="mailto:byorgey@seas.upenn.edu" target="_blank">byorgey@seas.upenn.edu</a>></span> wrote:<br>
</div><div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow:hidden">but is the code I linked now expected to<br>
fail termination checking?</div></blockquote></div></div><br>Using the --without-K option? I don't know. This is an open issue and<br>people working on this issue know that the current behaviour is too<br>restrictive. I don't know if they are working in a better solution<br>
right now.<span><font color="#888888"><br><br>-- <br><div dir="ltr">Andrés<br></div>
</font></span></div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div></div></div></blockquote></div><br></div>
</blockquote></div><br></div></body></html>