Hi Florian,
For a few number of constants it should be possible to write all
constants by hand. For a large number, I will see how feasible it is to
generate this list of constants, or find otherwise a simpler solution...
Cheers,
Frédéric
___
Hi Florian,
Between Isabelle 2014 and 2015, the option "open" appeared for the
command export_code, and by default the reflection minimizes the
exported code.
Would it be acceptable for code_reflect to also have a similar option
"open"?
As a draft example, here is a list of modifications
Dear all,
The following is a list with 2 elements:
definition "l = [let x = True in x, False]"
However after doing "export_code l in OCaml", we obtain a list with only
1 element, because at the end no parentheses are inserted around the
corresponding "let".
In particular by default in OCaml
Dear all,
During some programming tasks, I had to use the following functions:
BNF_FP_Def_Sugar.co_datatype_cmd
Classical.rule_tac
Metis_Tactic.metis_method
However they only appear inside their respective structures, would it be
possible to write their corresponding types in signatures, at
Hi,
During some programming tasks, I had to use the following functions:
BNF_FP_Def_Sugar.co_datatype_cmd
note that these *_cmd functions are merely supposed to be used when
declaring Isar commands; dervived Isabelle/ML code is always supposed to
work with proper internalized entities (types
