lean icon indicating copy to clipboard operation
lean copied to clipboard

Universe levels are ignored when using projection notation

Open fpvandoorn opened this issue 4 years ago • 0 comments

... 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.

fpvandoorn avatar May 14 '21 17:05 fpvandoorn