diff options
| author | Thomas Bauereiss | 2017-12-14 16:21:14 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-12-14 17:08:46 +0000 |
| commit | 1c16fa04954387521ff8a21b68fb5bca3f27a29e (patch) | |
| tree | 8852befd27f6d453b198ddb449b091b2820cd29e /src/test/hello4 | |
| parent | 2ef7c31074720997bbc519e44e34c076677ab282 (diff) | |
Un-tuple function arguments when pretty-printing to Lem
This makes Lem prefer plain "definition" when generating Isabelle output for
functions, which is processed by Isabelle much faster than "fun"/"function"
definitions.
This change is not complete yet, because the Sail library functions still need
to be changed to not use tupled arguments (possibly as part of a bigger
refactoring of the library). For now, external functions are special-cased in
the pretty-printer and get tupled arguments.
Diffstat (limited to 'src/test/hello4')
0 files changed, 0 insertions, 0 deletions