{- This file shows a natural attempt to do formatted printing, and where that attempt goes wrong. See string-format.agda for a (working) solution to this problem. -} module string-format-issue where open import char open import eq open import list open import nat open import nat-to-string open import string format-th : 𝕃 char β†’ Set format-th ('%' :: 'n' :: f) = β„• β†’ format-th f format-th ('%' :: 's' :: f) = string β†’ format-th f format-th (c :: f) = format-th f format-th [] = string format-t : string β†’ Set format-t s = format-th (string-to-𝕃char s) test-format-t : format-t "The %n% %s are %s." ≑ (β„• β†’ string β†’ string β†’ string) test-format-t = refl format-h : 𝕃 char β†’ (f : 𝕃 char) β†’ format-th f format-h s ('%' :: 'n' :: f) = Ξ» n β†’ format-h (s ++ (string-to-𝕃char (β„•-to-string n))) f format-h s ('%' :: 's' :: f) = Ξ» s' β†’ format-h (s ++ (string-to-𝕃char s')) f format-h s (c :: f) = {!!} format-h s [] = 𝕃char-to-string s format : (f : string) β†’ format-t f format f = format-h [] (string-to-𝕃char f)