meta ?MetaAnnotations?problemTheory ?Midpoint2/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Midpoint2/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 ?Midpoint2/Problem ❙
meta ?MetaAnnotations?label "Midpoint2" ❙
meta ?MetaAnnotations?description s"Our Midpoint2 scroll that given two points ${lverb P} and ${lverb Q} computes the Midpoint2 of the line ${lverb P Q}." ❙