Re: [isabelle] Declaring global attributes



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.