Skip to content
Snippets Groups Projects
Commit dfd4f338 authored by Paul-Walcher's avatar Paul-Walcher
Browse files

Changed SquareScroll and Circle Scroll

Added additional conditions for construction:

Square: Distance AB and Distance BC, so that inuitively the area is dAB * dBC.

Circle: The distance from thew center to the edgepoint, also for providing a more intuitive way to construct circles.
parent fcd81c6d
No related branches found
No related tags found
No related merge requests found
......@@ -16,6 +16,9 @@ theory CircleScroll =
❘ meta ?MetaAnnotations?description "A point on the circle" ❙
B : point ❘ meta ?MetaAnnotations?label "B"
❘ meta ?MetaAnnotations?description "A point within the plane the circle should lie in." ❙
dMA : Σ x:ℝ . ⊦ (d- M A) ≐ x
❘ meta ?MetaAnnotations?label "dMA"
❘ meta ?MetaAnnotations?description "The distance from the Midpoint M to the edge point A" ❙
theory Solution =
......
......@@ -24,8 +24,18 @@ theory SquareScroll =
rC: ⊦ (∠ A,B,C) ≐ 90.0
❘ meta ?MetaAnnotations?label "C"
❘ meta ?MetaAnnotations?description "The third point"
❘ meta ?MetaAnnotations?label "rC"
❘ meta ?MetaAnnotations?description "A right angle between ABC, where B is the point enclosed by A and B"
dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
❘ meta ?MetaAnnotations?label "dAB"
❘ meta ?MetaAnnotations?description "The distance from point A to point B"
dBC: Σ x:ℝ . ⊦ (d- B C) ≐ x
❘ meta ?MetaAnnotations?label "dBC"
❘ meta ?MetaAnnotations?description "The distance from point B to point C"
......@@ -35,11 +45,12 @@ theory SquareScroll =
theory Solution =
include ?SquareScroll/Problem ❙
meta ?MetaAnnotations?label "Square" ❙
meta ?MetaAnnotations?description s"Our Test scroll that given two points ${lverb P} and ${lverb Q} computes the Test of the line ${lverb P Q}." ❙
meta ?MetaAnnotations?description s"Scrolls that takes three points and given a right-angle fact between those points
and the distances from the first to the second and the second to the third point, constructs a rectangle." ❙
ConstructedSquare : Square
❘ = SquareCons A B C
❘ meta ?MetaAnnotations?label s"Mid[${lverb P Q}]"
❘ meta ?MetaAnnotations?description s"The Test between points ${lverb P} and ${lverb Q}."
❘ meta ?MetaAnnotations?label s"Square"
❘ meta ?MetaAnnotations?description s"The constructed Square."
\ No newline at end of file
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