f92f2fde6c
* Create Coq.v * Update readme.md * Removed useless things * Update c/Coq.v Co-authored-by: Gabe <66077254+MrBrain295@users.noreply.github.com>
11 lines
313 B
Coq
11 lines
313 B
Coq
Require Import Coq.Lists.List.
|
|
Require Import Io.All.
|
|
Require Import Io.System.All.
|
|
Require Import ListString.All.
|
|
|
|
Import ListNotations.
|
|
Import C.Notations.
|
|
|
|
(** The classic Hello World program. *)
|
|
Definition hello_world (argv : list LString.t) : C.t System.effect unit :=
|
|
System.log (LString.s "Hello World"). |