On 1/8/07, Roberto Zunino <zunino at di.unipi.it> wrote: > Does anyone else believe that using strictess annotations in GADT proof > terms would be good style? I think Tim Sheard uses strictness in his Omega project for the same reason you suggest. See http://web.cecs.pdx.edu/~sheard/ Jim