Re: [isabelle] case in LaTeX output

Dear Jeremy,

An eta-contraction is happening here, because the bound variable v1 is the last argument to the case operator, so Isabelle sees "%v1. case_val ... ... v1" here. Have you tried to disable locally eta-contraction, e.g., by declare [[eta_contract = false]]?

Alternatively, you can install a print_translation to avoid the eta-contraction for set_bind:

print_translation {*
     @{const_syntax set_bind} @{syntax_const "_set_bind"}

Disclaimer: I've just adapted this from the setup for Ball/Bex, but I haven't tried whether this works for your specific bind operation.

Hope this helps,

On 17/07/17 23:18, Siek, Jeremy wrote:

Iâm seeing a case turn into a call to the datatypeâs case function in the LaTeX output
(see case-val below), but Iâd prefer it to stay as a case.

In particular, I have the following equation in a fun definition.

"E (EIf e1 e2 e3) Ï = (v1 â E e1 Ï;
                               case v1 of
                                 (VNat n) â if n â 0 then E e2 Ï else E e3 Ï
                               | (VFun t) â zero)â

But itâs producing the following in the LaTeX (PDF):

E (if e1 then e2 else e3) Ï = set-bind (E e1 Ï) (case-val (În. if n   0 then E e2 Ï else E e3 Ï) (Ît. zero))

Iâm wondering if the set-bind is somehow triggering this behaviorâ Itâs the bind for a
non-determinism monad that I define as follows.

definition set_bind :: "'a M â ('a â 'b M) â 'b M" where
   "set_bind m f â { v. â v'. v' â m â v â f v' }"
declare set_bind_def[simp]

syntax "_set_bind" :: "[pttrns,'a M,'b] â 'c" ("(_ â _;//_)" 0)
translations "P â E; F" â "CONST set_bind E (ÎP. F)â

Any help is appreciated!


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