Re: [isabelle] TYPE_MATCH exception with adhoc_overloading
Thanks for the report, I'll have a look. First an immediate observation:
When adding the following to Scratch.thy
fix f :: "('b ⇒ 'b ⇒ 'a) stream"
and x :: "'b stream"
term "pure id :: ('b => 'b) stream"
the first "term" results in
:: "('c ⇒ 'c) stream"
while the second results in
:: "('b ⇒ 'b) stream"
So it is not surprising that the first causes problems while matching.
Why, however "'c" is produced instead of "'b" is not immediately clear
to me. I'll investigate.
On 11/21/2014 04:09 PM, Andreas Lochbihler wrote:
Dear experts on adhoc overloading,
When I want to instantiate variables in a theorem using the attribute
"of", sometimes the exception TYPE_MATCH gets raised. This seems strange
to me because I would expect that adhoc_overloading either complains
about not being able to uniquely resolve an overloaded constant or
exchanges the constant in the AST.
By adding more type annotations, I have so far been able to circumvent
the exception, but there seems to be a check missing. Attached you find
a small example.
This archive was generated by a fusion of
Pipermail (Mailman edition) and