[isabelle-dev] types and locales
filali at irit.fr
Wed Mar 25 08:05:04 CET 2009
Makarius a écrit :
> On Tue, 24 Mar 2009, filali at irit.fr wrote:
>> I have a problem with types and locales: in the attached file
>> The attached file has been processed by the Isabelle snapshot of
> Looks like their is still a problem with implicitly fixed variables in
> locale expressions. It appears to work if you make the binding of
> "init" explicit in locale r1, using the 'for' in postfix notation:
> locale r1 =
> r0 "init :: 'buffer => ('buffer \<times> 'value) set => 'value" for
> + fixes d2i :: "('buffer \<times> 'buffer) => 'buffer"
Actually it does work now.
May be a corresponding example and syntax diagram (inline)
More information about the isabelle-dev