[Agda] --without-K option too restrictive?

Nils Anders Danielsson nad at cse.gu.se
Thu May 30 17:31:41 CEST 2013

On 2013-05-29 22:52, Andreas Abel wrote:
> The error comes from universe polymorphism: Agda complains about
> Level.zero not being pattern, although Level.zero is only visible in
> the debug printing -v tc.lhs.split.well-formed:20.

The --without-K check reconstructs constructor parameters, but this
information is not propagated to the pretty-printer.


More information about the Agda mailing list