include [...] analogous to omit [...]

Stream: lean4

[Anatole Dedecker]

If I have a variable [Foo], I can do omit [Foo], but I can't do include [Foo]. Is there a reason this would be a bad idea?

[Kenny Lau]

probably not, because if you do [h : Foo] then you can include h anyways

[Anatole Dedecker]

Yes but the point of the omit [Foo] syntax is precisely not having to name typeclass arguments.

[Kenny Lau]

"probably not" is referring to "Is there a reason this would be a bad idea?"

[Anatole Dedecker]

Ah sorry read your message too fast