Skip to content
Snippets Groups Projects
Select Git revision
  • devel
  • Paul_Marius_Level
  • Paul_Marius
  • master default
  • testing_paul
  • Paul
  • marcel
  • loviwo-experimental
  • 3.0.0
9 results
Compare
Name Last commit Last update
META-INF
bin/info/kwarc/mmt/frameit/rules
content/http..BenniDoes.Stuff
errors/mmt-omdoc
narration
relational
scala
source
README.md
README.md

A Prototype Game for UFrameIT

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.