[Agda] difficulties with patterns

[Andreas Abel]

Mmh, I would guess this is because Agda creates a local function for the 
\ { ... } (which is called "extended-lambda" in Agda-speak).

What you can try instead is to write

   case toBDigits n of \ pr ->
     let (bs , (_ , hasLast1-if-bs)) = pr
         ... more let bindings ...

     in cong-...

Cheers,
Andreas

On 27.11.2013 15:27, Sergei Meshveliani wrote:
> Please,
> how can one avoid difficulties in using patterns?
> (what is a common way out?).
>
> For example, this program works:
>
>   hasLast1-toBDigs-suc-n : (n : ℕ) → HasLast1 $ toBDigs $ suc n
>   hasLast1-toBDigs-suc-n n =
>               cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>      where
>      pr             = toBDigits n
>      bs             = proj₁ pr
>      hasLast1-if-bs = proj₂ $ proj₂ pr
>
>      digs-n'          = toBDigs $ suc n
>      digs-n'=addC1-bs = toBDigs-suc-eq {n}
>
>      hasLast1-addC1-bs : HasLast1 $ addC1 bs
>      hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>
>
> Then I try to improve the style and replace the three assignments and
> projections with pattern matching:
>
>      case toBDigits n
>      of \
>      { (bs , (_ ,  hasLast1-if-bs)) →
>              let
>                 digs-n'          = toBDigs $ suc n
>                 digs-n'=addC1-bs = toBDigs-suc-eq {n}
>
>                 hasLast1-addC1-bs : HasLast1 $ addC1 bs
>                 hasLast1-addC1-bs = hasLast1-addC1 bs hasLast1-if-bs
>              in
>             cong-HasLast1 (blSym digs-n'=addC1-bs) hasLast1-addC1-bs
>      }
>
> And obtain the report
>
>    bs != (proj₁ (.Int.Bin2._.toBits n n n (≤refl PE.refl)))
>    of type  (List Bit)
>    when checking that the expression  hasLast1-addC1-bs  has type
>    HasLast1 (addC1 (toBDigs n)).
>
> The checker somehow does not allow to improve style.
>
> Thanks,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> 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/