I noticed the following unexpected (by me!) behaviour, illustrated by this MWE and its output in the figure below:

% arara: xelatex: { shell : yes }    

\mintinline{lean}{#print axioms}

#print axioms

\li{#print axioms}


enter image description here

It looks like the command to \li is interpreted as both a # and a ## (see What is the meaning of double pound symbol (number sign, hash character) ##1 in an argument?), which is rather odd!

From a typesetting perspective, the obvious "solution" to my problem is to use \mintinline{lean}{...} rather than the \li alias. But I'm also curious to know what's going on with the code. In principle it seems like \li should work, and, indeed, it does for input that doesn't start with a #.

  • You shouldn't do this. Better: \newcommand{\li}{\mintinline{lean}} – TeXnician Aug 1 '18 at 11:07

You are dealing with a verbatim command and especially its verbatim argument which is always dangerous. And you are overriding any special argument handling that minted may have by passing the parameter from your macro definition. A better version would be \newcommand{\li}{\mintinline{lean}} which leaves processing the argument to minted.

Aside: minted provides \newmintinline which is basically intended for creating such macros.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.