3 ms·
Idris: data EndsWith : Type where EndsWithPeriod : (s: String) -> { auto prf : ("." `Strings.isSuffixOf` s = True) } -> EndsWith s : EndsWith s = En
by cinnamonheart 7y ago
Idris:
data EndsWith : Type where
EndsWithPeriod : (s: String) -> { auto prf : ("." `Strings.isSuffixOf` s = True) } -> EndsWith
s : EndsWith
s = EndsWithPeriod "."
-- Value of type False = True cannot be found
-- s2 : EndsWith
-- s2 = EndsWithPeriod ""
The noun one might be possible -- I'm honestly less familiar with what a proper noun is offhand. (E: prefix=>suffix)