Re: [isabelle] Problem with "additional type variables" in a definition
> I'm having a problem with Isabelle 2016 which I've minimised to the following file. There seems to be something particular in how Isabelle handles types appearing in a definition but not in any arguments to the thing being defined.
> theory Test
> definition foo :: "bool" ("f" 50) where
> "foo â âx :: 'a. True"
> abbreviation bar :: "bool" where
> "bar â foo"
> lemma "foo"
> The definition gives the output
> foo :: "bool"
> Additional type variable(s) in specification of "foo": âa
The problem is the implicit type âa in the definition of foo. To this end, Isabelle inserts a
dummy argument in the definition of foo of type (âa itself). So your definition becomes
definition foo' :: "'a itself â bool" where
"foo' _ â â x :: 'a. Trueâ
you also see this definition, if you perform a âprint_theoremsâ after your definition of âfooâ.
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and