a

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
+preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A

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