CuboidScroll.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 CuboidScroll =
    meta ?MetaAnnotations?problemTheory  ?CuboidScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?CuboidScroll/Solution ❙
    theory Problem =

        R: Rectangle
         ❘ meta ?MetaAnnotations?label "R"
         ❘ meta ?MetaAnnotations?description "The given rectangle"
        ❙
        T: point
         ❘ meta ?MetaAnnotations?label "T"
         ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
        ❙

        
    ❚
    theory Solution =
        include ?CuboidScroll/Problem ❙
        meta ?MetaAnnotations?label "Cuboid" ❙
        meta ?MetaAnnotations?description s"Given a rectangle and a top point that lies above the point in the center of the right-angle formed by the squarepoints
                                            this scroll constructs a cuboid. Additionally you need a proof that there are two right angles between TBC and TBA" ❙
        ConstructedCuboid : Cuboid
                ❘ = ( CuboidCons R T )
                ❘ meta ?MetaAnnotations?label s"Cuboid"
                ❘ meta ?MetaAnnotations?description s"The constructed Cuboid."
        ❙
    ❚
❚