Kevin Kappelmann (May 09 2022 at 10:04): Kevin Kappelmann (May 09 2022 at 10:04):I am writing a tool which requires users to tag certain assumptions of their theorem. The theorem should then be stored together with a map from its assumptions to tags as indicated by the user. Basically, given something like this:
lemma test [my_attribute]:
assumes "A"
and [my_asm "some text"]: "B"
shows "A ∧ B"
sorry
It should store ?A ⟹ ?B ⟹ ?A ∧ ?B together with the map {2 -> "some text"}.
Is this even possible? It seems impossible to me since, as far as I can tell, the context passed when running the lemma's attribute (my_attribute above) won't contain whatever data is stored in the context by the assumption's attribute (my_asm above).
The alternative, of course, would be to include a list of tags for each assumption next to my_attribute but I find that not so nice from an UI perspective
Last updated: Apr 25 2024 at 20:15 UTC