Re: [isabelle] LaTeXsugar




Am 30/01/2013 14:53, schrieb Christian Sternagel:
> On 01/30/2013 04:03 PM, Tobias Nipkow wrote:
>> 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 don't know ;). I think {f i}_{i : ℕ} is fairly standard,

If you can convince me of that, I'll probably add your original syntax (unless
other problems crop up). I am just unsure myself, although it looks plausible.

Tobias

> and since all natural
> numbers are ge 0, I thought, just drop it. Alternatively, we could do the
> following specifically for nats:
> 
>  syntax (latex output)
>     "_CollectIndex_nat" ::
>       "pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_\<ge>0\<^esub>)")
> 
>  translations
>     "_CollectIndex_nat p i" <= "{p | (i::nat). CONST True}"
> 
> or
> 
>  syntax (latex output)
>     "_CollectIndex_nat" ::
>       "pttrn => pttrn => 'a set" ("(1{_}\<^bsub>_∈ℕ\<^esub>)")
> 
> cheers
> 
> chris
> 
>>
>> 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.