Bob Rubbens (Feb 06 2025 at 09:04): Bob Rubbens (Feb 06 2025 at 09:04):How do I reuse notation introduced in a locale? I'm trying to reuse the Labeled Transition Systems module from AFP, but I can't get it to work. Interpreting the locale works fine, but then reusing notation for its abbreviation doesn't. E.g.:
theory LtsTry
imports Main "Labeled_Transition_Systems.LTS"
begin
interpretation LTS "{(a, b, c). b = a + c} :: (nat, nat) transition set"
proof -
qed
lemma "step_relp a b" (* works, I can ctrl+click step_relp and it points to the above LTS instance *)
sorry
lemma "a ⇒ b" (* inner syntax error, failed to parse prop. Even though this notation is added at the definition of step_relp *)
sorry
end
The first lemma works fine, the second has an inner syntax error on =>. Do I have to specify all notation that I want manually using a rewrites clause on interpretation? Or is there some additional flag I need to put somewhere to propagate notation from the interpreted locale to my global theory? global_interpretation also doesn't do it. Or is it nonsensical to want to reuse notation from a locale, for some reason I don't know about yet? I guess if really necessary I could create some new abbreviations to introduce the syntax I need, but it feels like I'm missing something...
Bram Kohlen (Feb 06 2025 at 09:25):The interpretation seems to igore the notation introduced in the locale. Not sure how to do a clean solution, but you could do a quick hack by reintroducing the notation yourself with:
notation step_relp (infix "⇒" 80)
But if someone has a cleaner solution that does not involve introducing the same notation in two different places I would be happy to hear about it too.
Last updated: Mar 09 2025 at 12:28 UTC