module WithInParModule (A : Set) where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

data Bool : Set where
  true : Bool
  false : Bool

isZero : Nat -> Bool
isZero zero = true
isZero (suc _) = false


f : Nat -> Nat
f n with isZero n
f n | true = zero
f n | false = suc zero

g : Nat -> Nat
g zero = zero
g (suc n) with g n
g (suc n) | zero  = n
g (suc n) | suc _ = n

-- Andreas, 2014-11-06 outlawing with on module parameter.
-- The following will trigger an error:

-- data T : Set where
--   tt : T

-- module A (x : T) where
--   h : T
--   h with x  -- illegal!
--   h | y = y

-- postulate
--   C : T -> Set

-- test : C (A.h tt) -> C tt
-- test x = x

