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".
License
History
- 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.
Topics
Session Show
Session Old_Datatype_Show
Used by
- Executable Multivariate Polynomials
- Ordinary Differential Equations
- Implementing field extensions of the form Q[sqrt(b)]
- Affine Arithmetic
- Certification Monads
- XML
- Derivatives of Logical Formulas
- Polynomial Factorization
- The Factorization Algorithm of Berlekamp and Zassenhaus
- Dictionary Construction
- First-Order Terms
- CakeML
- Monadification, Memoization and Dynamic Programming
- A Verified Code Generator from Isabelle/HOL to CakeML
- AI Planning Languages Semantics
- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- MiniSail - A kernel language for the ISA specification language SAIL
- LL(1) Parser Generator
- Difference Bound Matrices