we need an informal version of assign

[kohlhase]

In {realization} and friends we have \assign{foo}{bar} where foo and bar are symbols in the source and target structures. But in the informal setting (currently looking at smglom/computing/source/mod/file-path.en.tex, which currently has

 \begin{realization}[smglom/graphs]{mod?tree/tree-structure}
     \assign{nodes}{objects}
     \assign{edges}{foo}
     \assign{root}{bar}
     \assign{root.cond}{foobar}
     \assign{degree.cond}{foobaz}
    The \symname{hfs?directory} structure in a \symname{hfs?hierarchical-file-system}
    induces a \symname{tree?tree}, so we inherit the concepts of (file system)
    \definame{file-path?root}, \definame{parent} (directory), \definame{child}, and \definame{file-path?path}
    from there.
  \end{realization}

I would rather do somerthing like

\iassign{nodes}{the \symname[post=s]{file} and \symname[post=s]{folder}}
\iassign{edges}{the ``file-in-folder'' \symname{relation}}
\assign{root}{file-system-root}
\iassign{root.cond}{there is only one \symname{root-folder} in a \symname{hfs}}
\iassign{degree.cond}{by construction}

[Jazzpirate]

\assign is already "informal" in that tex does not check the target of the assignment anyway - you can write whatever you want in there.

MMT might complain, because MMT actually checks the assignments, but all that does is give you a warning in the IDE, and I think it should :)

[kohlhase]

I think an \iassign would be useful in that it could tell MMT that the content is opaque.

[kohlhase]

And I do not want IDE warnings.

[Jazzpirate]

Indeed, all your assignments already are informal: \assign{root.cond}{foobar} <- note that you're assigning the symbol to the non-semantic plain text foobar here. MMT should complain that it doesn't know what foobar means.

If you want to assign the symbol foobar, use \assign{foo}{\symname{foobar}}. The second argument of \assign is expected to be an arbitrary term, not a symbol.

MMT already knows the content is opaque. It also knows that it can't actually do anything with opaque targets, so it rightfully complains. And I think it's a good idea to keep warnings there, if only as a reminder that something should be done here by the author ;) I'm very open to introducing something analogous to \proofsketch{arbitrary blabla} that works for all axioms, because with those it will get overly tedious very quickly, but:

\iassign{nodes}{the \symname[post=s]{file} and \symname[post=s]{folder}} <- this I disagree fundamentally with. If you don't actually want to assign things, then don't use a morphism that gives you assignments ;)

And I still maintain introducing tex-syntax just to avoid IDE-warnings is not a good design choice.

[Jazzpirate]

Just to clarify: with "this I diasagree fundamentall with" I mean "this should cause MMT to throw a warning", because that's the entire point of having MMT ;)