[isabelle] termination: Low-Level Exception, Last Function Definition
Two observations related to the termination command:
1) First, "termination foo" raises exception Option (line 81 of
"General/basics.ML") if foo is not a valid function name. A
user-digestible error message might be preferable.
2) Second, according to the Tutorial on Function Definitions, the
termination command "implicitly refers to the last function
definition." But consider this snippet:
locale l = ...
function (in l) ...
Perhaps it could be mentioned in the Tutorial that "last" is
context-dependent? (In fact, wonder if this feature might not be a bit
too obscure. Without having studied real-world usage, my gut feeling is
that the termination command should either directly follow function,
i.e., they should be parsed as a unit, or -- if it stands separately --
require the name of the function whose termination is proved.)
Ceterum censeo: Isabelle needs an issue tracker.
This archive was generated by a fusion of
Pipermail (Mailman edition) and