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