Hello world/Newbie: Difference between revisions
→{{header|Coq}}
m (→Example) |
|||
Line 550:
...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).
=={{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}}==
| |||