Commit 83acccfb authored by Florian Rabe's avatar Florian Rabe

no message

parent 1191aa1e
......@@ -92,8 +92,9 @@ end
define temp2
server on 8080
log+ server
//log+ debug
log+ debug
log+ object-checker
log+ subtype-rule-gen
//log+ object-simplifier
//log+ structure-simplifier
//log+ structure-checker
......@@ -101,11 +102,11 @@ define temp2
mathpath archive ../LFX
mathpath archive ../../MitM
//log+ backend
extension info.kwarc.mmt.lf.induction.InductiveTypes
extension info.kwarc.mmt.lf.structuralfeatures.InductiveTypes
log+ InductiveTypes
mathpath archive ../../Test/General
extension info.kwarc.mmt.odk.Plugin
build MMT/LFX mmt-omdoc
// build MMT/examples mmt-omdoc
build MMT/examples mmt-omdoc inductive.mmt
end
define MMTTest
......
This diff is collapsed.
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Bool" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#42.2.0:142.6.0"/></metadata><constant name="bool">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#95.3.2:107.3.14"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#103.3.10:106.3.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="true">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#111.4.2:123.4.14"/><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:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#119.4.10:122.4.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="false">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#127.5.2:140.5.15"/><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:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#136.5.11:139.5.14"/></metadata></om:OMS></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLEQ" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#640.21.0:755.24.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#694.22.2:706.22.14"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="equal">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#710.23.2:753.23.45"/><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#719.23.11:736.23.28"/></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="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: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#733.23.25:736.23.28"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="30" fixity="mixfix" arguments="1 ≐ 2"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLPatterns" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LFS"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#42.2.0:151.8.0"/></metadata><import from="http://cds.omdoc.org/examples?FOL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#75.3.2:87.3.14"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><derived feature="pattern" name="fun" base="http://cds.omdoc.org/examples"><type><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#102.5.10:112.5.20"/></metadata>
<om:OMS base="scala://patterns.api.mmt.kwarc.info/" module="PatternFeature"></om:OMS>
<om:OMBVAR><om:OMV name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#106.5.14:106.5.14"/></metadata><type><om:OMS base="http://cds.omdoc.org/urtheories" module="NatSymbols" name="NAT"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#108.5.16:110.5.18"/></metadata></om:OMS></type></om:OMV></om:OMBVAR>
</om:OMBIND></type><notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="L1 : 2"> <scope languages="" priority="0"/> </notation></notations><constant name="f">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#129.6.4:145.6.20"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></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/patterns.mmt#132.6.7:144.6.19"/></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/patterns.mmt#132.6.7:137.6.12"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="Sequences" name="rep"></om:OMS>
<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/patterns.mmt#132.6.7:135.6.10"/></metadata></om:OMS><om:OMV name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/patterns.mmt#137.6.12:137.6.12"/></metadata></om:OMV>
</om:OMA><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/patterns.mmt#141.6.16:144.6.19"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></derived></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#501.28.0:754.33.0"/></metadata><import from="http://cds.omdoc.org/examples?FOLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#559.29.2:577.29.20"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="FOL" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#135.4.0:316.9.0"/></metadata><import from="http://cds.omdoc.org/examples?PL"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#187.5.2:198.5.13"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="term">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#202.6.2:214.6.14"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#210.6.10:213.6.13"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="forall">
<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><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>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="∀ 1"> <scope languages="" priority="0"/> </notation><notation dimension="2" precedence="0" fixity="mixfix" arguments="∀ V1 2"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="exists">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/fol.mmt#268.8.2:314.8.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#277.8.11:296.8.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/logic/fol.mmt#277.8.11:289.8.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#285.8.19:288.8.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#293.8.27:296.8.30"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="0" fixity="mixfix" arguments="∃ 1"> <scope languages="" priority="0"/> </notation><notation dimension="2" precedence="0" fixity="mixfix" arguments="∃ V1 2"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="IntLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#315.13.0:581.18.0"/></metadata><import from="http://cds.omdoc.org/examples?IntRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#375.14.2:392.14.19"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#500.15.2:518.15.20"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?StandardInt"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#522.16.2:547.16.27"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="test">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#551.17.2:579.17.30"/></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/literals.mmt#559.17.10:568.17.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#561.17.12:568.17.19"/></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="equal"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#561.17.12:563.17.14"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Int" name="minus"></om:OMS><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="1"/><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="3"/>
</om:OMA><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#567.17.18:568.17.19"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Int" name="uminus"></om:OMS><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="2"/>
</om:OMA>
</om:OMA>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="trueI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#574.17.25:578.17.29"/></metadata></om:OMS></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Int" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#42.2.0:267.8.0"/></metadata><import from="http://cds.omdoc.org/examples?Nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#94.3.2:106.3.14"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="int">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#110.4.2:129.4.21"/></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#118.4.10:121.4.13"/></metadata></om:OMS></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#126.4.18:128.4.20"/></metadata></om:OMS></om:OMOBJ></definition>
</constant><constant name="pred">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#133.5.2:175.5.44"/><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/int.mmt#141.5.10:149.5.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#141.5.10:143.5.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#147.5.16:149.5.18"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="20" fixity="mixfix" arguments="pred 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="uminus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#179.6.2:219.6.42"/><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/int.mmt#187.6.10:195.6.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#187.6.10:189.6.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#193.6.16:195.6.18"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="20" fixity="mixfix" arguments="- 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="minus">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#223.7.2:265.7.44"/><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/int.mmt#231.7.10:245.7.24"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#231.7.10:233.7.12"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#237.7.16:239.7.18"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Nat" name="nat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/int.mmt#243.7.22:245.7.24"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="10" fixity="mixfix" arguments="1 - 2"> <scope languages="" priority="0"/> </notation></notations>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="LFI" base="http://cds.omdoc.org/examples"><metadata><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><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#94.4.0:155.7.0"/></metadata><import from="http://cds.omdoc.org/urtheories?LF"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#110.5.2:124.5.16"/><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></import><ruleconstant name="[scala://induction.lf.mmt.kwarc.info?InductiveTypes]"><type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="scala://induction.lf.mmt.kwarc.info" module="InductiveTypes"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#133.6.7:152.6.26"/></metadata></om:OMS></om:OMOBJ></type></ruleconstant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="Logic" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#145.8.0:286.12.0"/></metadata><import from="http://cds.omdoc.org/examples?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#199.9.2:212.9.15"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="ded" role="Judgment">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#216.10.2:266.10.52"/><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="Kinded" name="kind"></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/nat.mmt#224.10.10:234.10.20"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#224.10.10:227.10.13"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#231.10.17:234.10.20"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
<notations><notation dimension="1" precedence="-5" fixity="mixfix" arguments="⊦ 1"> <scope languages="" priority="0"/> </notation></notations>
</constant><constant name="trueI">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#270.11.2:284.11.16"/><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/nat.mmt#278.11.10:283.11.15"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="ded"></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="Bool" name="true"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/nat.mmt#280.11.12:283.11.15"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatExample" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/examples?LFI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#158.9.0:246.15.0"/></metadata><derived feature="inductive" name="nat" base="http://cds.omdoc.org/examples"><type><om:OMBIND><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#197.10.12:202.10.17"/></metadata>
<om:OMS base="scala://induction.lf.mmt.kwarc.info/" module="InductiveTypes"></om:OMS>
<om:OMBVAR></om:OMBVAR>
</om:OMBIND></type><constant name="n">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#209.11.4:216.11.11"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/urtheories" module="Typed" name="type"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#212.11.7:215.11.10"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="z">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#222.12.4:226.12.8"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></om:OMOBJ></meta></metadata>
<type><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#225.12.7:225.12.7"/></metadata></om:OMS></om:OMOBJ></type>
</constant><constant name="s">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#232.13.4:240.13.12"/><meta property="http://gl.mathhub.info/MMT/LFX/TypedHierarchy?Symbols?TypeLevel"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMA>
<om:OMS base="http://gl.mathhub.info/MMT/LFX/TypedHierarchy" module="Symbols" name="TypeLevel"></om:OMS>
<om:OMLIT type="http://mathhub.info/MitM/Foundation?Literals?nat_lit" value="100"/>
</om:OMA></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/inductive.mmt#235.13.7:239.13.11"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="arrow"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#235.13.7:235.13.7"/></metadata></om:OMS><om:OMS base="http://cds.omdoc.org/examples" module="NatExample/nat" name="n"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/inductive.mmt#239.13.11:239.13.11"/></metadata></om:OMS>
</om:OMA></om:OMOBJ></type>
</constant></derived></theory></omdoc>
\ No newline at end of file
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="NatLiterals" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#80.4.0:310.11.0"/></metadata><import from="http://cds.omdoc.org/examples?NatRules"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#140.5.2:157.5.19"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?Bool"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#161.6.2:179.6.20"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><import from="scala://real.omdoc.org/?StandardNat"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#183.7.2:208.7.27"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><constant name="test">
<metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#282.10.2:308.10.28"/></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/literals.mmt#290.10.10:298.10.18"/></metadata>
<om:OMS base="http://cds.omdoc.org/urtheories" module="LambdaPi" name="apply"></om:OMS>
<om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="ded"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#292.10.12:298.10.18"/></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="equal"></om:OMS><om:OMA><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#292.10.12:294.10.14"/></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:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="1"/><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="1"/>
</om:OMA><om:OMLIT type="http://cds.omdoc.org/examples?Nat?nat" value="2"/>
</om:OMA>
</om:OMA></om:OMOBJ></type>
<definition><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMS base="http://cds.omdoc.org/examples" module="Logic" name="trueI"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/literals.mmt#303.10.23:307.10.27"/></metadata></om:OMS></om:OMOBJ></definition>
</constant></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
<omdoc xmlns="http://omdoc.org/ns" xmlns:om="http://www.openmath.org/OpenMath"><theory name="PLProofs" base="http://cds.omdoc.org/examples" meta="http://cds.omdoc.org/urtheories?LF"><metadata><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#293.19.0:498.26.0"/></metadata><import from="http://cds.omdoc.org/examples?PLNatDed"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#350.20.2:367.20.19"/><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="Kinded" name="kind"></om:OMS></om:OMOBJ></meta></metadata></import><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/examples/logic/prover.mmt#374.22.2:405.22.33"/></metadata>this doesn't work currently</opaque></theory></omdoc>
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -19,7 +19,7 @@ http://foswiki.cs.uu.nl/foswiki/IFIP21/Goteborg/MMT-tutorial-final?Monad?assoc
<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.Importer.buildFile(Index.scala:133)</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>
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -15,5 +15,5 @@ Declares http://cds.omdoc.org/examples?Real http://cds.omdoc.org/examples?Real?t
constant http://cds.omdoc.org/examples?Real?times
Declares http://cds.omdoc.org/examples?Real http://cds.omdoc.org/examples?Real?div
constant http://cds.omdoc.org/examples?Real?div
Declares http://cds.omdoc.org/examples?Real http://cds.omdoc.org/examples?Real?[scala://lf.mmt.kwarc.info/?Realize]/2019407922
constant http://cds.omdoc.org/examples?Real?[scala://lf.mmt.kwarc.info/?Realize]/2019407922
Declares http://cds.omdoc.org/examples?Real http://cds.omdoc.org/examples?Real?[scala://lf.mmt.kwarc.info/?Realize]/-1146036500
constant http://cds.omdoc.org/examples?Real?[scala://lf.mmt.kwarc.info/?Realize]/-1146036500
......@@ -3,8 +3,8 @@ namespace http://cds.omdoc.org/examples ❚
import rules scala://structuralfeatures.lf.mmt.kwarc.info❚
theory LFI =
include ur:?LF
rule rules?InductiveTypes
include ur:?DHOL
rule rules?InductiveTypes❙

theory NatExample : ?LFI =
......
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