submodule.span

Stream: general

[petercommand]

I am trying to understand submodule.span, why can the type of Inf { p | s \sub p } (set beta) be converted to submodule \alpha \beta? Thanks!

[petercommand]

is there an option to show this information?

[Mario Carneiro]

There is a coercion on p there

[Mario Carneiro]

it is the infimum (in the lattice of submodules) of all submodules that when converted to a set are supersets of s

[Mario Carneiro]

Lean knows the inf is taken in submodules, and p is a submodule, because type inference is done from the outside in and the target type is a submodule

[petercommand]

hmm, how can I know that there is a coercion on p?

[Mario Carneiro]

If you print it there will be an up arrow

[petercommand]

ah

[petercommand]

can I know which coercion is applied?

[petercommand]

like where the coercion is defined

[petercommand]

Ah, there is only one submodule.has_coe in submodule.lean