[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