[Agda] -> and let in syntax definitions

[Darryl]

Is it possible to use -> and let in syntax definitions? I've tried but I get a parse error and I'm not sure what the problem actually is. What I was thinking of was cases like this (which could be used for pattern matching in type sigs):

syntax (x : A) -> (let P = x in B) = [ P \: A ]-> B

which would eliminate the need for an OPTION. similarly, you could have sigmas that bring witnesses into scope:

syntax (p : Sigma A B) -> (let a = proj1 p in C) = Sigma'[ a \: A ] B --> C

- Darryl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130126/933eb13d/attachment-0001.html