Email Gateway (Aug 19 2022 at 13:10): Email Gateway (Aug 19 2022 at 13:10):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
It seems that LaTexSugar does not process set expressions when
they occur in function definitions, meaning {x | P} instead
of {x. P}. Is this behavior intended?
I prepared a small example theory showing what I mean:
theory Test
imports Main "~~/src/HOL/Library/LaTeXsugar"
begin
datatype fool = Fool
fun silly::"fool ⇒ nat set" where
"silly Fool = {x. x≤7}"
text{*
In the above function definition, the set expression on the
right side of the equation is not processed by LaTeXsugar, while
here, @{term "{x. x≤ 7}"} it is.
*}
end
Best!
Email Gateway (Aug 19 2022 at 13:10):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
Dear Alfio,
it does process them everywhere where Isabelle pretty-prints.
In your example below, Isabelle’s pretty printer is only active for the antiquotation “term”. If you were to write @{thm silly_def} in the same text block, it would show the set comprehension as you expect.
The literal proof text above the “text {*” block is printed exactly as written without any pretty printing.
What I usually do for papers is to use only antiquotations and no literal proof text.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 13:11):From: Alfio Martini <alfio.martini@acm.org>
Thanks for the explanation, Gerwin.
Best!
Last updated: Apr 24 2024 at 01:07 UTC