Email Gateway (Aug 22 2022 at 11:09): Email Gateway (Aug 22 2022 at 11:09):From: Peter Lammich <lammich@in.tum.de>
Hi,
In Isabelle, each method also comes with a short documentation text.
Is there a way to attach such a documentation text to methods defined
via Eisbach, or is the feature of having a short documentation text for
methods considered deprecated?
Email Gateway (Aug 22 2022 at 11:10):From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Hi Peter,
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.
Regards,
Dan
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 12:29):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Apr 23 2024 at 08:19 UTC