Re: [isabelle] Auxiliary context in class target

Hi Andreas,

> I am having trouble to use Isabelle's new auxiliary contexts inside a
> class context, as in the following example:
> context ord begin
> context fixes x :: 'a begin
> definition bar where "bar = x"
> The definition is rejected because x is erroneously identified as a free
> variable:
> *** Extra variables on rhs: "x"
> *** The error(s) above occurred in definition
> "ord_class.ord_class.bar_dict":
> ***   "bar == x"
> *** At command "definition"
> The same error occurs when I use fun with a more complicated function.
> I would like to use such a context to emulate the "for" clause of
> inductive for function defintions, because the induction rule generated
> by fun is nicer.
> Is this just not yet implemented or am I again abusing things here?

this is indeed a current restriction in the class target; it expects all
occuring auxiliary parameters to be class parameters, which is a very
strong assumption.  I am currently testing a patch
( which is
supposed to lift this restriction.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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