Unexpected Identifier ':' expected command

Stream: new members

[Linski]

I have been consistently getting the error in the title from Lean simply on the expression 'constant a: Type' and it doesn't seem like anyone has a solution anywhere. I just installed Lean on WSL Ubuntu and I'm editing Lean with Neovim, if anyone could help it would be greatly appreciated.

[Linski]

Wait nevermind found a great solution

[Linski]

switching to Coq

[Mario Carneiro]

constant is not legal lean 4 syntax. Did you mean axiom or opaque?

[Mario Carneiro]

My guess is that you are reading some lean 3 materials, point it out so we can fix it