From 415a823decceced4fbef2b829ad7e77b999a2240 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 4 Dec 2023 22:49:32 +0100
Subject: [PATCH] comment out an unfinished definition lmao

---
 examples/nat.quox | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/examples/nat.quox b/examples/nat.quox
index 3b9894a..efc834d 100644
--- a/examples/nat.quox
+++ b/examples/nat.quox
@@ -149,6 +149,8 @@ def0 times-zero : (m : ℕ) → 0 ≡ timesω m 0 : ℕ =
     succ m', ih ⇒ ih
   };
 
+{-
+-- unfinished
 def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) : ℕ =
   λ m n ⇒
   case m
@@ -158,5 +160,6 @@ def0 times-succ : (m n : ℕ) → plus m (timesω m n) ≡ timesω m (succ n) :
     succ m', ih ⇒
       δ 𝑖 ⇒ plus (succ n) (ih @𝑖)
   };
+-}
 
 }