Printf.idr

printfType : List Char  -> Type
printfType [] = String
printfType ('%' :: 'd' :: rest)  = Int -> printfType rest
printfType ('%' :: 's' :: rest) = String -> printfType rest
printfType (c :: rest)  = printfType rest 


{- construct value level function -}
printfValue : (xs : List Char) -> String -> printfType xs
printfValue [] acc = acc
printfValue ('%' :: 'd' :: rest) acc = \x => printfValue rest (acc ++ show x)
printfValue ('%' :: 's' :: rest) acc = \x => printfValue rest (acc ++ x)
printfValue (c :: rest) acc = printfValue rest (acc ++ singleton c)


- + Errors (1)
 `-- Printf.idr line 31 col 30:
     When checking right hand side of printfValue with expected type
             printfType (c :: rest)
     
     Type mismatch between
             printfType rest (Type of printfValue rest (acc ++ singleton c))
     and
             printfType (c :: rest) (Expected type)