Re: [isabelle] Output panel term printing



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

On 24/10/16 13:17, Iulia Dragomir wrote:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.