Re: [isabelle] Declaring global attributes



Thanks. I can't seem to find Attrib.setup_config_int in Isabelle2011.
Assuming it's the same as Attrib.config_int, the following still gives
me an error:

ML {*
val foo = Attrib.config_int (@{binding "foo"} |> Binding.name_of) (K 2);
*}

declare [[foo = 3]]

John

On Sat, Oct 22, 2011 at 10:15 AM, Jasmin Blanchette
<jasmin.blanchette at gmail.com> wrote:
> Hi John,
>
>> I'm trying to declare an attribute using
>>
>> declare [[foo = 3]]
>>
>> I have this ML code:
>>
>> ML {*
>> Config.declare_global "foo" (K (Config.Int 2));
>> *}
>>
>> But it complains about *** Unknown attribute: "foo". Is something else
>> needed for registering attributes?
>
> The idiom I was taught by Makarius is
>
>    ML {*
>    val foo = Attrib.setup_config_int @{binding "foo"} (K 2);
>    *}
>
>    declare [[foo = 3]]
>
>    ML {*
>    Config.get @{context} foo;
>    *}
>
> Regards,
>
> Jasmin
>
>





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