Re: [isabelle] New AFP entry: Deriving generic class instances for datatypes



Okay, Jasmin showed me the paragraph on the website...

Am Mittwoch, den 21.11.2018, 10:18 +0100 schrieb Johannes Hölzl:
> So, what is the difference between Generic_Deriving and Deriving?
> 
>  - Johannes
> 
> Am Mittwoch, den 21.11.2018, 04:38 +0000 schrieb
> Gerwin.Klein at data61.csiro.au:
> > https://www.isa-afp.org/entries/Generic_Deriving.html
> > 
> > Deriving generic class instances for datatypes
> > Jonas Rädle and Lars Hupel
> > 
> > We provide a framework for automatically deriving instances for
> > generic type classes. Our approach is inspired by Haskell's
> > generic-
> > deriving package and Scala's shapelesslibrary. In addition to
> > generating the code for type class functions, we also attempt to
> > automatically prove type class laws for these instances. As of now,
> > however, some manual proofs are still required for recursive
> > datatypes.
> > 
> > 
> > Enjoy!
> > Gerwin
> 
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.