Error in tutorial files
I am new to MMT and OMDoc, so I may have incorrectly installed some things, but I am getting errors in the files Tutorials/Mathematicians/source/Algebra.mmt and Tutorials/Mathematicians/source/Numbers.mmt. In both cases the line
include mitm:?InformalProofs ❙
breaks and jEdit reports an error.
I have run the commands "lmh install MitM/Foundation" and "lmh install Tutorials/Mathematicians" and both appear to have executed without errors. The jEdit MMT plugin is set so that MMT/content is the mathhub root, which seems correct, the top level folders in that directory are MMT, MitM, and Tutorials.
Specifically the errors I get are:
P6 : ⊦ ∀[n] n + O ≐ n ❙
P7 : ⊦ ∀[n]∀[m] n + S m ≐ S (n + m) ❙
include mitm:?InformalProofs ❙
plus_assoc : ⊦ ∀[x]∀[y]∀[z] x + (y + z) ≐ (x + y) + z ❘
= sketch "I have a marvelous proof, which this
margin is too narrow to contain" ❙
❚
49: unbound token mitm
49: domain must be atomic: Some((http://cds.omdoc.org/urtheories?Typed?oftype "mitm" http://mathhub.info/Tutorials/Mathematicians?InformalProofs))
52:unbound token: sketch
52:unbound token "
52:unbound token I
(...) every word in this line raises an error
Also,
distributivity : ⊦ ∀[a]∀[b]∀[c] a ⋅ (b + c) ≐ a ⋅ b + a ⋅ c ❘
= sketch "by induction" ❙
Errors:
66: unbound token sketch
In Algebra.mmt there is again unbound token mitm
, Domain must be atomic.
Also
view OppositeSemiGroup : ?SemiGroup -> ?SemiGroup =
include ?Magma = ?OppositeMagma ❙
associativity = sketch "trivial" ❙
❚
Error:
29: unbound token =
view OppositeMonoid : ?Monoid -> ?Monoid =
48 include ?SemiGroup = ?OppositeSemiGroup ❙
unit = unit ❙
left_neutral = right_neutral ❙
right_neutral = left_neutral ❙
❚
Error:
48: Could not infer domain of included morphism.