fact: Definition string_token (rev_buf :string) : token := let buf := rev_string rev_buf in if string_dec buf "variables" then T_variables else if string_dec buf "in" then T_in else if string_dec buf "end" then T_end else if string_dec buf "while" then T_while else if string_dec buf "do" then T_do else if string_dec buf "done" then T_done else if string_dec buf "skip" then T_skip else T_id buf.
imports: String Ascii List ZArith little_w_string