[Agda] f (p1 , p2)

[Sergei Meshveliani]

On Sat, 2014-01-25 at 13:39 +0100, Andreas Abel wrote:
> Unfortunately, functions defined by pattern matching are currently not 
> accepted in let declarations. 

I do not know of how difficult is it to arrange this pattern matching.
But this feature is very desirable.
This is a matter of a code plainness, of saving effort. Currently the
programmer needs to remember of may be 30 tricks, and each time to
recall the needed trick ...    

Thanks,

------
Sergei


>  In this case
> 
>    let g : ...
>        g (p1 , p2) = ...
> [..]
> we are dealing with a record pattern, so it is not a definition by 
> pattern matching in the strict sense.  Still, it is rejected.  However, 
> the following workaround should be possible:
> 
>    let g : ...
>        g p = let (p1 , p2) = p in (p1 , p2)
> 
> Cheers,
> Andreas
> 
> [..]