Newer
Older
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 ❙
❚