Skip to content

Instantly share code, notes, and snippets.

Created October 13, 2016 05:52
What would you like to do?
Idris String with validation?
-- A data type wrapping a non-empty string
data Name : Type where
MkName : (s : String) -> (not (s == "") = True) -> Name
-- Some function that expects a valid Name
test : Name -> String
test (MkName s _) = s
-- Usage of that function. Do I need Refl here? Any better way of doing this?
foo : String
foo = test (MkName "foo" Refl)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment