lean
lean copied to clipboard
Universe levels are ignored when using projection notation
... if the projection notation can also be interpreted as a single name:
def foo := none.get_or_else.{3 4 5} 1 -- succeeds
def bar := (none).get_or_else.{3 4 5} 1 -- fails (as expected, but error message could be better)
foo is expected to fail, either because specifying universe levels is not supported in projection notation, or because it is supported, but these are wrong universes.