Hello world/Newbie: Difference between revisions
Content added Content deleted
m (→Example) |
|||
| Line 550: | Line 550: | ||
...which is also how you load source files in order to add their definitions to your program. |
...which is also how you load source files in order to add their definitions to your program. |
||
SBCL has the <code>save-lisp-and-die</code> function, which saves whatever has been defined in the REPL into a stand-alone executable that includes a copy of SBCL itself (because Lisp programs can generate, compile, and run additional Lisp code at runtime, and then reference functions and variables created by that generated code). |
SBCL has the <code>save-lisp-and-die</code> function, which saves whatever has been defined in the REPL into a stand-alone executable that includes a copy of SBCL itself (because Lisp programs can generate, compile, and run additional Lisp code at runtime, and then reference functions and variables created by that generated code). |
||
=={{header|Coq}}== |
|||
# Install [https://coq.inria.fr/download Coq]: |
|||
#* On Windows and MacOS, download the [https://github.com/coq/platform/releases most recent release]. |
|||
#* On Linux, run: <lang bash>sudo snap install coq-prover</lang> |
|||
# Open '''coqide''', the [https://coq.inria.fr/refman/practical-tools/coqide.html Coq Integrated Development Environment]. The large window on the left shows the current ''script buffer'', the upper window on the right is the ''goal window'', and below is the ''message window''. |
|||
# Write in the script buffer: <lang coq> |
|||
Require Import Coq.Strings.String. |
|||
Eval compute in ("Hello world!"%string). |
|||
</lang> |
|||
# On the top of the IDE, the third icon from the right is a down arrow. Press it twice to make the IDE evaluate the buffer. |
|||
# After evaluation, the message window returns: |
|||
= "Hello world!"%string |
|||
: string |
|||
=={{header|Corescript}}== |
=={{header|Corescript}}== |
||