Meta operations on ℚ #
This file defines functions for dealing with rational numbers as expressions.
They are not defined earlier in the hierarchy, in the
meta folders, since we do not
want to import
Main definitions #
rat.mk_numeralembeds a rational
qas a numeral expression into a type supporting the needed operations. It does not need a tactic state.
expr.to_ratevaluates a normal numeral expression as a rat.
expr.eval_ratevaluates a numeral expression with arithmetic operations as a rat.