1

タプルを引数とする定義を作成したいと思います。

definition my_def :: "('a × 'a) ⇒ bool" where
  "my_def (a, b) ⟷ a = b"

ただし、これは受け入れられません。エラーメッセージは

Bad arguments on lhs: "(a, b)"
The error(s) above occurred in definition:
"my_def (a, b) ≡ a = b"

fun作品の代わりに使用しdefinitionていますが、これは私が望むものではありません。次の表記も機能しますが、やや醜いです。

definition my_def :: "('a × 'a) ⇒ bool" where
  "my_def t ⟷ fst t = snd t"

タプルを引数として使用する最良の方法は何definitionですか？

4

1 に答える 1

2

使用するfunことはおそらくこれを行うための最も苦痛の少ない方法であり、定義パッケージは左側のパターンを認識しません。

別のオプションは、ラムダ式にタプルパターンを使用することです。 my_def ≡ %(a,b). a = b

于 2013-03-09T15:04:36.850 に答える