Documentation

Lean.Meta.NatInstTesters

Functions for testing whether expressions are canonical Nat instances.

source
def Lean.Meta.isInstOfNatNat (e : Expr) :
MetaM Bool
Equations
    Instances For
      source
      def Lean.Meta.isInstAddNat (e : Expr) :
      MetaM Bool
      Equations
        Instances For
          source
          def Lean.Meta.isInstSubNat (e : Expr) :
          MetaM Bool
          Equations
            Instances For
              source
              def Lean.Meta.isInstMulNat (e : Expr) :
              MetaM Bool
              Equations
                Instances For
                  source
                  def Lean.Meta.isInstDivNat (e : Expr) :
                  MetaM Bool
                  Equations
                    Instances For
                      source
                      def Lean.Meta.isInstModNat (e : Expr) :
                      MetaM Bool
                      Equations
                        Instances For
                          source
                          def Lean.Meta.isInstNatPowNat (e : Expr) :
                          MetaM Bool
                          Equations
                            Instances For
                              source
                              def Lean.Meta.isInstPowNat (e : Expr) :
                              MetaM Bool
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.isInstHAddNat (e : Expr) :
                                  MetaM Bool
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.isInstHSubNat (e : Expr) :
                                      MetaM Bool
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.isInstHMulNat (e : Expr) :
                                          MetaM Bool
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.isInstHDivNat (e : Expr) :
                                              MetaM Bool
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.isInstHModNat (e : Expr) :
                                                  MetaM Bool
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.isInstHPowNat (e : Expr) :
                                                      MetaM Bool
                                                      Equations
                                                        Instances For
                                                          source
                                                          def Lean.Meta.isInstLTNat (e : Expr) :
                                                          MetaM Bool
                                                          Equations
                                                            Instances For
                                                              source
                                                              def Lean.Meta.isInstLENat (e : Expr) :
                                                              MetaM Bool
                                                              Equations
                                                                Instances For
                                                                  source
                                                                  def Lean.Meta.isInstDvdNat (e : Expr) :
                                                                  MetaM Bool
                                                                  Equations
                                                                    Instances For