Commit 09ed0b60 authored by Florian Rabe's avatar Florian Rabe

no message

parent 8ccb101d
......@@ -113,7 +113,17 @@
</om:OMA>
</om:OMBIND><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#444.10.40:444.10.40"/></metadata></om:OMV><om:OMV name="y"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#446.10.42:446.10.42"/></metadata></om:OMV><om:OMV name="p"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#448.10.44:448.10.44"/></metadata></om:OMV><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#450.10.46:457.10.53"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Equality" name="refl"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#384.9.15:384.9.15"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#456.10.52:456.10.52"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples" module="Equality" name="refl"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="a"><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="x"><type><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#384.9.15:384.9.15"/></metadata></om:OMV></type></om:OMV><om:OMV name="y"><type><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#384.9.15:384.9.15"/></metadata></om:OMV></type></om:OMV><om:OMV name="p"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#389.9.20:393.9.24"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Equality" name="equal"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#384.9.15:384.9.15"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#389.9.20:389.9.20"/></metadata></om:OMV><om:OMV name="y"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#393.9.24:393.9.24"/></metadata></om:OMV>
</om:OMA></type></om:OMV><om:OMV name="u"><type><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#329.7.23:329.7.23"/></metadata></om:OMV></type></om:OMV></om:OMBVAR>
<om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#329.7.23:329.7.23"/></metadata></om:OMV>
</om:OMBIND>
<om:OMV name="a"></om:OMV><om:OMV name="x"></om:OMV><om:OMV name="y"></om:OMV><om:OMV name="p"></om:OMV><om:OMV name="x"></om:OMV>
</om:OMA><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#456.10.52:456.10.52"/></metadata></om:OMV>
</om:OMA>
</om:OMA>
</om:OMBIND>
......
......@@ -23,15 +23,15 @@
<om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="y"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS>
</om:OMBIND>
<om:OMV name="/T/2/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#900.30.16:930.30.46"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#901.30.17:901.30.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#903.30.19:903.30.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#901.30.17:901.30.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#903.30.19:903.30.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#906.30.22:930.30.46"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#906.30.22:912.30.28"/></metadata>
......@@ -68,7 +68,7 @@
<om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="y"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="x"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMBIND>
<om:OMV name="/F/2/v"></om:OMV>
......@@ -76,7 +76,7 @@
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#949.31.16:981.31.48"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#950.31.17:950.31.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#952.31.19:952.31.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#726.23.18:729.23.21"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="x"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#950.31.17:950.31.17"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV><om:OMV name="y"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#952.31.19:952.31.19"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#955.31.22:981.31.48"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#955.31.22:961.31.28"/></metadata>
......
......@@ -8,7 +8,7 @@
<om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="_"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="/A/1/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMBIND>
<om:OMV name="/A/1/v"></om:OMV>
......@@ -41,10 +41,18 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#457.15.2:511.15.56"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#468.15.13:492.15.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#469.15.14:469.15.14"/></metadata><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="A"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#469.15.14:469.15.14"/></metadata><type><om:OMBIND>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="/A/1/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="/A/1/v"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMBIND>
<om:OMV name="/A/1/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#472.15.17:492.15.37"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#472.15.17:478.15.23"/></metadata>
......@@ -78,15 +86,15 @@
<om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#285.8.19:288.8.22"/></metadata></om:OMS>
<om:OMBVAR><om:OMV name="c"><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"></om:OMS>
</om:OMBIND>
<om:OMV name="/A/2/v"></om:OMV>
</om:OMA>
</om:OMBIND></type></om:OMV></om:OMBVAR>
<om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#531.17.17:557.17.43"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="Pi"></om:OMS>
<om:OMBVAR><om:OMV name="c"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#532.17.18:532.17.18"/></metadata><type><om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMBVAR><om:OMV name="c"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#532.17.18:532.17.18"/></metadata><type><om:OMV name="/A/2/d"></om:OMV></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#535.17.21:557.17.43"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#535.17.21:541.17.27"/></metadata>
......
......@@ -7,7 +7,7 @@
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#218.7.2:264.7.48"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#227.7.11:246.7.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#227.7.11:239.7.23"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#235.7.19:238.7.22"/></metadata></om:OMS>
</om:OMA><om:OMS base="http://cds.omdoc.org/examples" module="PL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#243.7.27:246.7.30"/></metadata></om:OMS>
......
......@@ -77,11 +77,11 @@
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="nil"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="a"><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="m"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#850.23.23:855.23.28"/></metadata>
<om:OMBVAR><om:OMV name="a/r"><type><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"></om:OMS></type></om:OMV><om:OMV name="m/r"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#850.23.23:855.23.28"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="list"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#855.23.28:855.23.28"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="list"></om:OMS><om:OMV name="a/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#855.23.28:855.23.28"/></metadata></om:OMV>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#855.23.28:855.23.28"/></metadata></om:OMV>
<om:OMV name="a/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#855.23.28:855.23.28"/></metadata></om:OMV>
</om:OMBIND>
<om:OMV name="a"></om:OMV><om:OMV name="m"></om:OMV>
</om:OMA>
......@@ -106,16 +106,16 @@
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Equality" name="equal"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#802.22.33:807.22.38"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="list"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#894.24.23:894.24.23"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="list"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#905.24.34:905.24.34"/></metadata></om:OMV>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#919.24.48:928.24.57"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="append"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#894.24.23:894.24.23"/></metadata></om:OMV><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#919.24.48:924.24.53"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="append"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#905.24.34:905.24.34"/></metadata></om:OMV><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#919.24.48:924.24.53"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="cons"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#894.24.23:894.24.23"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#920.24.49:920.24.49"/></metadata></om:OMV><om:OMV name="l"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#923.24.52:923.24.52"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="cons"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#905.24.34:905.24.34"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#920.24.49:920.24.49"/></metadata></om:OMV><om:OMV name="l"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#923.24.52:923.24.52"/></metadata></om:OMV>
</om:OMA><om:OMV name="m"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#928.24.57:928.24.57"/></metadata></om:OMV>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#932.24.61:942.24.71"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="cons"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#894.24.23:894.24.23"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#932.24.61:932.24.61"/></metadata></om:OMV><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#936.24.65:942.24.71"/></metadata>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="cons"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#905.24.34:905.24.34"/></metadata></om:OMV><om:OMV name="x"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#932.24.61:932.24.61"/></metadata></om:OMV><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#936.24.65:942.24.71"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Lists" name="append"></om:OMS><om:OMV name="a"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#905.24.34:905.24.34"/></metadata></om:OMV><om:OMV name="l"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#937.24.66:937.24.66"/></metadata></om:OMV><om:OMV name="m"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/shallow_polymorphism.mmt#941.24.70:941.24.70"/></metadata></om:OMV>
</om:OMA>
......
......@@ -205,7 +205,7 @@
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="equal"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#1182.42.23:1186.42.27"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="plus"></om:OMS><om:OMV name="X"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#1182.42.23:1182.42.23"/></metadata></om:OMV><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="zero"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#1186.42.27:1186.42.27"/></metadata></om:OMS>
</om:OMA><om:OMV name="X"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#1046.39.31:1050.39.35"/></metadata></om:OMV>
</om:OMA><om:OMV name="X"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#1038.39.23:1042.39.27"/></metadata></om:OMV>
</om:OMA>
</om:OMA>
</om:OMBIND></om:OMOBJ></type>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -380,14 +380,14 @@
<om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="Elem"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="A"><type><om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="set"></om:OMS></type></om:OMV><om:OMV name="F"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3595.63.24:3606.63.35"/></metadata>
<om:OMBVAR><om:OMV name="A/r"><type><om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="set"></om:OMS></type></om:OMV><om:OMV name="F/r"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3595.63.24:3606.63.35"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3595.63.24:3600.63.29"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="Elem"></om:OMS><om:OMV name="A"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3600.63.29:3600.63.29"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="Elem"></om:OMS><om:OMV name="A/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3600.63.29:3600.63.29"/></metadata></om:OMV>
</om:OMA><om:OMS base="http://cds.omdoc.org/examples" module="Sets" name="set"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3604.63.33:3606.63.35"/></metadata></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMV name="A"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3600.63.29:3600.63.29"/></metadata></om:OMV>
<om:OMV name="A/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/set.mmt#3600.63.29:3600.63.29"/></metadata></om:OMV>
</om:OMBIND>
<om:OMV name="A"></om:OMV><om:OMV name="F"></om:OMV>
</om:OMA>
......
......@@ -74,7 +74,7 @@
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMA>
<om:OMBVAR><om:OMV name="x/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
......@@ -221,7 +221,7 @@
</om:OMA></type></om:OMV><om:OMV name="y/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMA>
<om:OMBVAR><om:OMV name="x/r/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
......@@ -276,9 +276,19 @@
<om:OMBVAR><om:OMV name="x/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="y/r"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
</om:OMA></type></om:OMV><om:OMV name="y/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x/r/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#265.7.27:265.7.27"/></metadata></om:OMS>
</om:OMA>
</om:OMBIND>
<om:OMV name="x/r"></om:OMV>
</om:OMA></type></om:OMV><om:OMV name="z/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
......@@ -319,6 +329,25 @@
<om:OMBVAR><om:OMV name="c"><metadata><tag property="http://cds.omdoc.org/mmt?mmt?inferred-type"/><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#2044.-1.53:2044.-1.53"/></metadata><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#4207.82.16:4210.82.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="y/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x/r/r"><type><om:OMA>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#265.7.27:265.7.27"/></metadata></om:OMS>
</om:OMA>
</om:OMBIND>
<om:OMV name="x/r"></om:OMV>
</om:OMA></type></om:OMV><om:OMV name="z/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="x"><type><om:OMA>
......@@ -327,9 +356,13 @@
</om:OMA></type></om:OMV><om:OMV name="y"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#265.7.27:265.7.27"/></metadata></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="z"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#3531.70.27:3534.70.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#265.7.27:265.7.27"/></metadata></om:OMS>
</om:OMA>
</om:OMBIND>
<om:OMV name="x/r"></om:OMV><om:OMV name="y/r"></om:OMV>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="Semigroup" name="u"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/2-algebra.mmt#258.7.20:258.7.20"/></metadata></om:OMS>
</om:OMBIND>
......
......@@ -640,17 +640,30 @@
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="s"><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="sort"></om:OMS></type></om:OMV><om:OMV name="A"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6863.148.30"/></metadata>
<om:OMBVAR><om:OMV name="s/r"><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="sort"></om:OMS></type></om:OMV><om:OMV name="A/r"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6863.148.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6856.148.23"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMV name="s"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMV name="s/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
</om:OMA><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6860.148.27:6863.148.30"/></metadata></om:OMS>
</om:OMA></type></om:OMV><om:OMV name="c"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6856.148.23"/></metadata>
</om:OMA></type></om:OMV><om:OMV name="c/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="s/r/r"><type><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="sort"></om:OMS></type></om:OMV><om:OMV name="A/r/r"><type><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6863.148.30"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6856.148.23"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMV name="s"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMV name="s/r/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
</om:OMA><om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="prop"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6860.148.27:6863.148.30"/></metadata></om:OMS>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6853.148.20:6856.148.23"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples/tutorial" module="FOL" name="term"></om:OMS><om:OMV name="s/r/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
</om:OMA>
</om:OMBIND>
<om:OMV name="s/r"></om:OMV><om:OMV name="A/r"></om:OMV>
</om:OMA></type></om:OMV></om:OMBVAR>
<om:OMV name="s"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
<om:OMV name="s/r"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/tutorial/1-sfol.mmt#6856.148.23:6856.148.23"/></metadata></om:OMV>
</om:OMBIND>
<om:OMV name="s"></om:OMV><om:OMV name="A"></om:OMV><om:OMV name="c"></om:OMV>
</om:OMA>
......
......@@ -32,7 +32,14 @@
<om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="STT" name="apply"></om:OMS><om:OMV name="A"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#967.39.38:967.39.38"/></metadata></om:OMV><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="A/r"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"></om:OMS></type></om:OMV><om:OMV name="B/r"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#594.25.13:595.25.14"/></metadata></om:OMS></type></om:OMV><om:OMV name="F/r"><type><om:OMA>
<om:OMBVAR><om:OMV name="A/r"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"></om:OMS></type></om:OMV><om:OMV name="B/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="A"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"></om:OMS></type></om:OMV></om:OMBVAR>
<om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#594.25.13:595.25.14"/></metadata></om:OMS>
</om:OMBIND>
<om:OMV name="A/r"></om:OMV>
</om:OMA></type></om:OMV><om:OMV name="F/r"><type><om:OMA>
<om:OMBIND>
<om:OMS base="http://cds.omdoc.org/mmt" module="mmt" name="free"></om:OMS>
<om:OMBVAR><om:OMV name="A"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"></om:OMS></type></om:OMV><om:OMV name="B"><type><om:OMS base="http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final" module="Types" name="tp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/IFIP21_tutorial.mmt#594.25.13:595.25.14"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
......
<errors>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?NatMinus?minus_inverse?definition: Judgment |- [X]trans minus_pi minus_intro_R plus_neut_Ex X : {X}⊦X-X!leq_refl =O" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:90)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:89)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:89)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:86)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:39)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: http://cds.omdoc.org/examples?NatMinus?minus_inverse?definition: Judgment |- [X]trans minus_pi minus_intro_R plus_neut_Ex X : {X}⊦X-X!leq_refl =O" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:90)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15$adapted(RuleBasedChecker.scala:89)</element>
<element>scala.collection.immutable.List.foreach(List.scala:389)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$13(RuleBasedChecker.scala:89)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:86)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16(MMTStructureChecker.scala:301)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$16$adapted(MMTStructureChecker.scala:277)</element>
<element>scala.Option.foreach(Option.scala:257)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:277)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:72)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:87)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:99)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:484)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:636)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:462)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:715)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:715)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:410)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:186)</element>
<element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
<element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
<element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:235)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:186)</element>
<element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:176)</element>
<element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:93)</element>
<element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:45)</element>
<element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:39)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:548)</element>
<element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
<element>info.kwarc.mmt.api.archives.BuildQueue$$anon$1.run(BuildQueue.scala:262)</element>
</stacktrace>
</error>
</errors>
......@@ -79,7 +79,7 @@ theory NatMinus : http://cds.omdoc.org/urtheories?LF =
include ?NatRules ❙
include ?NatRules/NatOnly❙
// A partial subtraction operation that takes a proof of definedness as a 3rd arguments. ❙
// A partial subtraction operation that takes a proof of definedness as a 3rd argument. ❙
minus : {X,Y} ⊦ Y≤X ⟶ nat ❘ # 1 - 2 ! 3 prec 15 ❘ ## 1 - 2 %I3❙
minus_pi : {X,Y,P,Q} ⊦ X-Y!P = X-Y!Q ❙
......@@ -89,7 +89,7 @@ theory NatMinus : http://cds.omdoc.org/urtheories?LF =
minus_elim : {X,Y,Z,P} ⊦ Z-Y!P = X ⟶ ⊦ X+Y = Z ❙
minus_inverse : {X} ⊦ X-X!leq_refl = O ❘
// minus_inverse : {X} ⊦ X-X!leq_refl = O ❘
= [X] trans minus_pi (minus_intro_R (plus_neut_Ex X)) ❙
// minus_neut : {X} ⊦ X-O!least = X ❘
= [X] trans minus_pi (minus_intro_L (plus_neut_Ex X)) ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment