[Agda] moving common from `with'

[Serge D. Mechveliani]

On Fri, Oct 12, 2012 at 08:10:52PM +0200, Andreas Abel wrote:
> I'd ditch the with in favor of a case with a pattern-matching lambda for  
> your example.
>
> open import Data.Nat
> open import Function
> open import Relation.Nullary
>
> f' : Nat -> Nat -> Nat
> f' m n = case m <=? n of
>          \lambda { (yes _) -> g (suc m)
>                  ; (no  _) -> g (suc n)
>                  }
>                  where
>                  g : Nat -> Nat
>                  g m = m + m + 1

(I replaced the math symbols in this citation -- SM).

As to `case', consinder the variant

  f : Nat -> Nat -> Nat
  f m n = case  m :: (m + n) :: []  of \lambda 
          { 
            (0 :: _)      -> g (suc m)
          ; (1 :: v :: _) -> g (n + 2 * a)  where
                                            a = v + v * v
          ; _             -> g (suc n)
          }
          where
          g : Nat -> Nat 
          g m = m + m + 1
       
It is not type-checked in  Agda-2.3.0.1 + MAlonzo + lib-0.6 :
the `where' inside `case' is rejected.
It can be replaced with `let'.
But I recall, it is said somewhere that, generally, `let' is not so 
well supported in Agda as `where' (do I recall right?).

Regards,
Sergei