Install emacs lean-mode

Stream: new members

[Raymond Baker]

Hi, I hope this is the right place to ask a "how to install" question.

I'm trying to install lean-mode for emacs. I already have lean4 installed and working.

I'm trying to follow the install instructions located on the github. But the instructions seem to presuppose that I have already downloaded some package. It thinks I already have "/path/to/lean4-mode". Where is that package supposed to come from? My guess is its the package in the github. But the documentation doesn't seem to specify and I wan't to confirm I have the right version.