Re: [isabelle] How do I retrieve the mixfix syntax of a constant?
On Fri, 26 Mar 2010, Rafal Kolanski wrote:
Purely out of interest, do you know how one can get the syn_ext for a
I do not know of a proper way. There is a conceptual problem here, since
there is not "the" syntax for a constant. If the user writes something
definition c (mixfix) where "c = t"
then there is along way down to the internal syntax data structures. And
it is hard to interpret these later, and even harder to recover a
high-level notation declaration from that.
Also note that users could have there own notation/no_notation
declarations apart from that. The whole thing is subject to local
contexts and interpretations. The print mode is another degree of freedom
Two many features, too many layers ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and