Skip to content
Snippets Groups Projects
Commit 2f880703 authored by ComFreek's avatar ComFreek
Browse files

add integration tests for closeGaps

parent bede8bb7
No related branches found
No related tags found
No related merge requests found
<errors>
</errors>
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#0.0.0:295.9.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?FactCollection"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#134.4.0:161.4.27"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#0.0.0:632.22.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?FactCollection"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#134.4.0:162.4.28"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.mmt#297.10.0:329.10.32"/></metadata></mref></omdoc>
\ No newline at end of file
document http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc
Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapTest_Codomain
Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain
Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/CloseGapTests.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact
theory http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain
HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain http://mathhub.info/FrameIT/frameworld?FactCollection
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld?AngleFact?angleFact?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld?AngleFact?angleFact?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?complexAngleFact?type http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pA
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pB
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC
dataconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v
datatypeconstructor http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pdistBC_v
theory http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad
HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld?FactCollection
Includes http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pA
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pA
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pA?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pB
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pB
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pB?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pB?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?definition
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?b?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_Codomain?a?definition
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pangleABC_v?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pdistBC_v
constant http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pdistBC_v
DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?CloseGapsTest_TermsNotepad?expected_gap_pdistBC_v?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
......@@ -2,8 +2,21 @@ namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
fixmeta http://mathhub.info/FrameIT/frameworld?FactCollection ❚
theory CloseGapTest_Codomain =
theory CloseGapsTest_Codomain =
a: ℝ ❘ = 42.0 ❙
b: ℝ ❘ = 4242.0 ❙
complexAngleFact : angleFact ⟨1.0, 2.0, 3.0⟩ ⟨4.0, 5.0, 6.0⟩ ⟨a, b, 0.0⟩ (90.0) ❙
theory CloseGapsTest_TermsNotepad =
include ?CloseGapsTest_Codomain ❙
// First simple test ❙
expected_gap_pA = ⟨1.0, 2.0, 3.0⟩ ❙
expected_gap_pB = ⟨4.0, 5.0, 6.0⟩ ❙
expected_gap_pC = ⟨a, b, 0.0⟩ ❙
expected_gap_pangleABC_v = 90.0 ❙
// Second test involving closeAndInfer ❙
expected_gap_pdistBC_v = ℝ
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment