Abstract
Isabelle's code generator performs various adaptations for target
languages. Among others, case statements are printed as match
expressions. Internally, this is a sophisticated procedure, because in
HOL, case statements are represented as nested calls to the case
combinators as generated by the datatype package. Furthermore, the
procedure relies on laziness of match expressions in the target
language, i.e., that branches guarded by patterns that fail to match
are not evaluated. Similarly, if-then-else is
printed to the corresponding construct in the target language. This
entry provides tooling to replace these special cases in the code
generator by ignoring these target language features, instead printing
case expressions and if-then-else as functions.