# Documentation

## Lean.Data.Rat

Rational numbers for implementing decision procedures. We should not confuse them with the Mathlib rational numbers.

structure Lean.Rat :
Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
instance Lean.instReprRat :
Equations
• One or more equations did not get rendered due to their size.
@[inline]
Equations
Instances For
def Lean.mkRat (num : Int) (den : Nat) :
Equations
Instances For
Equations
• = (a.den == 1)
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
• = if a.num < 0 then { num := -a.den, den := Int.natAbs a.num } else if (a.num == 0) = true then a else { num := a.den, den := Int.natAbs a.num }
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• = { num := -a.num, den := a.den }
Instances For
Equations
• = if (a.den == 1) = true then a.num else let r := Int.mod a.num a.den; if a.num < 0 then r - 1 else r
Instances For
Equations
• = if (a.den == 1) = true then a.num else let r := Int.mod a.num a.den; if a.num > 0 then r + 1 else r
Instances For
Equations
Equations
Equations
instance Lean.Rat.instOfNatRat {n : Nat} :
Equations
• Lean.Rat.instOfNatRat = { ofNat := { num := n, den := 1 } }
Equations