From 87fafc7a15c1b5de3fca3f7c77920a60e1c13381 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Wed, 6 Oct 2021 13:37:19 -0500
Subject: [PATCH] hmm

---
 src/Homework2.agda | 10 +++++-----
 src/OtherShit.agda | 26 +++++++++++++-------------
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/Homework2.agda b/src/Homework2.agda
index cb5fecc2..5f049b0c 100644
--- a/src/Homework2.agda
+++ b/src/Homework2.agda
@@ -94,16 +94,16 @@ postulate
 open import Debug.Trace
 
 postulate
-  makeProofEven : ∀ (n m : ℕ) → m * 2 ≡ n → suc m ≤′ n
-  makeProofOdd : ∀ (n m : ℕ) → suc (m * 2) ≡ n → suc m ≤′ n
+  makeProofEven : ∀ (n m : ℕ) → m * 2 ≡ n → suc m ≤′ suc n
+  makeProofOdd : ∀ (n m : ℕ) → suc (m * 2) ≡ n → suc m ≤′ suc n
 
 to' : (n : ℕ) → Terminating n → Bin
 to' zero _ = O
-to' n (box mWit) with parity? n
+to' (suc n) (box mWit) with parity? n
 -- this means n is odd
-... | ⟨ m , isOdd p ⟩ = (to' m (mWit (makeProofOdd n m p))) I
+... | ⟨ m , isOdd p ⟩ = (to' m (mWit (makeProofOdd n m p))) II
 -- this means n is even
-... | ⟨ m , isEven p ⟩ = (to' m (mWit (makeProofEven n m p))) II
+... | ⟨ m , isEven p ⟩ = (to' m (mWit (makeProofEven n m p))) I
 
 to : (n : ℕ) → Bin
 to n = to' n (term n)
diff --git a/src/OtherShit.agda b/src/OtherShit.agda
index 79399397..472f1469 100644
--- a/src/OtherShit.agda
+++ b/src/OtherShit.agda
@@ -12,19 +12,19 @@ data Bin : Set where
   _I : Bin → Bin
   _II : Bin → Bin
 
-data Bool : Set where
-  true : Bool
-  false : Bool
+data even : ℕ → Set
+data odd  : ℕ → Set
 
-T : Bool → Set
-T true = ⊤
-T false = ⊥
+data even where
+  zero : even zero
+  suc  : ∀ {n : ℕ} → odd n → even (suc n)
 
-T→≡ : ∀ (b : Bool) → T b → b ≡ true
-T→≡ true tt = refl
-T→≡ false ()
+data odd where
+  suc  : ∀ {n : ℕ} → even n → odd (suc n)
 
-data parity : ℕ → Set → Set where
-  zero : parity zero
-  oddSuc : ∀ {n : ℕ} → parity n → parity (evenSuc n)
-  evenSuc  : ∀ {n : ℕ} → parity n → parity (oddSuc n)
+to : ℕ → Bin
+to zero = O
+to n with odd n
+... | x = O I
+to n with even n
+... | x = O II
\ No newline at end of file