Documentation

Lean.Meta.IntInstTesters

Functions for testing whether expressions are canonical Int instances.

source
def Lean.Meta.isInstOfNatInt (e : Expr) :
MetaM Bool
Equations
    Instances For
      source
      def Lean.Meta.isInstNegInt (e : Expr) :
      MetaM Bool
      Equations
        Instances For
          source
          def Lean.Meta.isInstAddInt (e : Expr) :
          MetaM Bool
          Equations
            Instances For
              source
              def Lean.Meta.isInstSubInt (e : Expr) :
              MetaM Bool
              Equations
                Instances For
                  source
                  def Lean.Meta.isInstMulInt (e : Expr) :
                  MetaM Bool
                  Equations
                    Instances For
                      source
                      def Lean.Meta.isInstDivInt (e : Expr) :
                      MetaM Bool
                      Equations
                        Instances For
                          source
                          def Lean.Meta.isInstModInt (e : Expr) :
                          MetaM Bool
                          Equations
                            Instances For
                              source
                              def Lean.Meta.isInstDvdInt (e : Expr) :
                              MetaM Bool
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.isInstHAddInt (e : Expr) :
                                  MetaM Bool
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.isInstHSubInt (e : Expr) :
                                      MetaM Bool
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.isInstHMulInt (e : Expr) :
                                          MetaM Bool
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.isInstHDivInt (e : Expr) :
                                              MetaM Bool
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.isInstHModInt (e : Expr) :
                                                  MetaM Bool
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.isInstLTInt (e : Expr) :
                                                      MetaM Bool
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Meta.isInstLEInt (e : Expr) :
                                                          MetaM Bool
                                                          Equations
                                                            Instances For