+++ /dev/null
-<!DOCTYPE OpList SYSTEM "operator.dtd">
-
-<OpList xmlns:m="http://www.w3.org/1998/Math/MathML">
-
-<import href="modeset.xsl"/>
-
-<Operator
- name = "IN"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
- cook = "true"
- arity = "2">
- <mapp>
- <mop tag="in"/>
- <param id="2"/>
- <param id="1" mode="set"/>
- </mapp>
-</Operator>
-
-<NotOperator
- name = "NOT IN"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/In.con"
- cook = "true"
- arity = "2">
- <mapp>
- <m:notin/>
- <param id="2"/>
- <param id="1" mode="set"/>
- </mapp>
-</NotOperator>
-
-<OpSet
- name = "EMPTY SET"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind"
- cook = "true">
-
- <Case arity="0">
- <mop tag="set" helm:xref="$APP-ID"/>
- </Case>
-
- <Case arity="1">
- <mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
- <param id="1"/>
- <mop tag="set" helm:xref="$APP-ID"/>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "SINGLETON"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind"
- cook = "true">
-
- <Case arity="1">
- <mop tag="set" helm:xref="$APP-ID">
- <param id="1"/>
- </mop>
- </Case>
-
- <Case arity="2">
- <mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
- <param id="2"/>
- <m:set definitionURL="$OP-URI">
- <param id="1"/>
- </m:set>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "COUPLE"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind"
- cook = "true">
-
- <Case arity="2">
- <mop tag="set" helm:xref="$APP-ID">
- <param id="1"/>
- <param id="2"/>
- </mop>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
- <param id="3"/>
- <m:set definitionURL="$OP-URI">
- <param id="1"/>
- <param id="2"/>
- </m:set>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "TRIPLE"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind"
- cook = "true">
-
- <Case arity="3">
- <mop tag="set">
- <param id="1"/>
- <param id="2"/>
- <param id="3"/>
- </mop>
- </Case>
-
- <Case arity="4">
- <mapp>
- <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
- <param id="4"/>
- <m:set definitionURL="$OP-URI">
- <param id="1"/>
- <param id="2"/>
- <param id="3"/>
- </m:set>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "INTERSECTION"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind"
- cook = "true">
-
- <Case arity="2">
- <mapp>
- <mop tag="intersect"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </mapp>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in/>
- <param id="3"/>
- <m:apply>
- <mop tag="intersect"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </m:apply>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "UNION"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Union.ind"
- cook = "true">
-
- <Case arity="2">
- <mapp>
- <mop tag="union"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </mapp>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in/>
- <param id="3"/>
- <m:apply>
- <mop tag="union"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </m:apply>
- </mapp>
- </Case>
-</OpSet>
-
-<Operator
- name = "INCLUDED"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Included.con"
- cook = "true"
- arity = "2">
- <mapp>
- <mop tag="subset"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </mapp>
-</Operator>
-
-<Operator
- name = "STRICTLY INCLUDED"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con"
- cook = "true"
- arity = "2">
- <mapp>
- <mop tag="prsubset"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </mapp>
-</Operator>
-
-<OpSet
- name = "SET-DIFF"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con"
- cook = "true">
-
- <Case arity="2">
- <mapp>
- <mop tag="setdiff"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </mapp>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in/>
- <param id="3"/>
- <m:apply>
- <mop tag="setdiff"/>
- <param id="1" mode="set"/>
- <param id="2" mode="set"/>
- </m:apply>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "ADD-ELEM"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Add.con"
- cook = "true">
-
- <Case arity="2">
- <mapp>
- <mop tag="union"/>
- <param id="1" mode="set"/>
- <m:set>
- <param id="2" mode="set"/>
- </m:set>
- </mapp>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in/>
- <param id="3"/>
- <m:apply>
- <mop tag="union"/>
- <param id="1" mode="set"/>
- <m:set>
- <param id="2"/>
- </m:set>
- </m:apply>
- </mapp>
- </Case>
-</OpSet>
-
-<OpSet
- name = "SUBTRACT-ELEM"
- uri = "cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con"
- cook = "true">
-
- <Case arity="2">
- <mapp>
- <mop tag="setdiff"/>
- <param id="1" mode="set"/>
- <m:set>
- <param id="2"/>
- </m:set>
- </mapp>
- </Case>
-
- <Case arity="3">
- <mapp>
- <m:in/>
- <param id="3"/>
- <m:apply>
- <mop tag="setdiff"/>
- <param id="1" mode="set"/>
- <m:set>
- <param id="2"/>
- </m:set>
- </m:apply>
- </mapp>
- </Case>
-</OpSet>
-
-<Operator
- name = "CARD"
- uri = "cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind"
- cook = "true"
- arity = "2">
- <mapp>
- <m:eq/>
- <m:apply>
- <mop tag="card"/>
- <param id="1" mode="set"/>
- </m:apply>
- <param id="2"/>
- </mapp>
-</Operator>
-
-<Operator
- name = "SIGMA"
- uri = "cic:/Coq/Init/Specif/Subsets/sig.ind"
- arity = "2">
- <m:set>
- <mbvar name="x">
- <m:type>
- <param id="1"/>
- </m:type>
- </mbvar>
- <m:condition>
- <param id="2" bvar="x"/>
- </m:condition>
- </m:set>
-</Operator>
-
-</OpList>
projects / helm.git / blobdiff