Does anyone know what `_η_−1` means as part of the definition of `ϕ` in the <kotlin spec least upper...

# compiler

[Jake Woods]

Does anyone know what _η_−1 means as part of the definition of ϕ in the kotlin spec least upper bound algorithm? Everything else seems to be defined somewhere in the document but I can’t figure out what the substitution would be for ``_η_−1({out LUB(x_out, y_out), in GLB(x_in, y_in)}`. 🙏

[ephemient]

looks like η¯¹ is the inverse of η

[Jake Woods]

Ahhh I see, that makes a lot more sense now

[Jake Woods]

Thanks! 🙂