Hello world/Newbie: Difference between revisions
m
→{{header|Lean}}
Line 1,528:
# 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 the following in "HelloWorld.lean":
<syntaxhighlight lang="lean">
def main : IO Unit :=
Line 1,535:
#eval main
</syntaxhighlight>
# Place your cursor a at the end of <code>#eval main</code>, which updates the "Lean
=={{header|Locomotive Basic}}==
| |||