Skip to content
Snippets Groups Projects
Commit 9871b364 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

adding Benni's notes

parent a2001f63
No related branches found
No related tags found
No related merge requests found
# A Prototype Game for [UFrameIT](https://uframeit.github.io)
This Math Archive contains three directories:
## Library:
All things to describe basic math things.
Currently in use are:
- `3DVector.mmt`
- `Lines.mmt`
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.
## 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
`FactCollection.mmt`: Collects all FactType-theories to act as a language to implement scrolls
## Scrolls:
`ScrollMeta.mmt`:
- Some declarations to act as meta-keys at the scroll-formalizations
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.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment