DF
Пдф это рисунок а не документ
data Format =
Number Format
| Str Format
| Lit String Format
| End
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: tail) = Number (toFormat tail)
toFormat ('%' :: 's' :: tail) = Str (toFormat tail)
toFormat (x :: tail) = Lit (cast x) (toFormat tail)
reduceFormat : Format -> Format
reduceFormat (Number x) = Number (reduceFormat x)
reduceFormat (Str x) = Str (reduceFormat x)
reduceFormat (Lit x (Lit y t)) = reduceFormat (Lit (x ++ y) t)
reduceFormat (Lit x y) = Lit x (reduceFormat y)
reduceFormat End = End
