Documentation

Lean.Data.Rat

structure Lean.Rat :

Type

num : Int
den : Nat

instance Lean.instBEqRat :

Equations

Lean.instBEqRat = { beq := [anonymous] }

instance Lean.instInhabitedRat :

Inhabited Lean.Rat

Equations

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

instance Lean.instToStringRat :

ToString Lean.Rat

Equations

Lean.instToStringRat = { toString := fun a => if (a.den == 1) = true then toString a.num else toString "" ++ toString a.num ++ toString "/" ++ toString a.den ++ toString "" }

instance Lean.instReprRat :

Equations

Lean.instReprRat = { reprPrec := fun a x => if (a.den == 1) = true then repr a.num else Std.Format.text (toString "(" ++ toString a.num ++ toString " : Rat)/" ++ toString a.den ++ toString "") }

@[inline]

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

Equations

Lean.Rat.normalize a = let n := Nat.gcd (Int.natAbs a.num) a.den; if (n == 1) = true then a else { num := a.num / Int.ofNat 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 Lean.Rat.normalize { num := num, den := den }

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

Equations

Lean.Rat.lt a b = if (decide (a.num < 0) && decide (b.num ≥ 0)) = true then true else if (a.num == 0) = true then decide (b.num > 0) else if (decide (a.num > 0) && decide (b.num ≤ 0)) = true then false else decide (a.num * Int.ofNat b.den < b.num * Int.ofNat a.den)

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

Equations

Lean.Rat.mul a b = let g1 := Nat.gcd a.den (Int.natAbs b.num); let g2 := Nat.gcd (Int.natAbs a.num) b.den; { num := a.num / Int.ofNat g2 * (b.num / Int.ofNat g1), den := b.den / g2 * (a.den / g1) }

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

Equations

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

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

Equations

Lean.Rat.div a b = Lean.Rat.mul a (Lean.Rat.inv b)

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

Equations

Lean.Rat.add a b = let g := Nat.gcd a.den b.den; if (g == 1) = true then { num := a.num * Int.ofNat b.den + b.num * Int.ofNat a.den, den := a.den * b.den } else let den := a.den / g * b.den; let num := Int.ofNat b.den / Int.ofNat g * a.num + Int.ofNat a.den / Int.ofNat g * b.num; let g1 := Nat.gcd (Int.natAbs num) g; if (g1 == 1) = true then { num := num, den := den } else { num := num / Int.ofNat g1, den := den / g1 }

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

Equations

Lean.Rat.sub a b = let g := Nat.gcd a.den b.den; if (g == 1) = true then { num := a.num * Int.ofNat b.den - b.num * Int.ofNat a.den, den := a.den * b.den } else let den := a.den / g * b.den; let num := Int.ofNat b.den / Int.ofNat g * a.num - Int.ofNat a.den / Int.ofNat g * b.num; let g1 := Nat.gcd (Int.natAbs num) g; if (g1 == 1) = true then { num := num, den := den } else { num := num / Int.ofNat g1, den := den / g1 }

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

Equations

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

instance Lean.Rat.instLTRat :

Equations

Lean.Rat.instLTRat = { lt := fun a b => Lean.Rat.lt a b = true }

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

Decidable (a < b)

Equations

Lean.Rat.instDecidableLtRatInstLTRat a b = inferInstanceAs (Decidable (Lean.Rat.lt a b = true))

instance Lean.Rat.instLERat :

Equations

Lean.Rat.instLERat = { le := fun a b => ¬b < a }

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

Decidable (a ≤ b)

Equations

Lean.Rat.instDecidableLeRatInstLERat a b = inferInstanceAs (Decidable ¬b < a)

instance Lean.Rat.instAddRat :

Equations

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

instance Lean.Rat.instSubRat :

Equations

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

instance Lean.Rat.instNegRat :

Equations

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

instance Lean.Rat.instMulRat :

Equations

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

instance Lean.Rat.instDivRat :

Equations

Lean.Rat.instDivRat = { div := fun a b => a * Lean.Rat.inv b }

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

OfNat Lean.Rat n

Equations

Lean.Rat.instOfNatRat = { ofNat := { num := Int.ofNat n, den := 1 } }

instance Lean.Rat.instCoeIntRat :

Coe Int Lean.Rat

Equations

Lean.Rat.instCoeIntRat = { coe := fun num => { num := num, den := 1 } }