[Agda] status of inlining agda code

[Thorsten Altenkirch]

Thank you, Nisse.

Here is another question: I sometimes want to display different versions of the same program (with the same name). However, Agda won’t let me. What is the best workaround for this? I guess I could put the first version in a different module but then the indentation is different.

Thorsten




On 02/02/2020, 21:37, "Nils Anders Danielsson" <nad at cse.gu.se> wrote:

>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



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.