Hello world/Newbie: Difference between revisions
→{{header|Lean}}
Line 1,464:
Congratulations, your first web page is published.
</syntaxhighlight>
=={{header|Lean}}==
These are the steps to install Lean 4:
# Have a look at the [https://leanprover.github.io/lean4/doc/quickstart.html quickstart], which links to [https://www.youtube.com/watch?v=yZo6k48L0VY this video].
# Install [https://code.visualstudio.com/ VS Code], if it is not installed:
#* On Linux, run: <syntaxhighlight lang="bash">sudo snap install --classic code</syntaxhighlight>
# Start '''code''' and search in "Extensions (Ctrl+Shift+X)", and write "lean4" in the text box.
# Select the "lean4" extension and install it.
# Select "File / New File... (Alt+Ctrl+N)" and create the file "HelloWorld.lean".
# A message may pop up saying "Failed to start 'lean' language server". If that happens, press the button "Install Lean using Elan".
# Write in "HelloWorld.lean":
<syntaxhighlight lang="lean">
def main : IO Unit :=
IO.println ("Hello world!")
#eval main
</syntaxhighlight>
# Place your cursor a at the end of <code>#eval main</code>, which updates the "Lean Inforview" showing the message <code>Hello world!</code>.
=={{header|Locomotive Basic}}==
| |||