Ata Keskin (Dec 25 2023 at 23:58): Ata Keskin (Dec 25 2023 at 23:58):In a parent locale "linearly_filtered_measure", I introduced the following notation:
definition F_infinity :: "'a measure" ("F⇩∞") where
"F⇩∞ = sigma (space M) (⋃t∈{t⇩0..}. sets (F t))"
where "t⇩0" M and F are constants that the locale fixes.
When I use the notation in the context of this locale everything works as it should. I have a sublocale called "nat_filtered_measure" which is a sublocale of "linearly_filtered_measure". The parser does not recognize the notation inside the sublocale. To illustrate the issue further:
context linearly_filtered_measure
begin
thm F_infinity_def
outputs
F⇩∞ = sigma (space M) (⋃t∈{t⇩0..}. sets (F t))
whereas
context nat_filtered_measure
begin
thm F_infinity_def
outputs
F_infinity = sigma (space M) (⋃t∈{t⇩0..}. sets (F t))
which does not use the notation at all. Is this just an oversight concerning how the introduced notation is handled in the locale system or am I doing something wrong?
Ata Keskin (Dec 26 2023 at 00:02):I figured it out. Using the notation command fixes this issue. For anyone who might face a similar issue, you can just do:
notation F_infinity "F⇩∞"
after defining the constant.
Last updated: May 02 2024 at 04:18 UTC