Bruno,
Now we modify thin to take an extra Nat n (not needed, but just to show the duality with thickening):
I'm puzzled by the "not needed" bit. Isn't the introduction of Fin's indices reflected as values in the GADT , and the fact that the GADT makes that reflection, what makes it work? P. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
