[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) ...
  termination ...

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

Best regards,

Ceterum censeo: Isabelle needs an issue tracker.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.