From 23ca813c8c61a34dad0e4f078e0dbf1e2585e4a9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 19 Oct 2017 15:25:03 +0200
Subject: [PATCH] Define instructions

---
 wp.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 wp.v

diff --git a/wp.v b/wp.v
new file mode 100644
index 0000000..e3cfc04
--- /dev/null
+++ b/wp.v
@@ -0,0 +1,18 @@
+(* Projet Coq - WP - MPRI 2.7.1 *)
+
+(***** Partie 1 : definition de While ****************************************)
+
+Require Import ZArith.BinInt.
+Import Z.
+
+Parameter Var: Type.
+Definition Mem := Var -> Z.
+Definition Expr:= Mem -> Z.
+
+Inductive Instr : Type :=
+| skip: Instr
+| abort: Instr
+| assign: Var -> Expr -> Instr
+| seq: Instr -> Instr -> Instr
+| ifelse: Expr -> Instr -> Instr -> Instr
+| while: Expr -> Instr -> Instr.