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".
GNU Lesser General Public License (LGPL)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".
Depends On
Used by
- MiniSail
- Modular_arithmetic_LLL_and_HNF_algorithms
- AI_Planning_Languages_Semantics
- CakeML_Codegen
- Monad_Memo_DP
- CakeML
- Dict_Construction
- Berlekamp_Zassenhaus
- Polynomial_Factorization
- Certification_Monads
- XML
- Affine_Arithmetic
- Real_Impl
- Polynomials