Re: [isabelle] Eisbach: Method command: Documentation text

On Mon, 17 Aug 2015, Daniel Matichuk wrote:

There is currently no way to add documentation text to Eisbach methods. I don't think the feature is considered deprecated, it was just overlooked for the first release. I believe the canonical syntax for this is simply an optional string at the end of the declaration (e.g. named_theorems). I'll look into it.

I had a very brief look. There is a syntax problem that prevents to follow the canonical form: the method body consists of "args" without requiring delimeters. E.g. it is possible to define

  method a = rule refl

A post-fix description does not fit into that model: it is unclear where the method expression ends and the description starts.

Even a stricter method body that demands parentheses would render the syntax somewhat fragile, e.g. unclear errors with partial input.

I am unsure about the practical relevance of that. Descriptions are only available in rare situations, mainly historical accidents that were propagated from the original attribute and method concepts.


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