Hello world/Newbie: Difference between revisions
Content added Content deleted
| Line 1,528: | Line 1,528: | ||
# Select "File / New File... (Alt+Ctrl+N)" and create the file "HelloWorld.lean". |
# 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". |
# 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": |
# Write the following in "HelloWorld.lean": |
||
<syntaxhighlight lang="lean"> |
<syntaxhighlight lang="lean"> |
||
def main : IO Unit := |
def main : IO Unit := |
||
| Line 1,535: | Line 1,535: | ||
#eval main |
#eval main |
||
</syntaxhighlight> |
</syntaxhighlight> |
||
# Place your cursor a at the end of <code>#eval main</code>, which updates the "Lean |
# Place your cursor a at the end of <code>#eval main</code>, which updates the "Lean Infoview" showing the message <code>Hello world!</code>. |
||
=={{header|Locomotive Basic}}== |
=={{header|Locomotive Basic}}== |
||