1

是否可以在 COQ 中实现导数运算符？也就是说，一个运算符，它接受一个代数函数，例如x^2并返回它的导数；在这种情况下，2x。

4

1 回答 1

2

如果您的意思是一个可以采用任意函数的运算符，比如类型Z -> Z并构造它的导数，那么我相信这是不可能的。

虽然，您可以构建自己的（某些类）函数模型，然后您应该能够在该类上实现这样的运算符。

知道你的最终目标和动机是什么会很有帮助？

于 2013-08-05T04:11:33.873 回答