[Agda] status of inlining agda code

[Nils Anders Danielsson]

On 2020-02-02 23:56, Thorsten Altenkirch wrote:
> 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.

Did you try it? The following should work:

   \begin{code}[hide]
     module Hidden where
   \end{code}
   \begin{code}
       A : Set₁
       A = Set
   \end{code}
   \begin{code}
     A : Set₁
     A = Set
   \end{code}

-- 
/NAD