Re: [isabelle] Problem with "additional type variables" in a definition



Dear Lars-Henrik,

> 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
>  imports
>    HOL
>  begin
> 
>  definition foo :: "bool" ("f" 50) where
>    "foo â âx :: 'a. True"
> 
>  abbreviation bar :: "bool" where
>    "bar â foo"
> 
>  lemma "foo"
>    sorry
>  end
> 
> The definition gives the output
> 
>  consts
>    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,
RenÃ


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