From 8ed4e3ff381317a2ba4d9a7f794e8f9758655732 Mon Sep 17 00:00:00 2001 From: Navid Roux <navid.roux@fau.de> Date: Tue, 27 Oct 2020 13:16:17 +0100 Subject: [PATCH] cache test --- source/MetaTheories.mmt | 68 ++++++++++++++++++++--------------------- 1 file changed, 34 insertions(+), 34 deletions(-) diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index d4537ef..5d74cd0 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 ♠+⚠-- GitLab