[Agda] Checking the types of terms

[Peter Hancock]

On 06/03/2018 20:30, Larrytheliquid wrote:
> Agda does have underscore definitions, which do not add new identifiers:
> 
> \begin{code}
> _ : type_1
> _ = term_1
> ...
> _ : type_n
> _ = term_n
> \end{code}

Ah! The penny drops! That explains a lot of things I have been reading.


Something I have come to appreciate about Haskell is its nice 
use of underscores, so you can read 

k x _ = x,

without having to search through some enormous right-hand-side to see if some 
spuriously-invented name occurs there. Three cheers for that. 

Agda seems to take this further, from argument lists to the whole name-space.
It seems a very nice feature.  Remembering or thinking up names for things 
that are never going to be referenced is not fun. It is hard enough when they
are referenced. 

Hank