Re: [isabelle] Output panel term printing
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
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,
On 24/10/16 13:17, Iulia Dragomir wrote:
I have a question regarding the printing of terms in the Output panel of
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and