Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] syntax in auxiliary contexts

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: Nov 21 2024 at 12:39 UTC