bug repro

errors/mmt-omdoc/IntegrationTests/ExpectedTypeTests.mmt.err

-<errors>
-</errors>

narration/IntegrationTests/ExpectedTypeTests.omdoc

 <?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#0.0.0:634.21.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://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#441.10.0:472.10.31"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#0.0.0:741.26.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://mathhub.info/FrameIT/frameworld/integrationtests"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#441.10.0:470.10.29"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.mmt#564.17.0:595.17.31"/></metadata></mref></omdoc>
\ No newline at end of file

relational/IntegrationTests/ExpectedTypeTests.rel

 document http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain
 Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/ExpectedTypeTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain

relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.rel

-dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
-dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
-dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
-dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC
 dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
 dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?one_half
 dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleComplexExpression
 theory http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain
 HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld?FrameworldMeta
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
-constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
-constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
-constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
-Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
-constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v
-DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?pangleABC_v?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codA?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codB?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?codC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
 Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
 constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin
 DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Codomain?arcsin?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type

relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.rel

+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C
+dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC
+theory http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?ExpectedTypeTest_Domain?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type

source/IntegrationTests/ExpectedTypeTests.mmt

@@ -8,12 +8,17 @@ namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
 
 fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
 
-theory ExpectedTypeTest_Codomain =
-    pA: point ❙
-    pB: point ❙
-    pC: point ❙
+theory ExpectedTypeTest_Domain =
+    A: point ❙
+    B: point ❙
+    C: point ❙
+    angleABC: Σ a:ℝ . ⊦ ( ∠ A,B,C ) ≐ a ❙
+❚
 
-    pangleABC_v: ℝ ❙
+theory ExpectedTypeTest_Codomain =
+    codA: point ❙
+    codB: point ❙
+    codC: point ❙
 
     arcsin: ℝ ⟶ ℝ ❙
     one_half: ℝ ❙

source/IntegrationTests/SituationTheory.mmt

@@ -32,6 +32,12 @@ theory SampleSituationTheory =
    angleABC
         : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
         = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
-                meta ?MetaAnnotations?label "distanceBC"
+        meta ?MetaAnnotations?label "distanceBC"
+   ❙
+
+   angleBAC
+        : Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
+        = ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
+        meta ?MetaAnnotations?label "distanceBC"
    ❙
 ❚