Open kohlhase opened 1 year ago
Objection: Let $\defeq{\foo!}{\foo!!}$ be a \symname{foo}
<- notice how "foo" means two entirely different things here: \foo
refers to a (generic) instance, whereas \symname{foo}
does not refer to the same instance, but instead to the "class/type" of structures.
But we do need a mechanism for #363 anyway that allows for something like this - I've been thinking a macro \this
in structures that behaves basically like your \foo
, which would be "imported" by usestructure. It now occurs to me though that we might need to be able to distinguish between different structures being used...
...having \foo!!
expand to the corresponsing \mathstruct{...}
is difficult, because it's not clear which fields should end up in the mathstruct (and a surface syntax where you need to specify the fields does not offer much). I think there's an issue for that already.
I also notice though that we should rename something: either the mathstructure
-environment or the \mathstruct
-macro, because I notice you keep confusing them (and I don't blame you). Can we come up with something better?
There are currently two methods of "using a math structure", e.g. group that is defined by
\usestructure{foo}
gives you the macros\bar
and\baz
while\varinstantiate{F}{foo}{\comp{F}}
gives you\F{bar}
and\F{baz}
, but also\F!
(it expands to)\comp{F}
.It would be nice, if we had a
\foo!
as well from\usestructure{foo}
, this could come from\usestructure{foo}[op=F]
or even better from\begin{mathstructure}{foo}[op=F]
and be available in any\usestructure
.And when I am at it, I think that
\usestructure{foo}
should provide a notation that constructs the whole structures, i.e. something like\foo!!
(for lack of an idea about other characters) that expands to\mathstructure{\foo,\bar}
or even to.With that writing the run-of-the-mill definition would be relatively convenient: