Re: [isabelle] Problems with multiple patterns in simproc_setup

Dear Makarius,

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?

I would argue that this is very much /not/ what it is supposed to do and
that every pattern should fix variables and be type-checked
independently. The patterns are independent of one another – why should
they have a shared name space?

What is your opinion?


On 25/10/2019 10:49, Makarius wrote:
> On 24/10/2019 13:59, Christoph Madlener wrote:
>> Ok, thank you all for your replies. I see what is happening now. I'm
>> just asking myself if this behavior is intended or "just came to be"?
>> What I can say though is that it obviously wasn't the behavior I was
>> expecting and as far as I can tell it is also not documented (although I'm
>> also not sure what a good place for this information would be).
> Type inference is very useful, but there are sometimes situations where
> users get confused (very rarely). Luckily this is a non-issue today with
> the Isabelle Prover IDE: CTRL-hover tells you about inferred types.
> These are the traditional guidelines to isolate problems in
> specifications and implementations.
>   If something does not work unexpectedly:
>     (a) Inferred types might be more general or more special than expected.
>     (b) The context might be wrong.
> The latter refers to type Proof.context in Isabelle/ML.
> 	Makarius

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