Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Multiple type variables in class specification

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

From: Steve Wong <s.wong.731@gmail.com>
Hi all,

Is there a way to use several type variables in a class specification. For
example:

class test =
fixes foo :: "('a => 'b => 'c) => 'a itself => bool"

With the above, Isabelle complains about having multiple type variables.

Thanks!

Steve

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

From: Ramana Kumar <rk436@cam.ac.uk>
On Thu, Sep 1, 2011 at 11:28 PM, Steve Wong <s.wong.731@gmail.com> wrote:

Hi all,

Is there a way to use several type variables in a class specification. For
example:

class test =
 fixes foo :: "('a => 'b => 'c) => 'a itself => bool"

With the above, Isabelle complains about having multiple type variables.

I believe this is a fundamental limitation of type classes (or at
least this implementation thereof): only one type variable allowed.
You may want to consider using a locale instead.
(More experienced/knowledgeable users please correct me if I'm wrong!)

Thanks!

Steve

Last updated: Nov 21 2024 at 12:39 UTC