Re: [isabelle] Problems with multiple patterns in simproc_setup



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.