[Agda] tuple pattern sugar

[Andreas Abel]

You could put this up as an enhancement request on the bug tracker.

Cheers,
Andreas

On 25.01.13 12:35 AM, Darryl wrote:
> this could actually be a good explanation of what the sugar for this
> stuff would be.
>
> for a pattern PAT
>
> (PAT : A) -> B
>
> desugars to
>
> (x : A) -> let PAT = x in B
>
> this shouldn't break anything, and could be added as an option.
> - darryl
>
> ------------------------------------------------------------------------
> *From:* Dmytro Starosud <d.starosud at gmail.com>
> *To:* Serge D. Mechveliani <mechvel at botik.ru>
> *Cc:* agda at lists.chalmers.se
> *Sent:* Thursday, January 24, 2013 1:24 PM
> *Subject:* Re: [Agda] tuple pattern sugar
>
> Yes, I am also suffering from it, but not often.
>
> Best regards,
> Dmytro
>
> 2013/1/24 Serge D. Mechveliani <mechvel at botik.ru <mailto:mechvel at botik.ru>>
>
>     On Thu, Jan 24, 2013 at 04:50:59PM +0200, Dmytro Starosud wrote:
>      > Ah, sorry, didn't notice that Level3 is tuple :)
>      > For this you can use let-bindings:
>      >
>      > \all {t : Level3} let (x , y , z) = t in (A : Set x) (B : Set y) ...
>      >
>
>     Yes. I have also discovered the possibility of this `let'.
>     Initially, it was not parsed, because I have forgotten to import _,_
>
>     (the report is only  "cannot parse",
>     and it is difficult to guess and recall of importing _,_).
>
>     Thanks,
>
>     ------
>     Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> 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/