When trying to compile a file using the syntax SlRefl {_ _ x} = refl {SlObj.arr x}, I get an impossible:

$ agda -i lib -i . PullbackFunctor.agda

src/full/Syntax/Translation/ConcreteToAbstract.hs:736: the
impossible happened

Replacing by SlRefl {_} {_} {x} = refl {SlObj.arr x} works fine. I'm not sure whether the first syntax is correct, but it should at least die more gracefully.

Page last modified on May 28, 2007, at 04:34 PM
Powered by PmWiki