fact: Fixpoint show_quoted_string (s:string) : string := match s with | EmptyString => """" | String c s' => let quoted_s' := show_quoted_string s' in let n := nat_of_ascii c in if ascii_dec c "009" then "\t" ++ quoted_s' else if ascii_dec c "010" then "\n" ++ quoted_s' else if ascii_dec c "013" then "\r" ++ quoted_s' else if ascii_dec c """" then "\""" ++ quoted_s' else if ascii_dec c "\" then "\\" ++ quoted_s' else if ((n <? 32)%nat || (126 <? n)%nat )%bool then "\" ++ three_digit n ++ quoted_s' else String c quoted_s' end.
imports: Coq(Ascii Basics Decimal List String ZArith)