From 865772d512cd5adcdfd3b49a78cd19d415e99199 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 11 Jun 2023 19:25:32 +0200
Subject: [PATCH] remove stale todos

---
 examples/bool.quox             | 1 -
 lib/Quox/Parser/FromParser.idr | 1 -
 lib/Quox/Reduce.idr            | 1 -
 3 files changed, 3 deletions(-)

diff --git a/examples/bool.quox b/examples/bool.quox
index 79ad6f9..98d5429 100644
--- a/examples/bool.quox
+++ b/examples/bool.quox
@@ -10,7 +10,6 @@ def boolω : 1.Bool → [ω.Bool] =
 def if : 0.(A : ★) → 1.Bool → ω.A → ω.A → A =
   λ A b t f ⇒ case1 b return A of { 'true ⇒ t; 'false ⇒ f };
 
--- [todo]: universe lifting
 def0 If : 1.Bool → 0.★ → 0.★ → ★ =
   λ b T F ⇒ case1 b return ★ of { 'true ⇒ T; 'false ⇒ F };
 
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index 637be56..7ca26e5 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -255,7 +255,6 @@ mutual
       t   => let ctx = MkNameContexts (map fromPatVar ds) (map fromPatVar ns) in
              throw $ AnnotationNeeded t.loc ctx t
 
-  -- [todo] use SN if the var is named but still unused
   private
   fromPTermTScope : {s : Nat} -> Context' PatVar d -> Context' PatVar n ->
                     SnocVect s PatVar -> PTerm ->
diff --git a/lib/Quox/Reduce.idr b/lib/Quox/Reduce.idr
index 4363ab8..4879e9f 100644
--- a/lib/Quox/Reduce.idr
+++ b/lib/Quox/Reduce.idr
@@ -14,7 +14,6 @@ import Control.Eff
 %default total
 
 
--- [fixme] rename this to Whnf and the interface to CanWhnf
 public export
 Whnf : List (Type -> Type)
 Whnf = [NameGen, Except Error]