Re: [isabelle] Attribute code called 3 times



Hi Lukas,

On Sun, Mar 11, 2012 at 2:28 PM, Lukas Bulwahn <bulwahn at in.tum.de> wrote:
> It somewhat stores the data in three different layers.
> However, when you lookup data, you will probably only see one version from
> the one layer you are working in.

This answers the question, thanks!

> What's the point of getting it called only once anyway?

For certain theorems that are not of the valid format I want to print
a warning, and this warning is printed zero or three times. So far I
ignored the "Context.generic" argument, and checking that it is a
theory should to do the job.

Regards,

Cezary

> On 03/10/2012 11:38 PM, Cezary Kaliszyk wrote:
>>
>> Hi all,
>>
>> I want to define an attribute, that takes a string as an argument
>> with the code below:
>>
>> ML {* fun attr s = let val _ = warning s in
>>       (Thm.rule_attribute (fn _ =>  fn y =>  y)) end *}
>> setup {* Attrib.setup (Binding.name "map_const")
>>       (Scan.lift Parse.string>>  attr) "..." *}
>> lemma [map_const "foo"]: True
>>   by simp
>>
>> However upon defining the lemma, "foo" is printed 3 times. Is there a
>> good reason why the attribute code is called 3 times and is it
>> possible to get it called only once?
>>
>> Regards,
>>
>> Cezary
>>
>



-- 
Cezary Kaliszyk, University of Innsbruck,
http://cl-informatik.uibk.ac.at/~cek/





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