Hello world/Newbie: Difference between revisions
Content added Content deleted
Line 1,464: | Line 1,464: | ||
Congratulations, your first web page is published. |
Congratulations, your first web page is published. |
||
</syntaxhighlight> |
</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}}== |
=={{header|Locomotive Basic}}== |