no syntax error

Stream: general

[Sebastien Gouezel]

The following file doesn't generate any syntax error.

import Lean

universe u

Open Function Set

Note that I have misspellt Open instead of open, but this is not a problem since Lean thinks I am declaring a new universe (and in fact three new universes called Open, Function and Set). Would it make sense to let universe work just with a single line, to prevent stupid mistakes like this one? (Otherwise, you can go on adding nonsensical typos like Theorem foo and Lean will still be happy).

[Sebastian Ullrich]

It could either be single line or indentation, which may work better for variable as well. Please open an issue!

[Sebastien Gouezel]

lean4#2684

[Yaël Dillies]

I would expect ColGt to work better here.