From 6daa62540e6486f91f4562fe96c80cf5e88ffe33 Mon Sep 17 00:00:00 2001 From: ComFreek <comfreek@outlook.com> Date: Mon, 26 Oct 2020 20:04:48 +0100 Subject: [PATCH] docs --- README.md | 35 +++++++++++------------------------ 1 file changed, 11 insertions(+), 24 deletions(-) diff --git a/README.md b/README.md index 883dde4..791cec2 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,19 @@ -# 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. +See team <https://uframeit.github.io>. \ No newline at end of file -- GitLab