Reviving this old thread once more ;)
I think I need some clarifications first:
On 12/05/2013 05:05 PM, Florian Haftmann wrote:
Reviving this old thread, Peter and me found out what is actually going
on here.
Basically, nothing wrong. When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded. So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind. So, there is nothing wrong here.
Does that also mean that the resulting "unit itself" is as you would
expect in the following?
abbreviation
"abbr2 == do {
Some ();
Some False
}" -- "additional type variable"
Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode). @Christian. You might consider to adjust
your code accordingly after a second round of thinking about.
By "expanding adhoc overloading" do you mean replacing concrete
constants by overloaded generic ones?
When is Proof_Context.abbrev_mode actually true?
What I first thought was that I should avoid to insert overloaded (i.e.,
generic constants; cf. Adhoc_overloading.insert_overloaded) constants
whenever Proof_Context.abbrev_mode is true. But just trying this on some
examples did not change anything (as far as I can tell).
What's the concrete suggestion?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
