assuming a type with a given set of properties

Stream: new members

[Kayla Thomas]

Is there a way to assume a type that is an instance of multiple type classes without constructing it? For example, suppose I want to assume an arbitrary type named var_ that is infinite, countable, and has decidable equality. How would I write that? I imagine this would have to be done with something like constant var_ : Type, but I'm not sure how to say it has the given properties.

[Jireh Loreaux]

You want variable most likely, not constant.

variables {var_ : Type *} [countable var_] [decidable_eq var_] [infinite var_]

The square brackets introduce type class arguments. The curly brackets introduce implicit arguments. The asterisk makes the statements involving this variable universe polymorphic.

[Jireh Loreaux]

Oh, and I implicitly assumed you are using Lean 3.

[Jireh Loreaux]

Of course, you also need to import the relevant mathlib files containing those declarations.

[Kayla Thomas]

Thank you!

[Floris van Doorn]

Note: this does not work if the different classes share some data. You cannot assume like this that var_ is both a ring and a comm_monoid, since that will give you two multiplications that are not assumed to be related. Instead you have to assume it is a comm_ring.