Stream: General

Topic: Persistent assumption attributes


view this post on Zulip 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: Aug 15 2022 at 02:13 UTC