]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/style/inductive.xsl
Notation for if then else.
[helm.git] / helm / style / inductive.xsl
index 4066d4be3e289a76395cbd556adb8d4bb76b853a..21f16d7a4dbad930062197543237fc44b81070fe 100644 (file)
  <xsl:param name="arg_types" select="/.."/>
  <xsl:param name="actual_args" select="/.."/>
  <xsl:param name="bool_var" select="true()"/>
+ <!-- <xsl:value-of select="false()"/> -->
  <xsl:choose>
   <xsl:when test="count($arg_types) = 0">
     <xsl:value-of select="$bool_var"/>
   </xsl:when>
   <xsl:otherwise>
    <xsl:variable name="no_expected_arg_of_arg" 
-                 select="count($arg_types[1]/PROD/decl)"/>
+                 select="count($arg_types[1]/decl)"/>
    <xsl:variable name="no_actual_abst_of_arg" 
-                 select="count($actual_args[1]/LAMBDA/decl)"/> 
+                 select="count($actual_args[1]/decl)"/> 
    <xsl:variable name="test_arg" 
-    select="$no_actual_abst_of_arg >= $no_expected_arg_of_arg"/> 
+    select="($no_actual_abst_of_arg >= $no_expected_arg_of_arg)"/> 
    <xsl:call-template name="check_args">
     <xsl:with-param name="arg_types" select="$arg_types[position()>1]"/>
     <xsl:with-param name="actual_args" select="$actual_args[position()>1]"/>