module exampleDouble where


data Char : Set where
  a : Char
  b : Char


data String : Set where
  [] : String
  _::_ : Char -> String -> String


concat : String -> String -> String
concat [] s = s
concat (c :: s) s' = c :: (concat s s')

double : String -> String
double s = concat {! !} {! !}