Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Deriving generic class instance...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:46):

From: Gerwin.Klein@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

view this post on Zulip Email Gateway (Aug 22 2022 at 18:46):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
So, what is the difference between Generic_Deriving and Deriving?

view this post on Zulip Email Gateway (Aug 22 2022 at 18:47):

From: Johannes Hölzl <johannes.hoelzl@gmx.de>
Okay, Jasmin showed me the paragraph on the website...


Last updated: Apr 24 2024 at 08:20 UTC