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
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    @[inline]
    Equations
    • a.normalize = if (a.num.natAbs.gcd a.den == 1) = true then a else { num := a.num.div (a.num.natAbs.gcd a.den), den := a.den / a.num.natAbs.gcd a.den }
    Instances For
      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
      Instances For
        Equations
        • a.isInt = (a.den == 1)
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • a.mul b = { num := a.num.div (a.num.natAbs.gcd b.den) * b.num.div (a.den.gcd b.num.natAbs), den := b.den / a.num.natAbs.gcd b.den * (a.den / a.den.gcd b.num.natAbs) }
            Instances For
              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 }
              Instances For
                Equations
                • a.div b = a.mul b.inv
                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
                      • a.neg = { num := -a.num, den := a.den }
                      Instances For
                        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
                        Instances For
                          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
                          Instances For
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            Equations
                            • Lean.Rat.instOfNat = { ofNat := { num := n, den := 1 } }
                            Equations