Haskell's Show Class in Isabelle/HOL

Title:	Haskell's Show Class in Isabelle/HOL
Authors:	Christian Sternagel (c /dot/ sternagel /at/ gmail /dot/ com) and René Thiemann
Submission date:	2014-07-29
Abstract:	We implemented a type class for "to-string" functions, similar to Haskell's Show class. Moreover, we provide instantiations for Isabelle/HOL's standard types like bool, prod, sum, nats, ints, and rats. It is further possible, to automatically derive show functions for arbitrary user defined datatypes similar to Haskell's "deriving Show".
Change history:	[2015-03-11]: Adapted development to new-style (BNF-based) datatypes. [2015-04-10]: Moved development for old-style datatypes into subdirectory "Old_Datatype".
BibTeX:	@article{Show-AFP, author = {Christian Sternagel and René Thiemann}, title = {Haskell's Show Class in Isabelle/HOL}, journal = {Archive of Formal Proofs}, month = jul, year = 2014, note = {\url{http://isa-afp.org/entries/Show.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	GNU Lesser General Public License (LGPL)
Depends on:	Deriving
Used by:	Affine_Arithmetic, CakeML, CakeML_Codegen, Certification_Monads, Dict_Construction, Monad_Memo_DP, Polynomial_Factorization, Polynomials, Real_Impl, XML
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.