|
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: |
Datatype_Order_Generator, Deriving |
Used by: |
Affine_Arithmetic, Berlekamp_Zassenhaus, Certification_Monads, Dict_Construction, Formula_Derivatives, Monad_Memo_DP, Ordinary_Differential_Equations, 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.
|
|