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 constant?

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 like

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

Two many features, too many layers ...


	Makarius





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