Def cast_znum

feat(data/num): add tactics for evaluating arithmetic expressions made of literals, including `x \le y` and `x ^ y`