From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 10 Dec 2002 17:50:45 +0000 (+0000)
Subject: First experimental commit of the notation (partial!) for real numbers.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ff85e55518d06d96b9abbea4aa68d83e6be35b0;p=helm.git

First experimental commit of the notation (partial!) for real numbers.
---

diff --git a/helm/meta_style/positive.xsl b/helm/meta_style/positive.xsl
index 6a99d12ff..baee6a907 100644
--- a/helm/meta_style/positive.xsl
+++ b/helm/meta_style/positive.xsl
@@ -173,5 +173,46 @@ and @uri='cic:/Coq/ZArith/fast_integer/positive.ind' and @noConstr='2']">
  </xsl:choose>
 </xsl:template>
 
+<!-- **************************** Reals ******************************** -->
+
+<xsl:template match="APPLY[CONST[position() = 1 and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and count(*) = 3]" mode="pure">
+  <xsl:variable name="result">
+   <xsl:apply-templates select="." mode="reals"/>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="string($result) = ''">
+    <m:apply helm:xref="{@id}">
+      <m:plus xmlns:m="http://www.w3.org/1998/Math/MathML" definitionURL="{CONST[1]/@uri}" helm:xref="{CONST[1]/@id}"/>
+      <xsl:apply-templates select="*[2]" mode="noannot"/>
+      <xsl:apply-templates select="*[3]" mode="noannot"/>
+    </m:apply>
+   </xsl:when>
+   <xsl:otherwise>
+    <m:cn helm:xref="{CONST[1]/@id}"><xsl:value-of select="$result"/></m:cn>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template match="APPLY[CONST[position() = 1 and @uri='cic:/Coq/Reals/Rdefinitions/Rplus.con'] and CONST[position() = 2 and @uri='cic:/Coq/Reals/Rdefinitions/R1.con'] and count(*) = 3]" mode="reals">
+  <xsl:param name="real_counter" select="0"/>
+  <xsl:variable name="result">
+   <xsl:apply-templates select="*[3]" mode="reals">
+    <xsl:with-param name="real_counter" select="$real_counter + 1"/>
+   </xsl:apply-templates>
+  </xsl:variable>
+  <xsl:choose>
+   <xsl:when test="string($result) = ''"/>
+   <xsl:otherwise>
+    <xsl:value-of select="$result"/>
+   </xsl:otherwise>
+  </xsl:choose>
+</xsl:template>
+
+<xsl:template match="CONST[@uri='cic:/Coq/Reals/Rdefinitions/R1.con']" mode="reals">
+  <xsl:param name="real_counter" select="0"/>
+  <xsl:value-of select="$real_counter + 1"/>
+</xsl:template>
+
+<xsl:template match="*" mode="reals"/>
 
 </xsl:stylesheet>