String.agda 430 B

12345678910111213141516171819202122232425
  1. module Data.String where
  2. import Data.List
  3. import Data.Char
  4. open Data.List using (List)
  5. open Data.Char
  6. postulate String : Set
  7. {-# BUILTIN STRING String #-}
  8. infixr 50 _++_
  9. private
  10. primitive
  11. primStringAppend : String -> String -> String
  12. primStringToList : String -> List Char
  13. primStringFromList : List Char -> String
  14. _++_ = primStringAppend
  15. toList = primStringToList
  16. fromList = primStringFromList