MathHubInfo / Legacy-localmh

DEPRECATED - A cross-repository administration tool for the local authoring in MathHub.info
1 stars 0 forks source link

lmh symcheck should check mmt as well. #291

Open kohlhase opened 8 years ago

kohlhase commented 8 years ago

We have added "logic bindings" in MMT sysntax to MathHub, so lmh symcheck (see #290) should check the consistency of symbols between the sTeX and MMT bindings as well. In MMT, the symbol names are explicitly encoded. BUT, the theory and symbol names are not equal, but the MMT versions have underscores _ where the sTeX versions have dashes - (the respective other are forbidden in the language).