Documentation

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

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