정의에서 튜플 사용

Question

튜플을 인수로 갖는 정의를 만들고 싶습니다.

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

그러나 이것은 허용되지 않습니다. 오류 메시지가 fun 대신 definition의 작품을 사용

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

그러나 이것은 내가 원하는 것이 아니다. 다음 표기는 작동하지만 다소 못생긴 :

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

definition에 인수로 튜플을 사용하는 가장 좋은 방법은 무엇입니까?

Answer 1

아마도 fun을 사용하는 것이 가장 쉬운 방법 일 수 있습니다. 정의 패키지는 왼쪽의 패턴을 인식하지 못합니다.

또 다른 옵션은 람다 표현식 튜플 패턴을 사용하는 것입니다 my_def ≡ %(a,b). a = b