Email Gateway (Aug 22 2022 at 14:20): Email Gateway (Aug 22 2022 at 14:20):From: Iulia Dragomir <iulia.dragomir@aalto.fi>
Dear list,
I have a question regarding the printing of terms in the Output panel of
Isabelle jedit.
Whenever I have a term such as
term "λx. (0 ≤ x)"
this gets rewritten as
"op ≤ 0"
Is there a way to turn off this printing and see the term as it is defined?
Best regards,
Iulia Dragomir
Email Gateway (Aug 22 2022 at 14:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Iulia,
By default, pretty-printing eta-contracts terms. In your example, "%x. 0 <= x" is
internally represented as "%x. (op <=) 0 x", which is contracted to "(op <=) x", where "op
<=" is the prefix syntax for the less-than-or-equal operation. You can control
eta-contraction for pretty-printing with the attribute [[eta_contract]]. So, after
declare [[eta_contract=false]]
your term should print the way you have input it. Note, however, that some proof methods
internally perform eta expansion (in particular induction, subst, and simp with congruence
rules), so you may see lots of such eta-expanded terms in your goal state, but you can
still write them in the contracted form in "show" or "have" commands.
Hope this helps,
Andreas
Last updated: Apr 26 2024 at 12:28 UTC