Re: [isabelle] add_assoc, add.assoc and reflection

Thank you for the explanations

Name spaces are strictly separate for each "kind" of things. The syntax is usually done in a way that the distinction of kinds is clear from how the text is written. E.g. fact expressions refer to attributes and theorems in a certain way, and cannot be mistaken as terms, for example.


So I suppose the answer to your question is: theorem names /can/ occur in inner syntax, but then they do not refer to theorems;

while with respect to the following

The main meta-problem on this thread might be actually an expectation of something complicated, but the situation is quite plain and simple. And after decades of reforms of the system implementation it should all work out smoothly, including arbitrary nesting of languages.

some smoothness is lost in case one uses Isabelle not anticipated by design, for instance Lucas-Interpretation [1]: Here programs [2] contain theorem names, which are turned into theorems by functions available in Isabelle; this now requires additional conversion [3].

So thanks a lot for all the replies -- they tell us about prospects on Eisbach.


[2] We plan to employ Isabelle's function package for that purpose.

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