[isabelle] LaTeXsygar (bug or feature?)



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



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