Documentation

Lean.Meta.Tactic.Grind.Arith.CommRing.Functions

source
def Lean.Meta.Grind.Arith.CommRing.checkInst (declName : Name) (inst inst' : Expr) :
MetaM Unit
Equations
    Instances For
      source
      def Lean.Meta.Grind.Arith.CommRing.mkUnaryFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) (expectedInst : Expr) :
      m Expr
      Equations
        Instances For
          source
          def Lean.Meta.Grind.Arith.CommRing.mkBinHomoFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (type : Expr) (u : Level) (instDeclName declName : Name) (expectedInst : Expr) :
          m Expr
          Equations
            Instances For
              source
              def Lean.Meta.Grind.Arith.CommRing.mkPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) :
              m Expr
              Equations
                Instances For
                  source
                  def Lean.Meta.Grind.Arith.CommRing.mkNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] (u : Level) (type semiringInst : Expr) :
                  m Expr
                  Equations
                    Instances For
                      source
                      def Lean.Meta.Grind.Arith.CommRing.getAddFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
                      m Expr
                      Equations
                        Instances For
                          source
                          def Lean.Meta.Grind.Arith.CommRing.getSubFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
                          m Expr
                          Equations
                            Instances For
                              source
                              def Lean.Meta.Grind.Arith.CommRing.getMulFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
                              m Expr
                              Equations
                                Instances For
                                  source
                                  def Lean.Meta.Grind.Arith.CommRing.getNegFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
                                  m Expr
                                  Equations
                                    Instances For
                                      source
                                      def Lean.Meta.Grind.Arith.CommRing.getPowFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m] :
                                      m Expr
                                      Equations
                                        Instances For
                                          source
                                          def Lean.Meta.Grind.Arith.CommRing.getIntCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
                                          m Expr
                                          Equations
                                            Instances For
                                              source
                                              def Lean.Meta.Grind.Arith.CommRing.getNatCastFn {m : Type → Type} [MonadLiftT MetaM m] [Monad m] [MonadCanon m] [MonadRing m] :
                                              m Expr
                                              Equations
                                                Instances For
                                                  source
                                                  def Lean.Meta.Grind.Arith.CommRing.getOne {m : Type → Type} [Monad m] [MonadCanon m] [MonadRing m] [MonadLiftT GoalM m] :
                                                  m Expr
                                                  Equations
                                                    Instances For
                                                      source
                                                      def Lean.Meta.Grind.Arith.CommRing.getInvFn {m : Type → Type} [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadCommRing m] :
                                                      m Expr
                                                      Equations
                                                        Instances For