From 8c4fe037305639f4bd9f6843d188800c7e2583c0 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sat, 16 Oct 2021 00:44:35 -0500
Subject: [PATCH] a

---
 src/LambdaPi.agda        |  2 +-
 src/Project/Lambda1.agda | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 src/Project/Lambda1.agda

diff --git a/src/LambdaPi.agda b/src/LambdaPi.agda
index c372c01b..e959807a 100644
--- a/src/LambdaPi.agda
+++ b/src/LambdaPi.agda
@@ -78,4 +78,4 @@ progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
 ----------------------------------------------------
 -- preservation
 ----------------------------------------------------
-preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
\ No newline at end of file
+preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
diff --git a/src/Project/Lambda1.agda b/src/Project/Lambda1.agda
new file mode 100644
index 00000000..f3fb6396
--- /dev/null
+++ b/src/Project/Lambda1.agda
@@ -0,0 +1,19 @@
+module Project.Lambda1 where
+
+open import Data.Nat using (ℕ; suc; _≟_)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (yes; no; ¬_)
+
+data Term : Set where
+  `_ : ℕ →  Term
+  ƛ_ : Term →  Term
+  _·_ : Term →  Term →  Term
+
+  `suc _ : Term →  Term
+  `zero : Term
+
+data Value : Term →  Set where
+  V-ƛ : ∀ {N} →  Value (ƛ N)
+
+data Context : Set where
+  ⊙ : Context