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