Re: [isabelle] Problems with multiple patterns in simproc_setup

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.


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