Skip to content

Instantly share code, notes, and snippets.

@edwinb
Created August 10, 2015 13:33
Show Gist options
  • Save edwinb/eb8424a3e7773bdba54e to your computer and use it in GitHub Desktop.
Save edwinb/eb8424a3e7773bdba54e to your computer and use it in GitHub Desktop.
Faked overloaded strings
data FakeChar = A | B | C
data ValidMyString : List Char -> Type where
VA : ValidMyString xs -> ValidMyString ('a' :: xs)
VB : ValidMyString xs -> ValidMyString ('b' :: xs)
VC : ValidMyString xs -> ValidMyString ('c' :: xs)
VNil : ValidMyString []
implicit fromString : (x : String) -> {auto p : ValidMyString (unpack x)}
-> List FakeChar
fromString x {p} = fromListChar p
where
fromListChar : ValidMyString xs -> List FakeChar
fromListChar (VA x) = A :: fromListChar x
fromListChar (VB x) = B :: fromListChar x
fromListChar (VC x) = C :: fromListChar x
fromListChar VNil = []
foo : List FakeChar
foo = "abcab"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment