My conclusion is that simproc_patterns are different enough from normal and from disjunctive patterns that there is no abstract argument that they should behave like either.
In the absence of a strong abstract argument, I would indeed leave things as they are.
Tobias On 25/10/2019 11:58, Makarius wrote:
On 25/10/2019 11:45, Manuel Eberl wrote:I don't really undestand what you're trying to say. The question at hand is: Is the behaviour of simproc_setup here (type checking all the different patterns simultaneously, in the same context) what it is supposed to do or not?The default answer: by default the behaviour of the system is correct and as intended. There can be nonetheless situations of user confusion: the system provides tools to work that out, notably for type-inference. 'simproc_setup' might be an odd corner case from the past -- I can't say on the spot, but 10min of inspecting of the sources and the history don't show any irregularities so far. Generally, it is a bad idea to change established behaviour on the spot, just because the true reasons for it are forgotten, or take a long time to investigate. The Isabelle jargon for that is "brownian motion": something could be done like this or like that, and there is no clear indication for either side. Adhoc changes would make it oscilate back and forth over time, and break other applications for no particular reason. Makarius
Description: S/MIME Cryptographic Signature