Re: [isabelle] LaTeXsygar (bug or feature?)



Thanks for the  explanation, Gerwin.

Best!


On Tue, Dec 3, 2013 at 9:35 AM, Gerwin Klein <Gerwin.Klein at nicta.com.au>wrote:

> 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
>
> On 03.12.2013, at 10:10 pm, Alfio Martini <alfio.martini at acm.org> wrote:
>
> > 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!
> > --
> > Alfio Ricardo Martini
> > PhD in Computer Science (TU Berlin)
> > www.inf.pucrs.br/alfio
> > Lattes:  http://lattes.cnpq.br/4016080665372277
> > Associate Professor at Faculty of Informatics (PUCRS)
> > Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
> > 90619-900 -Porto Alegre - RS - Brasil
>
>
> ________________________________
>
> 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.
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
www.inf.pucrs.br/alfio
Lattes:  http://lattes.cnpq.br/4016080665372277
Associate Professor at Faculty of Informatics (PUCRS)
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil



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