Adding Coq hello world program (#1423)
* Create Coq.v * Update readme.md * Removed useless things * Update c/Coq.v Co-authored-by: Gabe <66077254+MrBrain295@users.noreply.github.com>
This commit is contained in:
11
c/Coq.v
Normal file
11
c/Coq.v
Normal file
@@ -0,0 +1,11 @@
|
||||
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").
|
||||
Reference in New Issue
Block a user