From 0ed58c80c51787196cfc40d529c425432b091f83 Mon Sep 17 00:00:00 2001
From: HuStmpHrrr <fdhzs2010@hotmail.com>
Date: Tue, 14 May 2024 16:20:14 -0400
Subject: [PATCH] intermediate commit

---
 theories/Extraction/Evaluation.v | 42 ++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 theories/Extraction/Evaluation.v

diff --git a/theories/Extraction/Evaluation.v b/theories/Extraction/Evaluation.v
new file mode 100644
index 00000000..b023db71
--- /dev/null
+++ b/theories/Extraction/Evaluation.v
@@ -0,0 +1,42 @@
+From Mcltt Require Import Base.
+From Mcltt Require Import Evaluation.Definitions.
+Import Domain_Notations.
+
+Generalizable All Variables.
+
+
+Inductive eval_exp_order : exp -> env -> Prop :=
+| eeo_typ :
+  `( eval_exp_order {{{ Type@i }}} p )
+| eeo_var :
+  `( eval_exp_order {{{ # x }}} p )
+| eeo_nat :
+  `( eval_exp_order {{{ ℕ }}} p )
+| eeo_zero :
+  `( eval_exp_order {{{ zero }}} p )
+| eeo_succ :
+  `( eval_exp_order {{{ M }}} p ->
+     eval_exp_order {{{ succ M }}} p )
+| eeo_natrec :
+  `( {{ eval_exp_order M p }} ->
+     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     eval_exp_order {{{ rec M return A | zero -> MZ | succ -> MS end }}} p ).
+
+| eval_exp_natrec :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ rec m ⟦return A | zero -> MZ | succ -> MS end⟧ p ↘ r }} ->
+     {{ ⟦ rec M return A | zero -> MZ | succ -> MS end ⟧ p ↘ r }} )
+| eval_exp_pi :
+  `( {{ ⟦ A ⟧ p ↘ a }} ->
+     {{ ⟦ Π A B ⟧ p ↘ Π a p B }} )
+| eval_exp_fn :
+  `( {{ ⟦ λ A M ⟧ p ↘ λ p M }} )
+| eval_exp_app :
+  `( {{ ⟦ M ⟧ p ↘ m }} ->
+     {{ ⟦ N ⟧ p ↘ n }} ->
+     {{ $| m & n |↘ r }} ->
+     {{ ⟦ M N ⟧ p ↘ r }} )
+| eval_exp_sub :
+  `( {{ ⟦ σ ⟧s p ↘ p' }} ->
+     {{ ⟦ M ⟧ p' ↘ m }} ->
+     {{ ⟦ M[σ] ⟧ p ↘ m }} )