[Agda] another possible without-K problem

Dan Licata drl at cs.cmu.edu
Wed Jul 10 16:54:45 CEST 2013

Also, related to implementing higher inductives, but not to without-K: 
is there a way to turn off/defeat the unused arguments analysis that is
new in  It breaks some of the things I'm doing: I want a
function with a "phantom" parameter, where different values of the
phantom parameter do not automatically get equated.  


More information about the Agda mailing list