From fdf5354cd1fd03067836dad22dd3e7eb07f7e5eb Mon Sep 17 00:00:00 2001
From: Kodai Nakamura <kodai.nakamura.215@gmail.com>
Date: Sun, 19 Jan 2020 18:53:04 +0900
Subject: [PATCH] Add enum

---
 src/eval_nat_exp/mod.rs    |  1 +
 src/eval_nat_exp/proofs.rs | 12 ++++++++++++
 2 files changed, 13 insertions(+)
 create mode 100644 src/eval_nat_exp/mod.rs
 create mode 100644 src/eval_nat_exp/proofs.rs

diff --git a/src/eval_nat_exp/mod.rs b/src/eval_nat_exp/mod.rs
new file mode 100644
index 0000000..9eefe6b
--- /dev/null
+++ b/src/eval_nat_exp/mod.rs
@@ -0,0 +1 @@
+pub mod proofs;
diff --git a/src/eval_nat_exp/proofs.rs b/src/eval_nat_exp/proofs.rs
new file mode 100644
index 0000000..3617b72
--- /dev/null
+++ b/src/eval_nat_exp/proofs.rs
@@ -0,0 +1,12 @@
+use super::super::nat::proofs::*;
+use super::super::nat::Nat;
+
+pub enum ProofEvalNatExp {
+    EConst,
+    EPlus,
+    ETimes,
+    ProofPlusIs::PZero,
+    ProofPlusIs::PSucc(Box<ProofPlusIs>),
+    ProofTimeIs::TZero,
+    ProofTimeIs::TSucc(Box<ProofTimeIs>, Box<ProofPlusIs>, Nat),
+}