+++ /dev/null
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
- xmlns:m="http://www.w3.org/1998/Math/MathML">
-
-<xsl:include href="nuprl_proof.xsl"/>
-<xsl:include href="nuprl_abstract.xsl"/>
-<xsl:include href="nuprl_rules.xsl"/>
-
-<!-- NuPrl Term -->
-<xsl:template match="var">
- <m:ci>
- <xsl:value-of select="@val"/>
- </m:ci>
-</xsl:template>
-
-
-<xsl:template match="function">
- <xsl:choose>
- <xsl:when test="type_of">
- <xsl:choose>
- <xsl:when test="type_of/@var=""">
- <m:apply>
- <m:csymbol>arrow</m:csymbol>
- <xsl:apply-templates select="type_of/*"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
- </xsl:when>
- <xsl:otherwise>
- <m:apply>
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="type_of/@var"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="type_of/*"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <m:apply>
- <m:csymbol>arrow</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
- </xsl:otherwise>
- </xsl:choose>
-</xsl:template>
-
-
-<xsl:template match="lambda">
- <m:lambda>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="@binder"/>
- </m:ci>
- </m:bvar>
- <xsl:apply-templates/>
- </m:lambda>
-</xsl:template>
-
-
-<xsl:template match="apply">
- <m:apply>
- <m:csymbol>app</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="product">
- <m:apply>
- <xsl:choose>
- <xsl:when test="type_of">
- <xsl:choose>
- <xsl:when test="type_of/@var=""">
- <m:csymbol>product_ind</m:csymbol>
- <m:type>
- <xsl:apply-templates select="type_of/*"/>
- </m:type>
- </xsl:when>
- <xsl:otherwise>
- <m:csymbol>product</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="type_of/@var"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="type_of/*"/>
- </m:type>
- </m:bvar>
- </xsl:otherwise>
- </xsl:choose>
- </xsl:when>
- <xsl:otherwise>
- <m:csymbol>product_ind</m:csymbol>
- <m:type>
- <xsl:apply-templates select="*[1]"/>
- </m:type>
- </xsl:otherwise>
- </xsl:choose>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="pair">
- <m:apply>
- <m:csymbol>pair</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="spread">
- <m:apply>
- <m:csymbol>mutcase</m:csymbol>
- <m:csymbol>NONE</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <m:piecewise>
- <m:piece>
- <xsl:apply-templates select="*[4]"/>
- <m:apply>
- <m:csymbol>pair</m:csymbol>
- <xsl:apply-templates select="binder[1]"/>
- <xsl:apply-templates select="binder[2]"/>
- </m:apply>
- </m:piece>
- </m:piecewise>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="union">
- <m:apply>
- <m:csymbol>union</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="inl">
- <m:apply>
- <m:csymbol>inl</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="inr">
- <m:apply>
- <m:csymbol>inr</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="decide">
- <m:apply>
- <m:csymbol>mutcase</m:csymbol>
- <m:csymbol>NONE</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <m:piecewise>
- <m:piece>
- <xsl:apply-templates select="*[3]"/>
- <m:apply>
- <m:csymbol>inl</m:csymbol>
- <xsl:apply-templates select="binder[1]"/>
- </m:apply>
- </m:piece>
- <m:piece>
- <xsl:apply-templates select="*[5]"/>
- <m:apply>
- <m:csymbol>inr</m:csymbol>
- <xsl:apply-templates select="binder[2]"/>
- </m:apply>
- </m:piece>
- </m:piecewise>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="universe">
- <m:apply>
- <m:csymbol>universe</m:csymbol>
- <m:cn>
- <xsl:value-of select="@level"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="equal">
- <m:apply>
- <m:csymbol>equal</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- <xsl:apply-templates select="*[3]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="axiom">
- <m:apply>
- <m:csymbol>Ax</m:csymbol>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="void">
- <m:apply>
- <m:csymbol>void</m:csymbol>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="any">
- <m:apply>
- <m:csymbol>mutcase</m:csymbol>
- <m:csymbol>NONE</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="atom">
- <m:apply>
- <m:csymbol>atom</m:csymbol>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="token">
- <m:apply>
- <m:csymbol>token</m:csymbol>
- <m:ci>
- <xsl:value-of select="@val"/>
- </m:ci>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="atom_eq">
- <m:apply>
- <m:csymbol>if_then_else</m:csymbol>
- <m:where>atom_eq</m:where>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- <xsl:apply-templates select="*[3]"/>
- <xsl:apply-templates select="*[4]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="int">
- <m:integers/>
-</xsl:template>
-
-
-<xsl:template match="natural_number">
- <m:cn>
- <xsl:value-of select="@val"/>
- </m:cn>
-</xsl:template>
-
-
-<xsl:template match="minus">
- <m:apply>
- <m:minus/>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="add">
- <m:apply>
- <m:plus/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="subtract">
- <m:apply>
- <m:minus/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="multiply">
- <m:apply>
- <m:times/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="divide">
- <m:apply>
- <m:divide/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="remainder">
- <m:apply>
- <m:rem/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="int_eq">
- <m:apply>
- <m:csymbol>if_then_else</m:csymbol>
- <m:where>int_eq</m:where>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- <xsl:apply-templates select="*[3]"/>
- <xsl:apply-templates select="*[4]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="less">
- <m:apply>
- <m:csymbol>if_then_else</m:csymbol>
- <m:where>less</m:where>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- <xsl:apply-templates select="*[3]"/>
- <xsl:apply-templates select="*[4]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="ind">
- <m:apply>
- <m:csymbol>by_induction</m:csymbol>
- <m:ci>ind</m:ci>
- <m:csymbol>NONE</m:csymbol>
- <m:apply> <!-- CASO BASE -->
- <m:csymbol>inductive_case</m:csymbol>
- <m:apply>
- <m:csymbol>case_lhs</m:csymbol>
- <m:ci>0</m:ci>
- </m:apply>
- <m:apply>
- <m:csymbol>induction_hypothesis</m:csymbol>
- </m:apply>
- <xsl:apply-templates select="*[5]"/>
- </m:apply>
-
- <m:apply> <!--CASO INDUTTIVO PER I NUMERI POSITIVI-->
- <m:csymbol>inductive_case</m:csymbol>
- <m:apply>
- <m:csymbol>case_lhs</m:csymbol>
- <m:ci>succ</m:ci>
- <m:bvar>
- <xsl:apply-templates select="*[6]"/> <!-- u -->
- <m:type>int</m:type>
- </m:bvar>
- </m:apply>
- <m:apply>
- <m:csymbol>induction_hypothesis</m:csymbol>
- <xsl:apply-templates select="*[7]"/> <!-- v -->
- </m:apply>
- <xsl:apply-templates select="*[8]"/> <!-- t -->
- </m:apply>
-
- <m:apply> <!--CASO INDUTTIVO PER I NUMERI NEGATIVI-->
- <m:csymbol>inductive_case</m:csymbol>
- <m:apply>
- <m:csymbol>case_lhs</m:csymbol>
- <m:ci>pred</m:ci>
- <m:bvar>
- <xsl:apply-templates select="*[2]"/> <!-- x -->
- <m:type>int</m:type>
- </m:bvar>
- </m:apply>
- <m:apply>
- <m:csymbol>induction_hypothesis</m:csymbol>
- <xsl:apply-templates select="*[3]"/> <!-- y -->
- </m:apply>
- <xsl:apply-templates select="*[4]"/>
- </m:apply>
- <m:apply>
- <m:csymbol>extra_args</m:csymbol>
- <xsl:apply-templates select="*[1]"/> <!-- a -->
- </m:apply>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="less_than">
- <m:apply>
- <m:lt/>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="list">
- <m:ci>list</m:ci>
-</xsl:template>
-
-
-<xsl:template match="nil">
- <m:apply>
- <m:csymbol>nil</m:csymbol>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="cons">
- <m:apply>
- <m:csymbol>cons</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="list_ind">
- <m:apply>
- <m:csymbol>by_induction</m:csymbol>
- <m:ci>list_ind</m:ci>
- <m:csymbol>NONE</m:csymbol>
- <m:apply>
- <m:csymbol>inductive_case</m:csymbol>
- <m:apply>
- <m:csymbol>case_lhs</m:csymbol>
- <m:ci>nil</m:ci>
- </m:apply>
- <m:apply>
- <m:csymbol>induction_hypothesis</m:csymbol>
- </m:apply>
- <xsl:apply-templates select="*[2]"/> <!-- base -->
- </m:apply>
- <m:apply>
- <m:csymbol>inductive_case</m:csymbol>
- <m:apply>
- <m:csymbol>case_lhs</m:csymbol>
- <m:ci>cons</m:ci>
- <m:bvar>
- <xsl:apply-templates select="*[3]"/> <!-- x -->
- <m:type>?</m:type>
- </m:bvar>
- <m:bvar>
- <xsl:apply-templates select="*[4]"/> <!-- l -->
- <m:type>?</m:type>
- </m:bvar>
- </m:apply>
- <m:apply>
- <m:csymbol>induction_hypothesis</m:csymbol>
- <xsl:apply-templates select="*[5]"/> <!-- Fxl -->
- </m:apply>
- <xsl:apply-templates select="*[6]"/> <!-- t -->
- </m:apply>
- <m:apply>
- <m:csymbol>extra_args</m:csymbol>
- <xsl:apply-templates select="*[1]"/> <!-- s -->
- </m:apply>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="rec">
- <m:apply>
- <m:csymbol>rec</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="rec_ind">
- <m:apply>
- <m:csymbol>app</m:csymbol>
- <m:apply>
- <m:csymbol>fix</m:csymbol>
- <m:ci>
- <xsl:apply-templates select="*[2]"/>
- </m:ci>
- <m:bvar>
- <m:ci>
- <xsl:apply-templates select="*[2]"/>
- </m:ci>
- <m:type>?</m:type>
- </m:bvar>
- <m:lambda>
- <m:bvar>
- <xsl:apply-templates select="*[3]"/>
- </m:bvar>
- <xsl:apply-templates select="*[4]"/>
- </m:lambda>
- </m:apply>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="set">
- <m:apply>
- <m:csymbol>t_set</m:csymbol>
- <m:bvar>
- <xsl:choose>
- <xsl:when test="type_of">
- <m:ci>
- <xsl:value-of select="type_of/@var"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="type_of/*"/>
- </m:type>
- </xsl:when>
- <xsl:otherwise>
- <m:type>
- <xsl:apply-templates select="*[1]"/>
- </m:type>
- </xsl:otherwise>
- </xsl:choose>
- </m:bvar>
- <xsl:apply-templates select="*[2]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="isect">
- <m:apply>
- <m:csymbol>isect</m:csymbol>
- <m:bvar>
- <m:ci>
- <xsl:value-of select="type_of/@var"/>
- </m:ci>
- <m:type>
- <xsl:apply-templates select="type_of/*"/>
- </m:type>
- </m:bvar>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="quotient">
- <m:apply>
- <m:csymbol>quotient</m:csymbol>
- <xsl:apply-templates select="*[1]"/>
- <m:bvar>
- <xsl:value-of select="binder[1]/@var"/>
- </m:bvar>
- <m:bvar>
- <xsl:value-of select="binder[2]/@var"/>
- </m:bvar>
- <xsl:apply-templates select="*[4]"/>
- </m:apply>
-</xsl:template>
-
-
-<xsl:template match="type_of">
- <m:apply>
- <m:csymbol>type_of</m:csymbol>
- <m:ci>
- <xsl:value-of select="@var"/>
- </m:ci>
- <xsl:apply-templates select="*[1]"/>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="prop">
- <m:apply>
- <m:csymbol>prop</m:csymbol>
- <m:cn>
- <xsl:value-of select="@level"/>
- </m:cn>
- </m:apply>
-</xsl:template>
-
-<xsl:template match="binder">
- <m:ci>
- <xsl:value-of select="@var"/>
- </m:ci>
-</xsl:template>
-
-</xsl:stylesheet>
projects / helm.git / blobdiff