[Agda] Re: Implicit arguments

[N. Raghavendra]

At 2015-04-12T21:21:16+01:00, Peter Hancock wrote:

> Me too. I often end up with scripts where there are masses of curly
> brackets around arguments, by being too optimistic about what the
> type-checker will infer.  Some general (not very helpful advice) is to
> use this feature only where the type will be so blindingly obvious
> that you can infer it in your head.

I'm glad that my dilemma isn't unique!

Cheers,
Raghu.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/