[Agda] A different implementation of --without-K

Nils Anders Danielsson nad at cse.gu.se
Mon Dec 2 11:46:23 CET 2013

On 2013-11-30 10:34, Andreas Abel wrote:
> On 29.11.2013 20:40, Jason Gross wrote:
>> Is there a computable/decidable/syntactic (and also complete)
>> characterization of what's provable with J but not K?  (Alternatively,
>> is there an algorithm for transforming proofs using K into proofs using
>> only J whenever they exist?)
> Not that I know of.  [Maybe there is one in one of the drawers of
> Conor's desk...]  I guess this is what Jesper Cockx and Pierre
> Boutillier are working on.

I would like to know if Conor's translation of pattern matching, which
relies on K, could be modified so that it supports fewer patterns but
doesn't require K.


More information about the Agda mailing list