Ashley Yakeley wrote:
Have a look at these:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness
Ah, nice! It seems most we came up with is already in there. Even Any
which I use in my project but didn't
Martijn van Steenbergen wrote:
Ashley Yakeley wrote:
Have a look at these:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/witness
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/open-witness
Ah, nice! It seems most we came up with is already in there. Even Any
which I
Martijn van Steenbergen wrote:
Olá café,
With the recent generic programming work and influences from
type-dependent languages such as Agda, the following data type seems to
come up often:
data (a :=: a') where
Refl :: a :=: a
Everyone who needs it writes their own version; I'd like to
