Newer
Older
namespace http://mathhub.info/FrameIT/frameworld/integrationtests ❚
import frameworld http://mathhub.info/FrameIT/frameworld ❚
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
theory SampleSituationSpace =
theory Root =
// planar triangle in R^2 ❙
include ☞frameworld:?OppositeLen ❙
include ☞frameworld:?AngleSum ❙
A
: point ❘
= ⟨0.0, 0.0, 0.0⟩ ❘
meta frameworld:?MetaAnnotations?label "𝔸"
❙
B
: point ❘
= ⟨3.0, 3.0, 0.0⟩ ❘
meta frameworld:?MetaAnnotations?label "𝔹"
❙
C
: point ❘
= ⟨0.0, 3.0, 0.0⟩ ❘
meta frameworld:?MetaAnnotations?label "ℂ"
❙
distanceBC
: Σ x:ℝ. ⊦ (d- B C ≐ x) ❘
= ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ❘
meta frameworld:?MetaAnnotations?label "𝔹ℂ"
❙
angleABC
: Σ β:ℝ. ⊦ ( ∠ A,B,C ) ≐ β ❘
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
meta frameworld:?MetaAnnotations?label "∠𝔸𝔹ℂ"
❙
angleBAC
: Σ β:ℝ. ⊦ ( ∠ B,A,C ) ≐ β ❘
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ❘
meta frameworld:?MetaAnnotations?label "∠ℬ𝔸ℂ"
❙
rightAngledC
: ⊦ ( ∠ B,C,A ) ≐ 90.0 ❘
= sketch "calculated by ComFreek by hand, hopefully correct" ❘
meta frameworld:?MetaAnnotations?label "∟ℂ"
❙
❚
❚
theory MyScroll =
theory Problem = a: type ❙❚
theory Solution =
include ?MyScroll/Problem ❙
c: type ❘ = a❙
❚
theory SituationSpace =
theory RootSituationTheory =
include ?MyScroll ❙
b: type ❙
view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
a = b ❙
❚
❚
theory PushedOutSituationTheory =
include ?SituationSpace/RootSituationTheory ❙
view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
a = c ❙
❚