From 7b3ccfc45a912f52e80a5f419b6177b0ae1e7c93 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 2 Jun 2024 17:34:52 +0200
Subject: [PATCH] comment out a partial definition in list.quox

---
 stdlib/list.quox | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/stdlib/list.quox b/stdlib/list.quox
index 2bab51e..5b34ee4 100644
--- a/stdlib/list.quox
+++ b/stdlib/list.quox
@@ -144,6 +144,7 @@ def elimω2 : 0.(A B : ★) → 0.(P : (n : ℕ) → Vec n A → Vec n B → ★
         pc x y n xs ys (IH xs ys)
     }
 
+{-
 postulate elimP :
     ω.(π : NzQty) → ω.(ρₙ ρₗ : Qty) →
     0.(A : ★) → 0.(P : (n : ℕ) → Vec n A → ★) →
@@ -156,6 +157,7 @@ postulate elimP :
   =
   λ π ρₙ ρₗ A P ⇒ uhhhhhhhhhhhhhhhhhhh
 -}
+-}
 
 def elimω2-uneven :
     0.(A B : ★) → 0.(P : (m n : ℕ) → Vec m A → Vec n B → ★) →