Documentation

Lean.Data.Rat

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

source
structure Lean.Rat :
Type
Instances For
    source
    instance Lean.instInhabitedRat :
    Inhabited Lean.Rat
    source
    instance Lean.instBEqRat :
    BEq Lean.Rat
    source
    instance Lean.instDecidableEqRat :
    DecidableEq Lean.Rat
    source
    instance Lean.instToStringRat :
    ToString Lean.Rat
    source
    instance Lean.instReprRat :
    Repr Lean.Rat
    source
    @[inline]
    def Lean.Rat.normalize (a : Lean.Rat) :
    Lean.Rat
    Instances For
      source
      def Lean.mkRat (num : Int) (den : Nat) :
      Lean.Rat
      Instances For
        source
        def Lean.Rat.isInt (a : Lean.Rat) :
        Bool
        Instances For
          source
          def Lean.Rat.lt (a : Lean.Rat) (b : Lean.Rat) :
          Bool
          Instances For
            source
            def Lean.Rat.mul (a : Lean.Rat) (b : Lean.Rat) :
            Lean.Rat
            Instances For
              source
              def Lean.Rat.inv (a : Lean.Rat) :
              Lean.Rat
              Instances For
                source
                def Lean.Rat.div (a : Lean.Rat) (b : Lean.Rat) :
                Lean.Rat
                Instances For
                  source
                  def Lean.Rat.add (a : Lean.Rat) (b : Lean.Rat) :
                  Lean.Rat
                  Instances For
                    source
                    def Lean.Rat.sub (a : Lean.Rat) (b : Lean.Rat) :
                    Lean.Rat
                    Instances For
                      source
                      def Lean.Rat.neg (a : Lean.Rat) :
                      Lean.Rat
                      Instances For
                        source
                        def Lean.Rat.floor (a : Lean.Rat) :
                        Int
                        Instances For
                          source
                          def Lean.Rat.ceil (a : Lean.Rat) :
                          Int
                          Instances For
                            source
                            instance Lean.Rat.instLTRat :
                            LT Lean.Rat
                            source
                            instance Lean.Rat.instDecidableLtRatInstLTRat (a : Lean.Rat) (b : Lean.Rat) :
                            Decidable (a < b)
                            source
                            instance Lean.Rat.instLERat :
                            LE Lean.Rat
                            source
                            instance Lean.Rat.instDecidableLeRatInstLERat (a : Lean.Rat) (b : Lean.Rat) :
                            Decidable (a ≤ b)
                            source
                            instance Lean.Rat.instAddRat :
                            Add Lean.Rat
                            source
                            instance Lean.Rat.instSubRat :
                            Sub Lean.Rat
                            source
                            instance Lean.Rat.instNegRat :
                            Neg Lean.Rat
                            source
                            instance Lean.Rat.instMulRat :
                            Mul Lean.Rat
                            source
                            instance Lean.Rat.instDivRat :
                            Div Lean.Rat
                            source
                            instance Lean.Rat.instOfNatRat {n : Nat} :
                            OfNat Lean.Rat n
                            source
                            instance Lean.Rat.instCoeIntRat :
                            Coe Int Lean.Rat