MiscScrolls.mmt

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

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

theory Midpoint =
    meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ❙

    theory Problem =
        P
            : point ❘
            meta ?MetaAnnotations?label "P" ❘
            meta ?MetaAnnotations?description "Some arbitrary input point"
        ❙

        Q
            : point ❘
            meta ?MetaAnnotations?label "Q" ❘
            meta ?MetaAnnotations?description "Some other arbitrary input point"
        ❙
    ❚

    theory Solution =
        include ?Midpoint/Problem ❙

        meta ?MetaAnnotations?label "MidPoint" ❙
        meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." ❙

        midpoint
            : point ❘
            = ⟨0.5 ⋅ (P _x + Q _x), 0.5 ⋅ (P _y + Q _y), 0.5 ⋅ (P _z + Q _z)⟩ ❘
            meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" ❘
            meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
        ❙
    ❚
❚