Open Jazzpirate opened 3 years ago
I suspect that the user of a math paper might be willing to give the explicit argument explicitly, but does not want it to be formatted in the result (alternatively be hidden in the result but available upon request). I consider this ability of hiding given arities an important capability of sTeX.
hiding given arguments would be easily achieved by a notation, e.g.:
\notation[hidefield]{gln}[2]{GL(#2)}
It occurs to me, that (some variant of) \abbrdef
might allow us to
E.g. expanding on https://github.com/KWARC/FoMID/issues/14 and https://github.com/KWARC/FoMID/issues/12, a module PLImplication
could extend a face-theory for Implication
by assigning \implication
to the implication in latin2.
e.g.
\abbrdef{implication}[2]{\OMA{latin:/?Implication?implication}{#1,#2}}{#1 \Rightarrow #2}
(where \OMA
would do nothing on the tex-side and represent an OMA/LFApply on the MMT-side...)
...in general I think the "definiens" in an \abbrdef
would only matter on the MMT-side, never on the tex-side
e.g. the general linear group of dimension n over a field K is usually just denoted as GL(n), omitting the field. Should we expect users to provide them each time?
Alternatively: Semantic abbreviations (I think sTeX has an
\abbrdef
, but it's not documented afaik?), possibly with an\implicit
macro that signals MMT that an implicit argument occurs here, e.g.\symdef{gln}[2]{GL(#1,#2)}
\abbrdef{glni}[1]{\gln{\implicit}{#1}}{GL(#1)}
Then MMT can attempt to do type inference and search the context for the most likely value. We can also allow for local\abbrdef
s that explicitly state a fixed argument for the current section, in which case we might want to mark these as not-exported in\includemodule
s.