Haskell's Show Class in Isabelle/HOL

Christian Sternagel 📧 and René Thiemann 🌐

July 29, 2014


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)


April 12, 2024
Added show-class based on string literals, added parsers for nat and int, added injectivity proofs.
April 10, 2015
Moved development for old-style datatypes into subdirectory "Old_Datatype".
March 11, 2015
Adapted development to new-style (BNF-based) datatypes.


Session Show

Session Old_Datatype_Show