TriangleScroll.mmt

namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚

theory TriangleScroll =
    meta ?MetaAnnotations?problemTheory  ?TriangleScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?TriangleScroll/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"
        ❙
        // D: point
            ❘ meta ?MetaAnnotations?label "D"
            ❘ meta ?MetaAnnotations?description "The fourth point"
        ❙
        // dAB: Σ x:ℝ . ⊦ (d- A B) ≐ x
         ❘ meta ?MetaAnnotations?label s"d${lverb A B}"
         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb A} to point ${lverb B}"
        ❙
        // dDC: Σ x:ℝ . ⊦ (d- D C) ≐ x
         ❘ meta ?MetaAnnotations?label s"d${lverb D C}"
         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb D} to point ${lverb C}"
        ❙
        // rADC: ⊦ (∠ A,D,C) ≐ 90.0
         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb A D C}, where ${lverb D} is the point enclosed by ${lverb A} and ${lverb C}"
        ❙
    ❚

    theory Solution =
        include ?TriangleScroll/Problem ❙

        meta ?MetaAnnotations?label "Triangle" ❙
        meta ?MetaAnnotations?description s"Scrolls that takes three points and constructs a triangle." ❙

        ConstructedTriangle : Triangle
                ❘ = TriangleCons A B C
                ❘ meta ?MetaAnnotations?label s"Triangle"
                ❘ meta ?MetaAnnotations?description s"The constructed Triangle."
        ❙
    ❚
❚