pub open spec fn ascii_digits(bytes: Seq<u8>, start: int, end: int) -> bool
{ forall |i: int| start <= i < end ==> ascii_digit(bytes[i]) }