Email Gateway (Aug 18 2022 at 20:22): Email Gateway (Aug 18 2022 at 20:22):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear all,
Why is the behavior after defining notation inside an auxiliary context
different depending on whether this auxiliary context is inside another
context?
More specifically, consider
context
fixes P :: "'a => 'a => bool"
begin
notation
P ("\<^raw:\foo>")
term P
end
Here "term P" results in: "\<^raw:\foo>" (as expected)
However, as soon as I put the above code inside another context (named
or unnamed), the syntax seems to be ignored and "term P" results in: "P".
What am I missing?
cheers
chris
Email Gateway (Aug 18 2022 at 20:26):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
To my understanding the context sandwich is not properly operating here,
but let us wait for Makarius to comment on this.
Florian
signature.asc
Last updated: Apr 24 2024 at 20:16 UTC