1
是否可以在COQ中實施派生操作員？即，具有代數函數的運算符，如x^2並返回其導數;在這種情況下，2x。是否可以在COQ中實施派生操作員？
A
回答
2
如果您的意思是一個運算符會採用任意函數，比如Z -> Z類型並構造它的導數，那麼我認爲這是不可能的。
雖然，你可以建立自己的模型（某些類）的功能，然後你應該能夠在該類上實現這樣的運算符。
這將有助於瞭解您的最終目標和動機是什麼？
相關問題
- 1. 是否可以在開關操作員中解構對象？
- 2. 如何在派生類上強制實施靜態成員？
- 3. 是否可以讓操作員在操作中使用先驗值
- 4. 是否可以實施Akka的Webservices
- 5. 是否可以在列中操作xml？
- 6. 是否有可能在派生類中
- 7. 是否可以使用？班級成員的操作員？
- 8. 在派生類中處理派生成員的標準實踐
- 9. Java 7鑽石操作員：爲什麼難以實施？
- 10. MarkLogic node.js - 是否可以在parseBindings中支持派生值？
- 11. 是否有可能實施切換按鈕在操作菜單中使用操作欄sherlock在android
- 12. 我們是否可以在Siebel中實施此驗證碼
- 13. 地鐵UI是否受版權保護？是否可以實施？
- 14. 我可以在編譯時檢查會員功能是否爲操作員？
- 15. Python - 是否可以爲操作員設置變量？
- 16. 試圖在Dr.Retet中實施remove *操作？
- 17. 是否可以實施檢查HintDb的Coq策略？如果是這樣，怎麼樣？
- 18. 是否可以在預生成事件中更改文件的生成操作？
- 19. 如果派生類包含其他方法和成員，static_cast是否可以從基類完成派生類？
- 20. 是否可以自動生成SSIS派生列轉換？
- 21. 基類可以確定派生類是否已覆蓋虛擬成員？
- 22. C＃是否可以從派生類中調用基類屬性
- 23. 是否可以在沒有GATT的情況下實施Proximity Profile？
- 24. 我可以在If語句中使用操作員2操作員
- 25. 是否可以在C++ 0x中自動執行以下操作？
- 26. 是否可以「加入」DownloadStringAsync操作？
- 27. 是否可以攔截READ操作？
- 28. 是否可以更改UIButton的操作？
- 29. 是否可以操作使用jQuery
- 30. 是否可以創建一個Matlab實例作爲管理員？
您也可以使用該模型編寫通過反射證明來簡化[衍生物]（http://coq.inria.fr/stdlib/Coq.Reals.Rderiv.html）命題的策略。 – 2013-08-07 16:37:54