Function ascii_digit 

pub open spec fn ascii_digit(b: u8) -> bool

{ ASCII_ZERO <= b <= ASCII_NINE }