Hello world/Newbie: Difference between revisions
→{{header|Coq}}
Line 555:
#* 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] (IDE). 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.
Line 561:
Eval compute in ("Hello world!"%string).
</lang>
# Evaluate the buffer:
#
# After evaluation, the message window returns:▼
#* Alternatively, press the seventh icon from the left, the underlined down arrow, to evaluate the buffer at once.
▲# After the evaluation, the message window returns:
= "Hello world!"%string
: string
| |||