...
 
Commits (5)
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://docs.omdoc.org/urtheories/module-expressions.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#0.0.0:2699.97.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/urtheories"/><instruction text="import example http://cds.omdoc.org/examples"/><instruction text="import rules scala://moduleexpressions.mmt.kwarc.info"/><instruction text="import operators scala://operators.moduleexpressions.mmt.kwarc.info"/><instruction text="import metaops scala://meta.operators.moduleexpressions.mmt.kwarc.info"/><mref name="[http://cds.omdoc.org/urtheories?ModExp]" target="http://cds.omdoc.org/urtheories?ModExp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#287.7.0:299.7.12"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?Combinators]" target="http://cds.omdoc.org/urtheories?Combinators"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#983.38.0:1000.38.17"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LFComb]" target="http://cds.omdoc.org/urtheories?LFComb"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#2644.93.0:2656.93.12"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://docs.omdoc.org/urtheories/module-expressions.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#0.0.0:2192.82.0"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://cds.omdoc.org/urtheories"/><instruction text="import rules scala://moduleexpressions.mmt.kwarc.info"/><instruction text="import operators scala://operators.moduleexpressions.mmt.kwarc.info"/><instruction text="import typeops scala://typeops.operators.moduleexpressions.mmt.kwarc.info"/><mref name="[http://cds.omdoc.org/urtheories?ModExp]" target="http://cds.omdoc.org/urtheories?ModExp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#244.6.0:256.6.12"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?Combinators]" target="http://cds.omdoc.org/urtheories?Combinators"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#809.28.0:826.28.17"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?LFComb]" target="http://cds.omdoc.org/urtheories?LFComb"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#2061.72.0:2073.72.12"/></metadata></mref><mref name="[http://cds.omdoc.org/urtheories?SFOLEQComb]" target="http://cds.omdoc.org/urtheories?SFOLEQComb"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://docs.omdoc.org/urtheories/module-expressions.mmt#2117.77.0:2133.77.16"/></metadata></mref></omdoc>
\ No newline at end of file
......@@ -5,23 +5,17 @@ untypedconstant http://cds.omdoc.org/urtheories?Combinators?rename
untypedconstant http://cds.omdoc.org/urtheories?Combinators?combine
untypedconstant http://cds.omdoc.org/urtheories?Combinators?translate
untypedconstant http://cds.omdoc.org/urtheories?Combinators?hom
untypedconstant http://cds.omdoc.org/urtheories?Combinators?single_typeindexifier
untypedconstant http://cds.omdoc.org/urtheories?Combinators?multi_typeindexifier
untypedconstant http://cds.omdoc.org/urtheories?Combinators?fol_typifier
untypedconstant http://cds.omdoc.org/urtheories?Combinators?pushout_inclusion
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_accessor
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_from_file
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_union
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_difference_by_label
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_prefix
untypedconstant http://cds.omdoc.org/urtheories?Combinators?diagram_closure
theory http://cds.omdoc.org/urtheories?Combinators
Includes http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?ModExp
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?empty
constant http://cds.omdoc.org/urtheories?Combinators?empty
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeEmpty]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeEmpty]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?extends
constant http://cds.omdoc.org/urtheories?Combinators?extends
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeExtends]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeExtends]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?rename1
constant http://cds.omdoc.org/urtheories?Combinators?rename1
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?rename
......@@ -38,33 +32,15 @@ Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheo
constant http://cds.omdoc.org/urtheories?Combinators?hom
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://operators.moduleexpressions.mmt.kwarc.info?ComputeHom]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://operators.moduleexpressions.mmt.kwarc.info?ComputeHom]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?single_typeindexifier
constant http://cds.omdoc.org/urtheories?Combinators?single_typeindexifier
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?multi_typeindexifier
constant http://cds.omdoc.org/urtheories?Combinators?multi_typeindexifier
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?fol_typifier
constant http://cds.omdoc.org/urtheories?Combinators?fol_typifier
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?pushout_inclusion
constant http://cds.omdoc.org/urtheories?Combinators?pushout_inclusion
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://operators.moduleexpressions.mmt.kwarc.info?ComputePushoutAlongInclusion]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://operators.moduleexpressions.mmt.kwarc.info?ComputePushoutAlongInclusion]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_accessor
constant http://cds.omdoc.org/urtheories?Combinators?diagram_accessor
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramAccess]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramAccess]
Includes http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Strings
Includes http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?LF
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_from_file
constant http://cds.omdoc.org/urtheories?Combinators?diagram_from_file
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramFromFile]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramFromFile]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_union
constant http://cds.omdoc.org/urtheories?Combinators?diagram_union
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramUnion]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramUnion]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_difference_by_label
constant http://cds.omdoc.org/urtheories?Combinators?diagram_difference_by_label
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramDifferenceByLabel]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramDifferenceByLabel]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_prefix
constant http://cds.omdoc.org/urtheories?Combinators?diagram_prefix
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputePrefixedDiagram]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputePrefixedDiagram]
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?diagram_closure
constant http://cds.omdoc.org/urtheories?Combinators?diagram_closure
Declares http://cds.omdoc.org/urtheories?Combinators http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramClosure]
constant http://cds.omdoc.org/urtheories?Combinators?[scala://meta.operators.moduleexpressions.mmt.kwarc.info?ComputeDiagramClosure]
theory http://cds.omdoc.org/urtheories?LFComb
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?LF
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?TermsTypesKinds
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/mmt?Errors
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?ModExp
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/mmt?mmt
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?Typed
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?Kinded
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?TypedConstants
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?KindedConstants
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?LambdaPi
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?LFRules
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?Combinators
Includes http://cds.omdoc.org/urtheories?LFComb http://cds.omdoc.org/urtheories?Strings
theory http://cds.omdoc.org/urtheories?SFOLEQComb
Includes http://cds.omdoc.org/urtheories?SFOLEQComb http://cds.omdoc.org/examples?SFOLEQ
......@@ -10,7 +10,7 @@ theory ModExp =
constant morphism # MOR 1 2❙
constant diagram # DIAG ❙
complextheory # {| L1Td,… |} prec -1000005❙
complextheory # {| %BL1T,… |} prec -1000005❙
complexmorphism # [| L1D,… |] prec -1000005❙
identity # IDENTITY 1 prec -1❙
......