Re: [isabelle] LaTeXsugar



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, 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.