SquareScroll.mmt

/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚

/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚


theory SquareScroll =
    meta ?MetaAnnotations?problemTheory  ?SquareScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?SquareScroll/Solution ❙
    theory Problem =
        A: point
         ❘ meta ?MetaAnnotations?label "A"
         ❘ meta ?MetaAnnotations?description "The first point"
        ❙
        B: point
         ❘ meta ?MetaAnnotations?label "B"
         ❘ meta ?MetaAnnotations?description "The second point"
        ❙
        C: point
         ❘ meta ?MetaAnnotations?label "C"
         ❘ meta ?MetaAnnotations?description "The third point"
        ❙

        rC: ⊦ (∠ A,B,C) ≐ 90.0
         ❘ 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"
        ❙


    ❙
        
    ❚
    theory Solution =
        include ?SquareScroll/Problem ❙
        meta ?MetaAnnotations?label "Square" ❙
        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"Square"
                ❘ meta ?MetaAnnotations?description s"The constructed Square."
        ❙
    ❚
❚