with_top vs with_bot

Stream: general

[Yaël Dillies]

docs#with_top.some_lt_none and docs#with_bot.none_lt_some don't have the same argument implicitness. Do we want a implicit or explicit?

[Anne Baanen]

(Assuming you mean docs#with_bot.bot_lt_some - that inconsistency should also be fixed!) My instinct is to have a explicit since it's not inferrable from any other parameter. Though I would only change this in practice if I find I have to write a lot of @s.

[Yaël Dillies]

Argh yes, I already mentally corrected that first inconsistency! Note that we also have docs#with_top.coe_lt_top and docs#with_bot.bot_lt_coe that syntactically apply to the coercion and bot/top.