Re: [isabelle] Declaring global attributes



Hi John,

Am 23.10.2011 um 22:49 schrieb John Munroe:

> 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
> *}

This declares the attribute "foo" twice, which is a bad idea. Try this (tested with Isabelle2011):

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

    declare [[ foo = 3 ]]

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

Regards,

Jasmin






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