[Agda] agda latex mode

[Nils Anders Danielsson]

On 2020-02-04 19:42, Thorsten Altenkirch wrote:
> However, the problem is that I seem to need the code environment in
> the output but if I use it agda will try to translate it.

I'm not sure why you want to do this, but Agda looks for
"\begin{code}"/"\end{code}" without any extra whitespace, so you could
add some spaces:

   \begin {code}
   \>[2]\AgdaFunction{proj₁}\AgdaSpace{}%
   \AgdaSymbol{:}\AgdaSpace{}%
   \AgdaSymbol{\{}\AgdaBound{A}\AgdaSpace{}%
   \AgdaBound{B}\AgdaSpace{}%
   \AgdaSymbol{:}\AgdaSpace{}%
   \AgdaPrimitiveType{Set}\AgdaSymbol{\}}\AgdaSpace{}%
   \AgdaSymbol{→}\AgdaSpace{}%
   \AgdaBound{A}\AgdaSpace{}%
   \AgdaOperator{\AgdaRecord{×}}\AgdaSpace{}%
   \AgdaBound{B}\AgdaSpace{}%
   \AgdaSymbol{→}\AgdaSpace{}%
   \AgdaBound{A}\<%
   \end {code}

I don't guarantee that this hack will work forever.

-- 
/NAD