Zili Wang (Feb 06 2025 at 20:34): Zili Wang (Feb 06 2025 at 20:34):I have a file in which I defined a logic and corresponding syntactic sugar for it, and I have a snippets.thy file (for LaTeX pretty printing) that I want to include a snippet of the semantics for the logic, which uses the syntactic sugar. However, I get the error that "Ambiguous input produces 2 parse trees... 2 terms are type correct...", where the 2 terms are exactly the same expressions.
I am trying to use the hide_const command to solve this issue, but can't get it to work for the syntactic sugar. I am wonder if it is possible to do this with hide_const, or if there are any other ways to resolve this error. Thanks very much in advance!
Last updated: Mar 09 2025 at 12:28 UTC