Michael Kohlhase (203dfffa) at 13 Nov 04:59
more LBS
Michael Kohlhase (0a7a60ef) at 30 Oct 18:12
fixes
Michael Kohlhase (9183ba6f) at 26 Oct 05:10
debugging
Michael Kohlhase (995da737) at 26 Oct 04:53
more annotations
Michael Kohlhase (d6567dd4) at 23 Oct 12:40
more annotation
Michael Kohlhase (4bb757c4) at 19 Sep 06:34
fixing dependencies in MANIFEST.MF
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.
Michael Kohlhase (f8423f63) at 21 Nov 11:54
taking care of \trefi and friends
Michael Kohlhase (9a35c43c) at 29 Oct 09:59
Michael Kohlhase (9a35c43c) at 28 Jun 06:40
undoing preamble changes from yesterday, they cannot work
... and 1 more commit
Michael Kohlhase (bea96efd) at 05 May 15:29
draining
Michael Kohlhase (3f8d0e4d) at 01 May 12:56
more preloading an debugging