[Agda] optional dot in dot patterns?

Peter Divianszky divipp at gmail.com
Mon Nov 19 10:05:43 CET 2012


Hi,

Could the dot be optional in dot patterns?

As I see there are three kinds of dot patterns:

- function calls
- constructors calls
- variables

Function calls could be recognized by checking whether there is a 
function with that name in scope.
Variables could be recognized by checking whether there a variable with 
that name in scope.
In case of constructor calls (like .6) the expression and the pattern 
should be the same so maybe the compiler could figure out that 6 is a 
pattern match or a dot pattern. Is this true?

Thanks,
Peter


More information about the Agda mailing list