Haskell's Show Class in Isabelle/HOL

Christian Sternagel 📧 and René Thiemann 📧

July 29, 2014

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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".
GNU Lesser General Public License (LGPL)

Change history

April 10, 2015

Moved development for old-style datatypes into subdirectory "Old_Datatype".

March 11, 2015

Adapted development to new-style (BNF-based) datatypes.


Theories of Show

Theories of Old_Datatype_Show