Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Axclass with multiple type variables?

view this post on Zulip Email Gateway (Aug 18 2022 at 11:10):

From: Nicole Rauch <rauch@informatik.uni-kl.de>
Dear all,

would there be any way of using multiple type variables in an
axclass, e.g. in a cascaded definition like this:

axclass A \<subseteq> type

consts
f :: "'a::A \<Rightarrow> 'b \<Rightarrow> bool"
axclass B \<subseteq> type
f_holds: "f a b"

Here, the error message of course is

*** Multiple type variables in class axiom:
*** f a b
*** At command "axclass".

Is there any solution to establish the above construction in Isabelle?

Thanks in advance,

Nicole

view this post on Zulip Email Gateway (Aug 18 2022 at 11:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Dear Nicole,

would there be any way of using multiple type variables in an axclass,

the fact that axclasses may only depend on one type parameter is a basic
property of the underlying logical calculus. Perhaps locales plus
interpretation offer an alternative for your particular problem.

Florian
florian.haftmann.vcf
signature.asc

Last updated: May 03 2024 at 04:19 UTC