Open Jazzpirate opened 4 years ago
Hmm, this is really one of the unresolved OMDoc/sTeX language design issues, that needs to taken care of now to make progress. I will use this place of develop my thoughts.
Background: I noticed in sTeX/SMGloM that I needed something like local symbols with complex notations in definitions. \vardef
is just the user interface, since mathematicians (I believe) think of them as variables. And an implementation as \symdef
just fit the bill.
The situation in quotient-group
is typical, you need a structure S=<a,b,c>, and you want to say things about the components in the definitions later. Which would be simple, if they were all individuals, but some of them are functions, so I need notations on them. Hence \vardec
.
I wonder if what I really want here is a structure. In MMT I would (non-modularly write down)
a: t
b: t
c: t -> t
hmmm, I am confused, I need a whiteboard and a discussion partner.
https://gl.mathhub.info/smglom/algebra/blob/master/source/quotient-group.de.tex#L3 causes
malformed:omdoc:symbol <omdoc:symbol> isn't allowed in <omdoc:definition>
. The current binding for\vardef
is######## temporal hack by MiKo; @DG,please remove after implementation. Let('\vardef', '\symdef');
so should \vardef (ultimately) be allowed in a definition? If so, should it yield something other than a
omdoc:symbol
or does the schema need to be adapted?