module RecursivePatterns where

open import Data.Bool
open import Data.List using (List ; [] ; _∷_)

infixr 6 _,_

pattern [   xs    = xs
pattern _,_ hd tl = hd ∷ tl
pattern _] a      = a ∷ []

tail : ∀ {A : Set} (xs : List A) → List A
tail []          = []
tail ([ a ])     = []
tail ([ a , b ]) = [ b ]
tail ([ a , b , x , d , e , f ]) = [ b , x , d , e , f ]
tail (hd ∷ tl) = tl