Bounded length string

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