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

[Nils Anders Danielsson]

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.

-- 
/NAD