[Agda] status of inlining agda code

[Nils Anders Danielsson]

On 2020-02-02 15:53, Thorsten Altenkirch wrote:
> If I want to discuss f 3 in some text, do I have to write
> $\AgdaFunction{f}\,3$ or is there a better solution?

If f is in scope, then you can use a code environment with the option
inline (or inline*):

   https://agda.readthedocs.io/en/latest/tools/generating-latex.html#inline-code

However, this is a bit clunky:

   Consider the application
   \begin{code}[hide]
     _ =
   \end{code}
   \begin{code}[inline]
       f 3
   \end{code}.

If Agda cannot infer the type of the application, then you can give it
manually:

   We know that
   \begin{code}[hide]
     _ : …
     _ =
   \end{code}
   \begin{code}[inline*]
       f 3
   \end{code}
   must be…

-- 
/NAD