set coercion

Stream: lean4

[Nir Paz]

Can I define a coercion or something so that this works?

import Mathlib

structure Foo (α : Type*) where
  carrier : Set α
  prop : True

variable (α : Type*) (foo : Foo α)

#check foo ⊆ Set.univ -- fails

I want foo ⊆ S to be interpreted as foo.carrier ⊆ S whenever S : Set α.

[Nir Paz]

Actually I would like #foo and similar things to also work, so lean should always tries to interpret foo as foo.carrier. I assume things like this exist in mathlib but I can't think of an example to check.

[Vasilii Nesterov]

The problem here is that a ⊆ b is just a notation for Subset a b which expects instance of HasSubset for the type of a and b, and this isn't connected to Set.

[Nir Paz]

Looks like #S typechecks when S : UpperSet α (which is a carrier and a property), so I'll see what's done there.

[Nir Paz]

Although subsets don't work, so I will add a HasSubset instance manually.

[Nir Paz]

It must be SetLike, I'll take a look at it later.

[Jireh Loreaux]

Yes, you want to write a docs#SetLike instance for Foo.