[Agda] -> and let in syntax definitions

[Andreas Abel]

The actual problem is that there is no maintainer for the `syntax' facility.

On 27.01.13 4:38 AM, Darryl wrote:
> 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
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/