Stream: Beginner Questions

Topic: Additional type variable(s) in locale specification

view this post on Zulip 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?

Last updated: Apr 27 2024 at 20:14 UTC