search

slatex / sTeX

A semantic Extension of TeX/LaTeX
50 stars 9 forks source link

realizations missing fields #365

Open kohlhase opened 2 years ago

kohlhase commented 2 years ago

In smglom/linear-algebra/source/mod/vector-space.en.tex I have

Screenshot 2022-09-30 at 15 01 10

and indeed there are some fields missing, but in this case, I do not want to do all the (trivial) assignments. Is there a way to be more convenient here?

Jazzpirate commented 2 years ago

well, the actual targets of the assignments are only checked by MMT, so from the point of view of sTeX you can easily do \assign{foo}{I have a marvelous proof which this .tex file is too narrow to contain} - but a realization requires assigning all fields in principle, so I think it useful to have latex insist on it and have MMT complain ;)

Jazzpirate commented 2 years ago

Ah, for the special case where you want to assign the identity on a whole module/mathstructure, there is the abbreviation \donotcopy{module-name}, which automatically assign everything in module-name to itself, so modularity helps/is encouraged

kohlhase commented 2 years ago

Ah, that is what I was hoping for, does that take a CSL as the argument?

Jazzpirate commented 2 years ago

No, but I'd be surprised if the situation occurs too often that you have several (>2) modules you want to assign to the identity...