On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg <e...@cis.upenn.edu> wrote:
> > > On Apr 8, 2013, at 3:12 PM, Paul Brauner <polux2...@gmail.com> wrote: > > > from the output of -ddump-splices I dont think it is the case but I'm > asking anyway: is there any way to deduce a ~ b from a :==: b? > > Not easily. You would have to write a (potentially recursive) function > that explicitly matches singleton constructors, similarly to what you > wrote. (You could say that this function is a (potentially inductive) proof > that the generated definition of :==: is correct.) Ok. > I agree that this is boilerplate and could easily be generated. I've added > it to the list of features to be included in the next version of > singletons. I'm surprised myself that it hasn't occurred to me to include > this before. > > Great! Paul > Richard > > >
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
