Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. computation preprocessing rules to allow literals as input for computations
  2. dedicated preprocessor for computations
  3. extended syntax allows to include datatype constructors directly in computations
  4. variables and type must be checked before entering evaluation sandwich
  5. more explicit errors in pathological cases
  6. more computation antiquotations
  7. computations and partiality
  8. tuned
Changeset 64994:6e4c05e8edbb by haftmann:
computation preprocessing rules to allow literals as input for computations
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/String.thy (diff)
Changeset 64993:4fb84597ec5a by haftmann:
dedicated preprocessor for computations
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64992:41e2c3617582 by haftmann:
extended syntax allows to include datatype constructors directly in computations
The file was modified src/HOL/ex/Computations.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64991:d2c79b16e133 by haftmann:
variables and type must be checked before entering evaluation sandwich
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64990:c6a7de505796 by haftmann:
more explicit errors in pathological cases
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64989:40c36a4aee1f by haftmann:
more computation antiquotations
The file was modified src/HOL/ex/Computations.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64988:93aaff2b0ae0 by haftmann:
computations and partiality
The file was modified src/HOL/ex/Computations.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 64987:1985502518ce by haftmann:
tuned
The file was modified src/HOL/ex/Computations.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)