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 PullbackFunctor.agda:7,1-18 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