[Agda] Checking the types of terms

[Nils Anders Danielsson]

On 2018-03-06 23:49, Guillaume Brunerie wrote:
> Using the syntax mechanism and an infix symbol, you can even get
> 
> _ = term1 :> type1
> _ = term2 :> type2
> 
> or whatever other symbol you choose.

And you can hide parts of the code:

   \begin{code}[hide]
     _ =
   \end{code}
   \begin{code}
       term1 :> type1
   \end{code}

(This is assuming that you are using the development version of Agda.
Agda 2.5.3 provides a different syntax for hiding code, see
http://agda.readthedocs.io/en/v2.5.3/tools/generating-latex.html#features.)

-- 
/NAD