Skip to content
Snippets Groups Projects
Commit 82552d5f authored by Paul-Walcher's avatar Paul-Walcher
Browse files

cleanup test

parent f3e5e1ee
No related branches found
No related tags found
No related merge requests found
......@@ -121,7 +121,7 @@ theory FrameITRectangles =
// TODO maybe delete ❙
rectangle_type : type ❘ # rect ❙
testPoint_type : type ❘ # testPoint ❙
mkRectangle : { A: point , B : point, C : point , D : point } ( ⊦ isRect A B C D ) ⟶ rect ❘ # mkRect 1 2 3 4 5 ❙
cornerA : rect ⟶ point ❘ # rectA 1 ❙
......
/T Miscellaneous scrolls for playing around/testing that don't have a good home yet ❚
namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚
theory Test =
meta ?MetaAnnotations?problemTheory ?Test/Problem ❙
meta ?MetaAnnotations?solutionTheory ?Test/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 ?Test/Problem ❙
meta ?MetaAnnotations?label "Test" ❙
meta ?MetaAnnotations?description s"Our Test scroll that given two points ${lverb P} and ${lverb Q} computes the Test of the line ${lverb P Q}." ❙
Test: 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 Test between points ${lverb P} and ${lverb Q}."
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment