[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