mathlib documentation

data.rat.meta_defs

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 #

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.

@[protected, instance]
meta def rat.reflect  :

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

meta def rat.to_pexpr (q : ) :

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

@[protected]
meta def expr.to_nonneg_rat  :

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

@[protected]
meta def expr.to_rat  :

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.

@[protected]
meta def expr.eval_rat  :

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

@[protected]
meta def expr.of_rat (α : 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.

@[protected]

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.