Productions

options : number(s)
number  : prefix /\d+/
prefix  : 'num' | '#'