diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index d4537efa5248828c8aa8f708e8da778e729280c7..895da273153564f46b2b36d37c20c8333d37afcb 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -1,34 +1,34 @@ -namespace http://mathhub.info/FrameIT/frameworld ⚠- -fixmeta ur:?LF ⚠- -/T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls ⚠-theory MetaAnnotations = - include ☞http://mathhub.info/MitM/Foundation?Strings ♠- - label ♠- description ♠- - problemTheory ♠- solutionTheory♠- - /T Example usages: - - `lverb A`, where A refers to a symbol - - `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments - ♠- label_verbalization_of # lverb ♠- description_verbalization_of # dverb ♠-⚠- -/T The meta theory to use for situation theories, scroll problem, and scroll solution theories ⚠-theory FrameworldMeta = - include ?MetaAnnotations ♠- - include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ♠- - include ☞http://mathhub.info/MitM/Foundation?Strings ♠- include ☞http://mathhub.info/MitM/Foundation?Math ♠- - include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠- include ☞http://mathhub.info/MitM/core/geometry?Planes ♠-⚠+namespace http://mathhub.info/FrameIT/frameworld ⚠+ +fixmeta ur:?LF ⚠+ +/T MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls ⚠+theory MetaAnnotations = + include ☞http://mathhub.info/MitM/Foundation?Strings ♠+ + label ♠+ description ♠+ + problemTheory ♠+ solutionTheory♠+ + /T Example usages: + - `lverb A`, where A refers to a symbol + - `lverb A B`, a shorthand for `concat (lverb A) (lverb B)`; works for arbitrary number of arguments + ♠+ label_verbalization_of # lverb ♠+ description_verbalization_of # dverb ♠+⚠+ +/T The meta theory to use for situation theories, scroll problem, and scroll solution theories ⚠+theory FrameworldMeta = + include ?MetaAnnotations ♠+ + include ☞http://gl.mathhub.info/MMT/LFX/Sigma?LFSigma ♠+ + include ☞http://mathhub.info/MitM/Foundation?Strings ♠+ include ☞http://mathhub.info/MitM/Foundation?Math ♠+ + include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ♠+ include ☞http://mathhub.info/MitM/core/geometry?Planes ♠+⚠diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md index 90be86bed2e044724b516c146e8a0fcba3dc2e78..95e8ed120b3fd9198eb22bae7c15dc95316d35bf 100644 --- a/source/Scrolls/README.md +++ b/source/Scrolls/README.md @@ -33,6 +33,9 @@ theory Midpoint = to have access to the facts formalized in the problem theory ♠include ?Midpoint/Problem ♠+ // the next meta annotations (to the theory) actually make this theory into a scroll: + We specify the Problem and Solution theories ♠+ meta ?MetaAnnotations?label "MidPoint" ♠meta ?MetaAnnotations?problemTheory ?Midpoint/Problem ♠meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution ♠@@ -52,10 +55,10 @@ theory Midpoint = midpoint : point ☠- = ⟨0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x), 0.5 ⋅ (P_x + Q_x)⟩ ☠+ = ⟨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}." ♠⚠⚠-``` \ No newline at end of file +```