fact: Fixpoint Z_of_rev_string (s:string) : Z := match s with "" => 0 | String a tl => (Z_of_nat (nat_of_ascii a) - Z_of_nat (nat_of_ascii "0"%char))+10*Z_of_rev_string tl end.
imports: String Ascii List ZArith little_w_string