Meta operations on ℚ
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.
Main definitions
rat.mk_numeralembeds a rationalqas a numeral expression into a type supporting the needed operations. It does not need a tactic state.rat.reflectspecializesrat.mk_numeraltoℚ.expr.of_ratbehaves likerat.mk_numeral, but uses the tactic state to infer the needed structure on the target type.expr.to_ratevaluates a normal numeral expression as a rat.expr.eval_ratevaluates 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.
c.of_rat q embeds q as a numeral expression inside the type α.
Lean will try to infer the correct type classes on c.α, 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.