Re: [isabelle] typeclasses?



> If you find this behavior to be confusing, it is best to simply avoid
> using "==>" with "show". Just use "assumes" instead.

It is only confusing if you have multiple subgoals. With a single
subgoal ==> works fine and avoids some noise in case of inductions ---
otherwise the assume-show style is simpler.

Tobias

>> OK, skip goal 1. and try to solve goal 2.
>>
>>  fix x::var show "FV (tvar x) = {x}"
>>
>> *** Local statement will fail to refine any pending goal
>> *** Failed attempt to solve goal by exported rule:
>> ***   FV (tvar ?x3) = {?x3}
>> *** At command "show".
> 
> It looks like you need a type annotation here. Since "FV" and "tvar"
> are both overloaded constants, Isabelle can't tell what the return
> type of "tvar" should be. (Turn on "show consts" to see the inferred
> type; it probably introduces a new free type variable.) Try this
> instead:
> 
> fix x::var show "FV (tvar x :: trm) = {x}"
> 
> (Note to Isabelle developers: Introducing a new type variable in the
> middle of a proof like this is not something users usually do on
> purpose. Would it be possible to print a warning message when this
> happens?)
> 
> Hope this helps,
> - Brian





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