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_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.

source

meta def rat.mk_numeral (type has_zero has_one has_add has_neg has_div : expr) :

ℚ → expr

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.

source

@[protected, instance]

meta def rat.reflect :

has_reflect ℚ

rat.reflect q represents the rational number q as a numeral expression of type ℚ.

source

meta def rat.to_pexpr (q : ℚ) :

pexpr

rat.to_pexpr q creates a pexpr that will evaluate to q. The pexpr does not hold any typing information: to_expr ``((%%(rat.to_pexpr (3/4)) : K)) will create a native K numeral (3/4 : K).

source

@[protected]

meta def expr.to_nonneg_rat :

expr → option ℚ

Evaluates an expression as a rational number, if that expression represents a numeral or the quotient of two numerals.

source

@[protected]

meta def expr.to_rat :

expr → option ℚ

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.

source

@[protected]

meta def expr.eval_rat :

expr → option ℚ

Evaluates an expression into a rational number, if that expression is built up from numerals, +, -, *, /, ⁻¹

source

@[protected]

meta def expr.of_rat (α : expr) :

ℚ → tactic expr

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.

source

@[protected]

meta def tactic.instance_cache.of_rat (c : tactic.instance_cache) :

ℚ → tactic (tactic.instance_cache × expr)

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.