[Agda] f (p1 , p2)

[Andreas Abel]

Unfortunately, functions defined by pattern matching are currently not 
accepted in let declarations.  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

On 25.01.2014 13:08, Sergei Meshveliani wrote:
> Please,
> how to make work the below pattern of    g {d} (p1 , p2) = ...
> ?
> I have
>
> ----------------------------------------------------------------------
> ...
>    private IncludedCommonDivs : C × C → C × C → Set (α ⊔ α=)
>            IncludedCommonDivs (a , b) (a' , b') =
>                               ∀ {d} → (d ∣ a × d ∣ b) → (d ∣ a' × d ∣ b')
>
>    f : ∀ {x y} → IncludedCommonDivs (x , y) (x , y)
>    f {d} (p1 , p2) = (p1 , p2)
>    ...
>
>    extGCD a b =  eGcd ...
>      where
>      a-eq :  a ≈ (a * 1#) + (b * 0#)
>      ...
>
>      eGcd u1 u2  ...  with v ≟ 0#
>      ...
>          | yes v=0 =  record{ ...}  where ...
>      ... | no v≉0  =
>            let
>               (divRem′ q r u=q*v+r remLess) = divRem u v v≉0
>               ...
>
>               g : IncludedCommonDivs (a , b) (a , b)
>               g {d} (p1 , p2) =  (p1 , p2)
>               ...
>            in
>            ...
> -----------------------------------------------------------------------
>
> Now:
> 1)  the pattern for  f  is type-checked,
> 2)  the pattern for  g  causes  "Not a valid let-declaration ..."
>
> 3)  the variant      g {d} pair =  (proj₁ pair , proj₂ pair)
>      is type checked.
>
> I set `let' there because this allows the above pattern of
>              (divRem′ q r u=q*v+r remLess) = divRem u v v≉0.
>
> Can this combination of  `with', `where' and `let' be reliable?
>
> I could try  `case' + `let',  with removing  `with' + `where'.
> But
> a) `case' is often difficult to make it type-checked,
> b) I doubt of whether the matter is in mixing  "with + let".
>
> Thanks,
>
> ------
> Sergei
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>