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 SimpleCircleScroll =
meta ?MetaAnnotations?problemTheory ?SimpleCircleScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?SimpleCircleScroll/Solution ❙
theory Problem =
M: point
❘ meta ?MetaAnnotations?label "M"
❘ meta ?MetaAnnotations?description "The midpoint of the circle"
❙
A: point
❘ meta ?MetaAnnotations?label "A"
❘ meta ?MetaAnnotations?description "The edge point of the circle"
❙
B: point
❘ meta ?MetaAnnotations?label "T"
❘ meta ?MetaAnnotations?description "A point on the plane of the circle"
❙
❚
theory Solution =
include ?SimpleCircleScroll/Problem ❙
meta ?MetaAnnotations?label "Circle" ❙
meta ?MetaAnnotations?description s"Takes a midpoint, a point on the edge of the circle and a point on the plane of it to construct a circle" ❙
ConstructedCircle : Circle
❘ = ( CircleCons M A B )
❘ meta ?MetaAnnotations?label s"Circle"
❘ meta ?MetaAnnotations?description s"The constructed circle"
❙
❚
❚