hmm

src/Homework2.agda

@@ -94,16 +94,16 @@ postulate
 open import Debug.Trace
 
 postulate
-  makeProofEven : ∀ (n m : ℕ) → 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 ≤′ 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)

src/OtherShit.agda

@@ -12,19 +12,19 @@ data Bin : Set where
   _I : Bin → Bin
   _II : Bin → Bin
 
-data Bool : Set where
+data even : ℕ → Set
-  true : Bool
+data odd  : ℕ → Set
-  false : Bool
 
-T : Bool → Set
+data even where
-T true = ⊤
+  zero : even zero
-T false = ⊥
+  suc  : ∀ {n : ℕ} → odd n → even (suc n)
 
-T→≡ : ∀ (b : Bool) → T b → b ≡ true
+data odd where
-T→≡ true tt = refl
+  suc  : ∀ {n : ℕ} → even n → odd (suc n)
-T→≡ false ()
 
-data parity : ℕ → Set → Set where
+to : ℕ → Bin
-  zero : parity zero
+to zero = O
-  oddSuc : ∀ {n : ℕ} → parity n → parity (evenSuc n)
+to n with odd n
-  evenSuc  : ∀ {n : ℕ} → parity n → parity (oddSuc n)
+... | x = O I
+to n with even n
+... | x = O II