This file defines functions for dealing with rational numbers as expressions.
They are not defined earlier in the hierarchy, in the tactic or meta folders, since we do not want to import data.rat.basic there.
rat.mk_numeral embeds a rational q as a numeral expression into a type supporting the needed operations. It does not need a tactic state.
rat.reflect specializes rat.mk_numeral to ℚ.
expr.of_rat behaves like rat.mk_numeral, but uses the tactic state to infer the needed structure on the target type.
expr.to_rat evaluates a normal numeral expression as a rat.
expr.eval_rat evaluates a numeral expression with arithmetic operations as a rat.
rat.mk_numeral q embeds q as a numeral expression inside a type with 0, 1, +, -, and /
type: an expression representing the target type. This must live in Type 0. has_zero, has_one, has_add: expressions of the type has_zero %%type, etc.
This function is similar to expr.of_rat but takes more hypotheses and is not tactic valued.
rat.reflect q represents the rational number q as a numeral expression of type ℚ.
Evaluates an expression as a rational number, if that expression represents a numeral or the quotient of two numerals.
Evaluates an expression as a rational number, if that expression represents a numeral, the quotient of two numerals, the negation of a numeral, or the negation of the quotient of two numerals.
Evaluates an expression into a rational number, if that expression is built up from numerals, +, -, *, /, ⁻¹
expr.of_rat α q embeds q as a numeral expression inside the type α. Lean will try to infer the correct type classes on α, and the tactic will fail if it cannot. This function is similar to rat.mk_numeral but it takes fewer hypotheses and is tactic valued.