[Agda] optional dot in dot patterns?

Nils Anders Danielsson nad at chalmers.se
Mon Nov 19 14:00:10 CET 2012

On 2012-11-19 13:26, Peter Divianszky wrote:
> I don't see that shadowing is a problem.
> If we have a pattern (f x) such that f is a function in scope, then
> the compiler could replace (f x) by .(f x), couldn't it?
> And I ask the same for more than one or zero arguments.

Currently accepted code:

     A : Set

   f : Set → Set
   f A = A

Should A be dotted here?


More information about the Agda mailing list