4
はなぜ以下です。TypeCheckます：なぜ "mod"に関連する等価性がIdrisでタイプチェックでないのですか？
v1 : mod 3 2 = 1
v1 = Refl
しかし、これは罰金です。TypeCheckます：
v2 : 3 - 2 = 1
v2 = Refl
A
答えて
5
それが原因mod機能（@AntonTrunov明確化のおかげで）の不公平に発生します。それは多相であり、デフォルトで数値定数はIntegerです。 Integerタイプmod機能について
Idris> :t mod
mod : Integral ty => ty -> ty -> ty
Idris> :t 3
3 : Integer
Idris> :t mod 3 2
mod 3 2 : Integer
合計はありません。
代わりにmodNatNZ機能を使用して、すべてのタイプのチェックが完璧で機能するようにします。
v1 : modNatNZ 3 2 SIsNotZ = 1
v1 = Refl
関連する問題
- 1. Scilabでこの等価性がFalseを返すのはなぜですか？
- 2. Idris - 2つの数値の等価性を証明する
- 3. このオブジェクトの等価性テストが失敗するのはなぜですか？
- 4. ハスケル：なぜこのタイプチェックですか？
- 5. 関連性のないセクションテンプレートの要素がないのはなぜですか？
- 6. 転置の等価性が正しくないようです。
- 7. タイプチェックには高価な理由は何ですか？
- 8. なぜGHC 7.10でタイプチェックされたこのコードは、GHC 8.0.1でタイプチェックをしなくなったのですか？
- 9. idrisにStreamのフィルタ機能がないのはなぜですか？
- 10. ノードで+ =（加算代入、等価）が遅いのはなぜですか？
- 11. =（等号）=を使った等価比較がJavaで正しく機能しないのはなぜですか？
- 12. PHPの等価性チェックでエラーが発生しない
- 13. glslで変動フロートの等価性テストが失敗するのはなぜですか？
- 14. jQuery $ .mapの等価な等価物ですか？
- 15. なぜerase（）関数が高価なのですか？
- 16. なぜ（n mod const）が（const mod n）より速いのですか？
- 17. コマンドラインでタイプチェックが必要なルールのタイプチェックを有効にするにはどうすればよいですか？
- 18. Javascriptでの等価性テスト
- 19. Ruby on OSX 10.10.5に関連するシステムファイルがないのはなぜですか？
- 20. Where-Objectは、関連するオブジェクトではなく、ソースオブジェクトの* all *プロパティを評価するのはなぜですか？
- 21. なぜデフォルト==実装は等価を呼び出さないのですか？
- 22. Clojure関数の等価性を名前で確認する
- 23. なぜPyHamcrestに負の平等マッチャーがないのですか？
- 24. なぜcollectionViewでスペーシングが等しくないのですか？
- 25. javascriptでNaNの等価性を評価するには？
- 26. アニメーション関数で要素の等価性をチェックする
- 27. 構造体がCの等価式で使用できないのはなぜですか？
- 28. なぜis_atom（nil）がエリキシルでtrueに等しいのですか？
- 29. UIStackViewディストリビューションを等価に設定すると、サブビューが表示されないのはなぜですか？
- 30. 等価ではない列挙型の比較可能性
"コンパイルステージでIdrisがタイプでパターンマッチングしか実行できません"という文句は正しくありません。たとえば、 '（the Int 3）-2 = 1'を取ると、 'Int'は帰納的データ型ではありませんが、' Refl'を使ってそれを証明できます。 'Refl'が' mod'で動作しないのは、あなたがすでに説明したように、偏見です。 –