[Agda] moving common from `with'

[Andreas Abel]

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' : ℕ -> ℕ -> ℕ
f' m n = case m ≤? n of
     λ { (yes _) -> g (suc m)
       ; (no  _) -> g (suc n)
       }
   where
     g : ℕ -> ℕ
     g m = m + m + 1


On 12.10.2012 14:24, Serge D. Mechveliani wrote:
> Please, what is the nicest way to move a common function from under
> `with' ?
>
> Consider the program
>
>    f : Nat -> Nat -> Nat
>    f m n  with  m <=? n
>    ...  | yes _ = g (suc m) where
>                             g : Nat -> Nat
>                             g m = m + m + 1
>    ...  | no _  = g (suc n) where
>                             g : Nat -> Nat
>                             g m = m + m + 1
>
> The neccessity of moving  g  out is stronger for the examples having
> larger expressions for  g.
>
> I find that it works
>    f m n = h
>            where
>            g : Nat -> Nat     -- to be replaced
>            g m = m + m + 1    -- with a larger code
>
>            h : Nat
>            h  with  m <= n
>            ...  | yes _ = g (suc m)
>            ...  | no _  = g (suc n)
>
> But this looks a bit awkward, it introduces an additional function  h,
> and its signature. This does not look as nice as the Haskell code
>
>    f m n = (case compare m n of GT -> g (suc n)
>                                 _  -> g (suc m))
>            where
>            g :: Int -> Int
>            g m = m + m + 1
>
> (apart of that the signature for  g  can be skipped in Haskell).
>
> 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/