Newer
Older
1
2
3
4
5
6
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
namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚
theory CylinderScroll =
meta ?MetaAnnotations?problemTheory ?CylinderScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?CylinderScroll/Solution ❙
theory Problem =
M: point
❘ meta ?MetaAnnotations?label "M"
❘ meta ?MetaAnnotations?description "The point in the middle of the bottom circle-plane"
❙
E: point
❘ meta ?MetaAnnotations?label "E"
❘ meta ?MetaAnnotations?description "The point on the edge of the bottom-circle-plane"
❙
P: point
❘ meta ?MetaAnnotations?label "P"
❘ meta ?MetaAnnotations?description "A point in the bottom-circle-plane"
❙
T: point
❘ meta ?MetaAnnotations?label "T"
❘ meta ?MetaAnnotations?description "The point directly above the point M"
❙
❚
theory Solution =
include ?CylinderScroll/Problem ❙
meta ?MetaAnnotations?label "Cylinder" ❙
meta ?MetaAnnotations?description s"Given four points: Three points that form the bottom-plane and one directly above this scroll constructs a cylinder" ❙
ConstructedCylinder: Cylinder
❘ = ( CylinderCons M E P T )
❘ meta ?MetaAnnotations?label s"Cylinder"
❘ meta ?MetaAnnotations?description s"The constructed Cylinder."
❙
❚
❚