Zulip Chat Archive

Stream: new members

Topic: assuming a type with a given set of properties


Kayla Thomas (Jan 29 2023 at 03:47):

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 (Jan 29 2023 at 04:23):

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 (Jan 29 2023 at 04:24):

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

Jireh Loreaux (Jan 29 2023 at 04:25):

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

Kayla Thomas (Jan 29 2023 at 04:32):

Thank you!

Floris van Doorn (Jan 29 2023 at 11:22):

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.


Last updated: Dec 20 2023 at 11:08 UTC