CODEWITHSUNDEEP
isabelle
corny
corny

Reputation: 7852

Using tuples in definitions

I want to create a definition which has a tuple as its argument.

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

However, this is not accepted. The error message is

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

Using fun instead of definition works but this is not what I want. The following notation also works but is somewhat ugly:

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

What is the best way to use tuples as arguments in a definition?

Upvotes: 1

Views: 640

Answers (1)

lsf37
lsf37

Reputation: 535

Using fun is probably the least painful way to do this, the definition package doesn't recognise patterns on the left hand side.

Another option is to use tuple patterns for lambda expressions: my_def ≡ %(a,b). a = b

Upvotes: 2

Related Questions