Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Polymorphic minus

Email Gateway (Aug 18 2022 at 18:24):

From: John Munroe <munddr@gmail.com>
Hi all,

If my understanding is correct, the minus operator has a polymorphic type:
'a => 'a => bool. However, if I have something like:

typedecl T

axiomatization
a :: T
where "a - a = a"

I get an error saying "No type arity T :: minus". So is the minus
polymorphic? The = operator is fine though.

Thanks in advance.

John

Email Gateway (Aug 18 2022 at 18:24):

From: René Thiemann <rene.thiemann@uibk.ac.at>

If my understanding is correct, the minus operator has a polymorphic type:
'a => 'a => bool. However, if I have something like:

But 'a must have sort minus.

typedecl T

axiomatization
a :: T
where "a - a = a"

I get an error saying "No type arity T :: minus".

I would start as follows

locale test =
fixes a :: "'T :: minus"
assumes ax1: "a - a = a"
begin

...

end

Cheers,
René

Email Gateway (Aug 18 2022 at 18:24):

From: John Munroe <munddr@gmail.com>
I see. But

fixes a :: "'T :: minus"

means that a is assigned to a type variable 'T rather than a concrete
type T. What if a is of a concrete type?

Thank you
John

Email Gateway (Aug 18 2022 at 18:24):

From: René Thiemann <rene.thiemann@uibk.ac.at>

I see. But

fixes a :: "'T :: minus"

means that a is assigned to a type variable 'T rather than a concrete
type T. What if a is of a concrete type?

Then this type T has to be in the class minus,
otherwise you cannot write "a - a".

René

2011/9/20 René Thiemann <rene.thiemann@uibk.ac.at>:

If my understanding is correct, the minus operator has a polymorphic type:
'a => 'a => bool. However, if I have something like:

But 'a must have sort minus.

I would start as follows

locale test =
fixes a :: "'T :: minus"
assumes ax1: "a - a = a"
begin

Last updated: Apr 26 2024 at 16:20 UTC