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, 2018 at 11:07

1 Answer 1


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.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .