Bounded length string
1234567891011121314151617181920212223242526
module Main
import Data.Fin
import Data.Vect
data BoundedString : (maxLen: Nat) -> Type where
MaxLenString : (s: String) -> { auto prf : length s < maxLen = True } -> BoundedString maxLen
Str4 : Type
Str4 = BoundedString 4
a : Str4
a = MaxLenString ""
b : Str4
b = MaxLenString "a"
c : Str4
c = MaxLenString "abc"
-- Won't compile
-- c : Str4
-- c = MaxLenString "abcd"
main : IO ()
main = putStrLn "Hello World!"
Idris
INFO