# A Prototype Game for [UFrameIT](https://uframeit.github.io)
# FrameWorld: Formalizations for the [UFrameIT game](https://uframeit.github.io)
This Math Archive contains three directories:
— following the FrameIT approach.
## Library:
All things to describe basic math things.
## Contents
Currently in use are:
-`3DVector.mmt`
-`Lines.mmt`
Importantly, in [`./source`](./source) you can find
Most of the other stuff was practicing MMT / having fun with it.
*Note*: `BenniDoesStuff.mmt` collects all theories of this folder and is used as some kind of basic geometry-language.
-[`MetaTheories.mmt`](./source/MetaTheories.mmt): contains includes and symbols for meta keys/values shared by all other theories
-[`Scrolls/`](./source/Scrolls): contains all scrolls
-[`Library/`](./source/Library): contains files of the upcoming Loviwo proposal
## Fact-Types:
`FactTypes.mmt`: Definition of the FrameIt-Fact-Types:
- Distance, Angles, OnLine
- The "UnorderedPair" was a experiment to solve the `Type( d(a,b) ) == Type( d(b,a) )` problem.
Which should be solved by the equality-rule from Dennis right now
- Note that `Vector` and `Line` use the "constructor"-functions from 3DVector.mmt and Line.mmt of the library-directory
Besides that, there is also
`FactCollection.mmt`: Collects all FactType-theories to act as a language to implement scrolls
-[`IntegrationTests/`](./source/IntegrationTests): contains some integration tests run by the unit tests in the frameit-mmt submodule of the UniFormal/MMT project
## Scrolls:
`ScrollMeta.mmt`:
- Some declarations to act as meta-keys at the scroll-formalizations
## Authors
other files:
- Scrolls as Problem-Solution Pairs
- Usable at the time of my submission
- All but the TangensScroll strangly dissapeared on the playable Demo =(
-`PlaygroundScroll.mmt`: playground to test views, Communication with the frontend etc.
