### 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.

### License

BSD License

### Topics

- Tools

### Session Lazy_Case

- Lazy_Case
- Test_Lazy_Case

### Used by

- Dictionary Construction

## Cite

×

Lazy_Case-AFP

    @article{Lazy_Case-AFP,
      author  = {Lars Hupel},
      title   = {Lazifying case constants},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Lazy_Case.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Apr 20, 2017 : Isabelle2016-1