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!"