MetaTheories.mmt

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