[Agda] moving common from `with'
Serge D. Mechveliani
mechvel at botik.ru
Sat Oct 13 19:06:04 CEST 2012
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
More information about the Agda
mailing list