Contents

Require Import Coq.Strings.String.

Open Scope string_scope.

Definition hello:string := "Hello, World!".

(* Unit test *)
Lemma HelloTest:
  hello = "Hello, World!" .
Proof.
  reflexivity.
Qed.

Version data entries

357 entries across 229 versions & 1 rubygems

Version	Path
trackler-2.2.1.180	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.180	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.179	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.179	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.178	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.178	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.177	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.177	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.176	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.176	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.175	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.175	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.174	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.174	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.173	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.173	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.172	tracks/coq/exercises/hello-world/example.v
trackler-2.2.1.172	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.171	tracks/coq/docs/SNIPPET.txt
trackler-2.2.1.171	tracks/coq/exercises/hello-world/example.v