fact: Fixpoint mkline s acc {struct s} := if s is String a s1 then let n := nat_of_ascii a in if n == sp then if acc is some x then mkline s1 (some (0::x)) else mkline s1 None else if n == nl then mkline s1 None else if n == sep then if acc is some x then app (rev x) (mkline s1 (some [::])) else mkline s1 (some [::]) else if is_num n then if acc is some x then mkline s1 (some ((get_num n)::x)) else mkline s1 None else mkline s1 None else [::].
imports: mathcomp(all_ssreflect) mathcomp(zify) String