Re: [isabelle] LaTeXsugar



I don't like the {f i|i. True} syntax either but your {f i}_i is a bit
non-standard, too, isn't it? I sometimes write UN i. {f i} in such cases. Of
course, it gives you a different term, but mostly it behaves the same.

Tobias

Am 30/01/2013 04:26, schrieb Christian Sternagel:
> Dear Sugarers,
> 
> how about adding the following to LaTeXsugar.thy?
> 
> syntax (latex output)
>   "_CollectIndex" ::
>     "pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<^esub>)")
> 
> translations
>   "_CollectIndex p i" <= "{p | i. CONST True}"
> 
> 
> term "{f i | i. True}"
> 
> cheers
> 
> chris





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