Documentation

Lean.Data.Rat

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

structure Lean.Rat :

num : Int
den : Nat

Instances For

instance Lean.instInhabitedRat :

Inhabited Lean.Rat

Equations

Lean.instInhabitedRat = { default := { num := default, den := default } }

instance Lean.instBEqRat :

Equations

Lean.instBEqRat = { beq := Lean.beqRat✝ }

instance Lean.instDecidableEqRat :

DecidableEq Lean.Rat

Equations

Lean.instDecidableEqRat = Lean.decEqRat✝

instance Lean.instToStringRat :

ToString Lean.Rat

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]

def Lean.Rat.normalize (a : Lean.Rat) :

Equations

a.normalize = let n := a.num.natAbs.gcd a.den; if (n == 1) = true then a else { num := a.num.div ↑n, den := a.den / n }

def Lean.mkRat (num : Int) (den : Nat) :

Equations

Lean.mkRat num den = if (den == 0) = true then { num := 0, den := 1 } else { num := num, den := den }.normalize

def Lean.Rat.isInt (a : Lean.Rat) :

Equations

a.isInt = (a.den == 1)

def Lean.Rat.lt (a : Lean.Rat) (b : Lean.Rat) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Rat.mul (a : Lean.Rat) (b : Lean.Rat) :

Equations

a.mul b = let g1 := a.den.gcd b.num.natAbs; let g2 := a.num.natAbs.gcd b.den; { num := a.num.div ↑g2 * b.num.div ↑g1, den := b.den / g2 * (a.den / g1) }

def Lean.Rat.inv (a : Lean.Rat) :

Equations

a.inv = if a.num < 0 then { num := -↑a.den, den := a.num.natAbs } else if (a.num == 0) = true then a else { num := ↑a.den, den := a.num.natAbs }

def Lean.Rat.div (a : Lean.Rat) (b : Lean.Rat) :

Equations

a.div b = a.mul b.inv

def Lean.Rat.add (a : Lean.Rat) (b : Lean.Rat) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Rat.sub (a : Lean.Rat) (b : Lean.Rat) :

Equations

One or more equations did not get rendered due to their size.

def Lean.Rat.neg (a : Lean.Rat) :

Equations

a.neg = { num := -a.num, den := a.den }

def Lean.Rat.floor (a : Lean.Rat) :

Equations

a.floor = if (a.den == 1) = true then a.num else let r := a.num.mod ↑a.den; if a.num < 0 then r - 1 else r

def Lean.Rat.ceil (a : Lean.Rat) :

Equations

a.ceil = if (a.den == 1) = true then a.num else let r := a.num.mod ↑a.den; if a.num > 0 then r + 1 else r

instance Lean.Rat.instLT :

Equations

Lean.Rat.instLT = { lt := fun (a b : Lean.Rat) => a.lt b = true }

instance Lean.Rat.instDecidableLt (a : Lean.Rat) (b : Lean.Rat) :

Decidable (a < b)

Equations

a.instDecidableLt b = inferInstanceAs (Decidable (a.lt b = true))

instance Lean.Rat.instLE :

Equations

Lean.Rat.instLE = { le := fun (a b : Lean.Rat) => ¬b < a }

instance Lean.Rat.instDecidableLe (a : Lean.Rat) (b : Lean.Rat) :

Decidable (a ≤ b)

Equations

a.instDecidableLe b = inferInstanceAs (Decidable ¬b < a)

instance Lean.Rat.instAdd :

Equations

Lean.Rat.instAdd = { add := Lean.Rat.add }

instance Lean.Rat.instSub :

Equations

Lean.Rat.instSub = { sub := Lean.Rat.sub }

instance Lean.Rat.instNeg :

Equations

Lean.Rat.instNeg = { neg := Lean.Rat.neg }

instance Lean.Rat.instMul :

Equations

Lean.Rat.instMul = { mul := Lean.Rat.mul }

instance Lean.Rat.instDiv :

Equations

Lean.Rat.instDiv = { div := fun (a b : Lean.Rat) => a * b.inv }

instance Lean.Rat.instOfNat {n : Nat} :

OfNat Lean.Rat n

Equations

Lean.Rat.instOfNat = { ofNat := { num := ↑n, den := 1 } }

instance Lean.Rat.instCoeInt :

Coe Int Lean.Rat

Equations

Lean.Rat.instCoeInt = { coe := fun (num : Int) => { num := num, den := 1 } }