Stream: Beginner Questions

Topic: Additional type variable(s) in locale specification

Robert Soeldner (Oct 11 2023 at 07:18):

I'm defining the class:

class countably_infinite =
  assumes "infinite (UNIV :: 'a set)"

and the output includes the following warning:

Additional type variable(s) in locale specification "countably_infinite": 'a
class countably_infinite = type +
  assumes "infinite UNIV"

I saw the same warning in HOL-Library.Countable, is there a general way of overcoming it or is it always ignored?

Tobias Heindel (Heliax GmbH) (May 03 2024 at 12:49):

Robert Soeldner said:

I'm defining the class:

class countably_infinite =
  assumes "infinite (UNIV :: 'a set)"

and the output includes the following warning:

Additional type variable(s) in locale specification "countably_infinite": 'a
class countably_infinite = type +
  assumes "infinite UNIV"

I saw the same warning in HOL-Library.Countable, is there a general way of overcoming it or is it always ignored?

bump

Mathias Fleury (May 03 2024 at 12:56):

class countably_infinite =
  fixes ty_p :: "'a itself"
  assumes "infinite (UNIV :: 'a set)"

For explicit instantiations you can then use TYPE('a)

Last updated: May 06 2024 at 16:21 UTC