fact: Fixpoint read_quoted_string (s : string) : option string := match s with | String c s' => if ascii_dec c """" then match s' with | EmptyString => Some EmptyString | _ => None end else if ascii_dec c "\" then match s' with | String c2 s'' => if ascii_dec c2 "n" then option_map (String "010") (read_quoted_string s'') else if ascii_dec c2 "r" then option_map (String "013") (read_quoted_string s'') else if ascii_dec c2 "t" then option_map (String "009") (read_quoted_string s'') else if ascii_dec c2 "\" then option_map (String "\") (read_quoted_string s'') else if ascii_dec c2 """" then option_map (String """") (read_quoted_string s'') else match s'' with | String c1 (String c0 s''') => match unthree_digit c2 c1 c0 with | Some c' => option_map (String c') (read_quoted_string s''') | None => None end | _ => None end | _ => None end else option_map (String c) (read_quoted_string s') | _ => None end.
imports: Coq(Ascii Basics Decimal List String ZArith)