Issue735.agda

-- Andreas, 2012-10-30 Sections
-- Reported by guillaume.brunerie, Oct 24 2012
module Issue735 where

import Common.Level
open import Common.Prelude using (Nat; zero; suc)

module _ {a} (A : Set a) where

  data List : Set a where
    []  : List
    _∷_ : (x : A) (xs : List) → List

module _ {a} {A : Set a} where

    _++_ : List → List → List
    []       ++ ys = ys
    (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

-- should not work, we cannot cut a section in two
-- correct is: List A

test : List Nat
test = (5 ∷ []) ++ (3 ∷ [])