Re: [isabelle] Declaring global attributes



Thanks. Can I try to imitate the setup_config_int function with:

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

val foo_raw = Config.declare_global "foo" (K (Config.Int 2));
val foo = Config.int foo_raw
*}
declare [[ foo = 3 ]]

But reading the attribute with

ML {*
val max_stuff_arty = Config.get_global @{theory} max_stuff_arity
*}

gives 2 rather than 3. Am I missing something here?

Thanks for the help.

John


On Sun, Oct 23, 2011 at 6:48 PM, Makarius <makarius at sketis.net> wrote:
> On Sat, 22 Oct 2011, John Munroe wrote:
>
>> I can't seem to find Attrib.setup_config_int in Isabelle2011.
>
> It is there in the current official release, which is Isabelle2011-1.
>
>
>> 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]]
>
> The ML foo above is a pair (config, setup).  The setup component needs to be
> applied to the theory context using the 'setup' command in Isar.
>
>
>        Makarius
>





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