Function decimal_mark 

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

{ b == ASCII_FULL_STOP || b == ASCII_COMMA }