helm/style/set.xsl

   1 <?xml version="1.0"?>
   2
   3 <!-- Copyright (C) 2000, HELM Team                                     -->
   4 <!--                                                                   -->
   5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
   6 <!-- Library of Mathematics, developed at the Computer Science         -->
   7 <!-- Department, University of Bologna, Italy.                         -->
   8 <!--                                                                   -->
   9 <!-- HELM is free software; you can redistribute it and/or             -->
  10 <!-- modify it under the terms of the GNU General Public License       -->
  11 <!-- as published by the Free Software Foundation; either version 2    -->
  12 <!-- of the License, or (at your option) any later version.            -->
  13 <!--                                                                   -->
  14 <!-- HELM is distributed in the hope that it will be useful,           -->
  15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
  16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
  17 <!-- GNU General Public License for more details.                      -->
  18 <!--                                                                   -->
  19 <!-- You should have received a copy of the GNU General Public License -->
  20 <!-- along with HELM; if not, write to the Free Software               -->
  21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
  22 <!-- MA  02111-1307, USA.                                              -->
  23 <!--                                                                   -->
  24 <!-- For details, see the HELM World-Wide-Web page,                    -->
  25 <!-- http://cs.unibo.it/helm/.                                         -->
  26
  27 <!--******************************************************************-->
  28 <!-- Basic Set Theory                                                 -->
  29 <!-- First draft: April 3 2000                                        -->
  30 <!-- HELM Group: Asperti, Padovani, Sacerdoti, Schena                 -->
  31 <!--******************************************************************-->
  32
  33 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
  34                               xmlns:m="http://www.w3.org/1998/Math/MathML"
  35                               xmlns:helm="http://www.cs.unibo.it/helm">
  36
  37
  38 <!-- ************************* LOGIC *********************************-->
  39
  40
  41
  42 <xsl:template match="*" mode="set">
  43     <xsl:choose>
  44      <xsl:when test="name() = 'LAMBDA'">
  45       <m:set>
  46        <m:bvar>
  47         <m:ci>
  48          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="target/@binder"/></xsl:with-param></xsl:call-template>
  49         </m:ci>
  50         <m:type>
  51          <xsl:apply-templates select="source" mode="noannot"/>
  52         </m:type>
  53        </m:bvar>
  54        <m:condition>
  55         <xsl:apply-templates select="target" mode="noannot"/>
  56        </m:condition>
  57       </m:set>
  58      </xsl:when>
  59      <xsl:otherwise>
  60       <xsl:apply-templates select="." mode="noannot"/>
  61      </xsl:otherwise>
  62     </xsl:choose>
  63 </xsl:template>
  64
  65
  66 <!-- IN -->
  67
  68 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]" mode="pure">
  69     <xsl:variable name="no_params">
  70      <xsl:call-template name="get_no_params">
  71       <xsl:with-param name="first_uri" select="$CICURI"/>
  72       <xsl:with-param name="second_uri" select="CONST/@uri"/>
  73      </xsl:call-template>
  74     </xsl:variable>
  75     <xsl:choose>
  76      <xsl:when test="(count(child::*) - number($no_params)) = 3">
  77       <m:apply helm:xref="{@id}">
  78        <m:in definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
  79        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
  80        <!-- <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/> -->
  81        <xsl:apply-templates select="*[2+$no_params]" mode="set" />
  82       </m:apply>
  83      </xsl:when>
  84      <xsl:otherwise>
  85       <xsl:apply-imports/>
  86      </xsl:otherwise>
  87     </xsl:choose>
  88 </xsl:template>
  89
  90
  91 <!-- NOT-IN -->
  92 <!-- NOT ha no parameters -->
  93 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Init/Logic/not.con']
  94 and (count(child::*) = 2) and APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/In.con']]]" mode="pure">
  95     <xsl:variable name="no_params">
  96      <xsl:call-template name="get_no_params">
  97       <xsl:with-param name="first_uri" select="$CICURI"/>
  98       <xsl:with-param name="second_uri" select="APPLY/CONST/@uri"/>
  99      </xsl:call-template>
 100     </xsl:variable>
 101     <xsl:choose>
 102      <xsl:when test="(count(APPLY/child::*) - number($no_params)) = 3">
 103       <m:apply helm:xref="{@id}">
 104        <m:notin/>
 105        <xsl:apply-templates select="*[2]/*[3+$no_params]" mode="noannot"/>
 106   <!-- <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="noannot"/> -->
 107        <xsl:apply-templates select="*[2]/*[2+$no_params]" mode="set"/>
 108       </m:apply>
 109      </xsl:when>
 110      <xsl:otherwise>
 111       <xsl:apply-imports/>
 112      </xsl:otherwise>
 113     </xsl:choose>
 114 </xsl:template>
 115
 116 <!-- EMPTY SET -->
 117
 118 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Empty_set.ind']]" mode="pure">
 119     <xsl:variable name="no_params">
 120      <xsl:call-template name="get_no_params">
 121       <xsl:with-param name="first_uri" select="$CICURI"/>
 122       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 123      </xsl:call-template>
 124     </xsl:variable>
 125     <xsl:choose>
 126      <xsl:when test="(count(child::*) - number($no_params)) = 1">
 127       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 128       </m:set>
 129      </xsl:when>
 130      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 131       <m:apply helm:xref="{@id}">
 132        <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
 133        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 134        <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 135        </m:set>
 136       </m:apply>
 137      </xsl:when>
 138      <xsl:otherwise>
 139       <xsl:apply-imports/>
 140      </xsl:otherwise>
 141     </xsl:choose>
 142 </xsl:template>
 143
 144 <!-- SINGLETON -->
 145
 146 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Singleton.ind']]" mode="pure">
 147     <xsl:variable name="no_params">
 148      <xsl:call-template name="get_no_params">
 149       <xsl:with-param name="first_uri" select="$CICURI"/>
 150       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 151      </xsl:call-template>
 152     </xsl:variable>
 153     <xsl:choose>
 154      <xsl:when test="(count(child::*) - number($no_params)) = 2">
 155       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 156        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 157       </m:set>
 158      </xsl:when>
 159      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 160       <m:apply helm:xref="{@id}">
 161        <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
 162        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 163        <m:set definitionURL="{MUTIND/@uri}">
 164         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 165        </m:set>
 166       </m:apply>
 167      </xsl:when>
 168      <xsl:otherwise>
 169       <xsl:apply-imports/>
 170      </xsl:otherwise>
 171     </xsl:choose>
 172 </xsl:template>
 173
 174 <!-- COUPLE -->
 175
 176 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Couple.ind']]" mode="pure">
 177     <xsl:variable name="no_params">
 178      <xsl:call-template name="get_no_params">
 179       <xsl:with-param name="first_uri" select="$CICURI"/>
 180       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 181      </xsl:call-template>
 182     </xsl:variable>
 183     <xsl:choose>
 184      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 185       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 186        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 187        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 188       </m:set>
 189      </xsl:when>
 190      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 191       <m:apply helm:xref="{@id}">
 192        <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
 193        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 194        <m:set definitionURL="{MUTIND/@uri}">
 195         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 196         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 197        </m:set>
 198       </m:apply>
 199      </xsl:when>
 200      <xsl:otherwise>
 201       <xsl:apply-imports/>
 202      </xsl:otherwise>
 203     </xsl:choose>
 204 </xsl:template>
 205
 206 <!-- TRIPLE -->
 207
 208 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Triple.ind'] and (count(child::*) = 5)]" mode="pure">
 209     <xsl:variable name="no_params">
 210      <xsl:call-template name="get_no_params">
 211       <xsl:with-param name="first_uri" select="$CICURI"/>
 212       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 213      </xsl:call-template>
 214     </xsl:variable>
 215     <xsl:choose>
 216      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 217       <m:set definitionURL="{MUTIND/@uri}" helm:xref="{@id}">
 218        <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 219        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 220        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 221       </m:set>
 222      </xsl:when>
 223      <xsl:when test="(count(child::*) - number($no_params)) = 5">
 224       <m:apply helm:xref="{@id}">
 225        <m:in definitionURL="cic:/Coq/Sets/Ensembles/Ensembles/In.con"/>
 226        <xsl:apply-templates select="*[5+$no_params]" mode="noannot"/>
 227        <m:set definitionURL="{MUTIND/@uri}">
 228         <xsl:apply-templates select="*[2+$no_params]" mode="noannot"/>
 229         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 230         <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 231        </m:set>
 232       </m:apply>
 233      </xsl:when>
 234      <xsl:otherwise>
 235       <xsl:apply-imports/>
 236      </xsl:otherwise>
 237     </xsl:choose>
 238 </xsl:template>
 239
 240 <!-- INTERSECTION -->
 241
 242 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Intersection.ind']]" mode="pure">
 243     <xsl:variable name="no_params">
 244      <xsl:call-template name="get_no_params">
 245       <xsl:with-param name="first_uri" select="$CICURI"/>
 246       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 247      </xsl:call-template>
 248     </xsl:variable>
 249     <xsl:choose>
 250      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 251       <m:apply helm:xref="{@id}">
 252        <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 253        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 254        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 255       </m:apply>
 256      </xsl:when>
 257      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 258       <m:apply helm:xref="{@id}">
 259        <m:in/>
 260        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 261        <m:apply>
 262         <m:intersect definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 263         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 264         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 265        </m:apply>
 266       </m:apply>
 267      </xsl:when>
 268      <xsl:otherwise>
 269       <xsl:apply-imports/>
 270      </xsl:otherwise>
 271     </xsl:choose>
 272 </xsl:template>
 273
 274
 275 <!-- UNION -->
 276
 277 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Union.ind']]" mode="pure">
 278     <xsl:variable name="no_params">
 279      <xsl:call-template name="get_no_params">
 280       <xsl:with-param name="first_uri" select="$CICURI"/>
 281       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 282      </xsl:call-template>
 283     </xsl:variable>
 284     <xsl:choose>
 285      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 286       <m:apply helm:xref="{@id}">
 287        <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 288        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 289        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 290       </m:apply>
 291      </xsl:when>
 292      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 293       <m:apply helm:xref="{@id}">
 294        <m:in/>
 295        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 296        <m:apply>
 297         <m:union definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 298         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 299         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 300        </m:apply>
 301       </m:apply>
 302      </xsl:when>
 303      <xsl:otherwise>
 304       <xsl:apply-imports/>
 305      </xsl:otherwise>
 306     </xsl:choose>
 307 </xsl:template>
 308
 309 <!-- INCLUDED -->
 310
 311 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Included.con']]" mode="pure">
 312     <xsl:variable name="no_params">
 313      <xsl:call-template name="get_no_params">
 314       <xsl:with-param name="first_uri" select="$CICURI"/>
 315       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 316      </xsl:call-template>
 317     </xsl:variable>
 318     <xsl:choose>
 319      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 320       <m:apply helm:xref="{@id}">
 321        <m:subset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 322        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 323        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 324       </m:apply>
 325      </xsl:when>
 326      <xsl:otherwise>
 327       <xsl:apply-imports/>
 328      </xsl:otherwise>
 329     </xsl:choose>
 330 </xsl:template>
 331
 332 <!-- STRICTLY INCLUDED -->
 333
 334 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Strict_Included.con']]" mode="pure">
 335     <xsl:variable name="no_params">
 336      <xsl:call-template name="get_no_params">
 337       <xsl:with-param name="first_uri" select="$CICURI"/>
 338       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 339      </xsl:call-template>
 340     </xsl:variable>
 341     <xsl:choose>
 342      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 343       <m:apply helm:xref="{@id}">
 344        <m:prsubset definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 345        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 346        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 347       </m:apply>
 348      </xsl:when>
 349      <xsl:otherwise>
 350       <xsl:apply-imports/>
 351      </xsl:otherwise>
 352     </xsl:choose>
 353 </xsl:template>
 354
 355 <!-- SET-DIFF -->
 356
 357 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Setminus.con']]" mode="pure">
 358     <xsl:variable name="no_params">
 359      <xsl:call-template name="get_no_params">
 360       <xsl:with-param name="first_uri" select="$CICURI"/>
 361       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 362      </xsl:call-template>
 363     </xsl:variable>
 364     <xsl:choose>
 365      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 366       <m:apply helm:xref="{@id}">
 367        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 368        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 369        <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 370       </m:apply>
 371      </xsl:when>
 372      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 373       <m:apply helm:xref="{@id}">
 374        <m:in/>
 375        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 376        <m:apply>
 377         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 378         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 379         <xsl:apply-templates select="*[3+$no_params]" mode="set"/>
 380        </m:apply>
 381       </m:apply>
 382      </xsl:when>
 383      <xsl:otherwise>
 384       <xsl:apply-imports/>
 385      </xsl:otherwise>
 386     </xsl:choose>
 387 </xsl:template>
 388
 389 <!-- ADD-ELEM -->
 390
 391 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Add.con']]" mode="pure">
 392     <xsl:variable name="no_params">
 393      <xsl:call-template name="get_no_params">
 394       <xsl:with-param name="first_uri" select="$CICURI"/>
 395       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 396      </xsl:call-template>
 397     </xsl:variable>
 398     <xsl:choose>
 399      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 400       <m:apply helm:xref="{@id}">
 401        <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 402        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 403        <m:set>
 404         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 405        </m:set>
 406       </m:apply>
 407      </xsl:when>
 408      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 409       <m:apply helm:xref="{@id}">
 410        <m:in/>
 411        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 412        <m:apply>
 413         <m:union definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 414         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 415         <m:set>
 416          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 417         </m:set>
 418        </m:apply>
 419       </m:apply>
 420      </xsl:when>
 421      <xsl:otherwise>
 422       <xsl:apply-imports/>
 423      </xsl:otherwise>
 424     </xsl:choose>
 425 </xsl:template>
 426
 427 <!-- SUBTRACT-ELEM -->
 428
 429 <xsl:template match="APPLY[CONST[attribute::uri='cic:/Coq/Sets/Ensembles/Ensembles/Subtract.con']]" mode="pure">
 430     <xsl:variable name="no_params">
 431      <xsl:call-template name="get_no_params">
 432       <xsl:with-param name="first_uri" select="$CICURI"/>
 433       <xsl:with-param name="second_uri" select="CONST/@uri"/>
 434      </xsl:call-template>
 435     </xsl:variable>
 436     <xsl:choose>
 437      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 438       <m:apply helm:xref="{@id}">
 439        <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 440        <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 441        <m:set>
 442         <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 443        </m:set>
 444       </m:apply>
 445      </xsl:when>
 446      <xsl:when test="(count(child::*) - number($no_params)) = 4">
 447       <m:apply helm:xref="{@id}">
 448        <m:in/>
 449        <xsl:apply-templates select="*[4+$no_params]" mode="noannot"/>
 450        <m:apply>
 451         <m:setdiff definitionURL="{CONST/@uri}" helm:xref="{CONST/@id}"/>
 452         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 453         <m:set>
 454          <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 455         </m:set>
 456        </m:apply>
 457       </m:apply>
 458      </xsl:when>
 459      <xsl:otherwise>
 460       <xsl:apply-imports/>
 461      </xsl:otherwise>
 462     </xsl:choose>
 463 </xsl:template>
 464
 465 <!-- CARD -->
 466
 467 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Sets/Finite_sets/Ensembles_finis/cardinal.ind']]" mode="pure">
 468     <xsl:variable name="no_params">
 469      <xsl:call-template name="get_no_params">
 470       <xsl:with-param name="first_uri" select="$CICURI"/>
 471       <xsl:with-param name="second_uri" select="MUTIND/@uri"/>
 472      </xsl:call-template>
 473     </xsl:variable>
 474     <xsl:choose>
 475      <xsl:when test="(count(child::*) - number($no_params)) = 3">
 476       <m:apply helm:xref="{@id}">
 477        <m:eq/>
 478        <m:apply>
 479         <m:card definitionURL="{MUTIND/@uri}" helm:xref="{MUTIND/@id}"/>
 480         <xsl:apply-templates select="*[2+$no_params]" mode="set"/>
 481        </m:apply>
 482        <xsl:apply-templates select="*[3+$no_params]" mode="noannot"/>
 483       </m:apply>
 484      </xsl:when>
 485      <xsl:otherwise>
 486       <xsl:apply-imports/>
 487      </xsl:otherwise>
 488     </xsl:choose>
 489 </xsl:template>
 490
 491 <!-- *******************  SIGMA TYPES  **************************** -->
 492
 493 <xsl:template match="APPLY[MUTIND[attribute::uri='cic:/Coq/Init/Specif/Subsets/sig.ind']]" mode="pure">
 494  <xsl:choose>
 495   <xsl:when test="count(child::*) = 3">
 496    <xsl:choose>
 497     <xsl:when test="name(*[3]) = 'LAMBDA'">
 498      <m:set>
 499        <m:bvar>
 500         <m:ci>
 501          <xsl:call-template name="insert_subscript"><xsl:with-param name="node_value"><xsl:value-of select="*[3]/target/@binder"/></xsl:with-param></xsl:call-template>
 502         </m:ci>
 503         <m:type>
 504          <xsl:apply-templates select="*[3]/source/*[1]" mode="noannot"/>
 505         </m:type>
 506        </m:bvar>
 507        <m:condition>
 508         <xsl:apply-templates select="*[3]/target/*[1]" mode="noannot"/>
 509        </m:condition>
 510      </m:set>
 511     </xsl:when>
 512     <xsl:otherwise>
 513      <m:set>
 514        <m:bvar>
 515         <m:ci>$x</m:ci>
 516         <m:type>
 517          <xsl:apply-templates select="*[2]" mode="noannot"/>
 518         </m:type>
 519        </m:bvar>
 520        <m:condition>
 521         <m:apply>
 522          <m:csymbol>app</m:csymbol>
 523          <xsl:apply-templates select="*[3]" mode="noannot"/>
 524          <m:ci>$x</m:ci>
 525         </m:apply>
 526        </m:condition>
 527      </m:set>
 528     </xsl:otherwise>
 529    </xsl:choose>
 530   </xsl:when>
 531   <xsl:otherwise>
 532    <xsl:apply-imports/>
 533   </xsl:otherwise>
 534  </xsl:choose>
 535 </xsl:template>
 536
 537
 538 </xsl:stylesheet>