[Agda] difficulties with patterns

[Sergei Meshveliani]

Sorry, I have forgotten to copy my reply to the list:


On Thu, 2013-11-28 at 23:08 +0100, Andreas Abel wrote:
> On 28.11.2013 18:05, Sergei Meshveliani wrote:
> > Andreas responded recently:
> >> 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-...
> 
> Ah, I screwed this one up.  The case loses the connection between 
> "toBDigits n" and "pr".  You should do without the case.
> 
>    hasLast1-toBDigs-suc : (n : ℕ) → HasLast1 $ toBDigs $ suc n
>    hasLast1-toBDigs-suc n =
>            let (bs , (_ , hasLast1-if-bs)) = toBDigits n
>                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
> 
> Can you try again?
> 


It works! Thank you.

`let' works here, `where' does not. And in various Agda versions I had
various adventures with all of them: `let', `where', `case', `with', 
calling a new function ... Many of these adventures were due to my own
errors.  So that currently it is difficult for me to predict which one
will work. This is why I have forgotten to try "simple let".

Agda is good, though. 
Probably, it is difficult to join dependent types and a language
clarity. 

Thanks,

------
Sergei