[Agda] list equality decision procedure fails termination check with Agda 2.4.0.1?

[Dan Licata]

Is this restriction addressing the "termination checker + propositional univalence inconsistency" issue, or something else?

-Dan

On Jun 21, 2014, at 1:44 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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:
> 
> - 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.
> 
> - 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.
> 
> 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.
> 
> Jesper
> 
> 
> On Fri, Jun 20, 2014 at 7:13 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> 
> On 20 June 2014 09:07, Brent Yorgey <byorgey at seas.upenn.edu> wrote:
> but is the code I linked now expected to
> fail termination checking?
> 
> Using the --without-K option? I don't know. This is an open issue and
> people working on this issue know that the current behaviour is too
> restrictive. I don't know if they are working in a better solution
> right now.
> 
> -- 
> Andrés
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140627/c941e5fc/attachment.html