From 2cafb35bc16eb9787881a904f39127b8752df69f Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 27 Nov 2023 06:43:48 +0100
Subject: [PATCH] fix some comments

---
 lib/Quox/Whnf/Interface.idr | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/lib/Quox/Whnf/Interface.idr b/lib/Quox/Whnf/Interface.idr
index d2b11da..1fccefc 100644
--- a/lib/Quox/Whnf/Interface.idr
+++ b/lib/Quox/Whnf/Interface.idr
@@ -83,7 +83,7 @@ isTagHead (Ann (Tag {}) (Enum {}) _) = True
 isTagHead (Coe {})                   = True
 isTagHead _                          = False
 
-||| an expression like `0 ∷ ℕ` or `suc n ∷ ℕ`
+||| an expression like `𝑘 ∷ ℕ` for a natural constant 𝑘, or `suc n ∷ ℕ`
 public export %inline
 isNatHead : Elim {} -> Bool
 isNatHead (Ann (Nat  {}) (NAT {}) _) = True
@@ -160,11 +160,13 @@ isK (K {}) = True
 isK _      = False
 
 
-||| if `ty` is a type constructor, and `val` is a value of that type where a
-||| coercion can be reduced. which is the case if any of:
-||| - `ty` is an atomic type
-||| - `ty` has η
-||| - `val` is a constructor form
+||| true if `ty` is a type constructor, and `val` is a value of that type where
+||| a coercion can be reduced
+|||
+||| 1. `ty` is an atomic type
+||| 2. `ty` has an η law that is usable in this context
+|||    (e.g. η for pairs only exists when σ=0, not when σ=1)
+||| 3. `val` is a constructor form
 public export %inline
 canPushCoe : SQty -> (ty, val : Term {}) -> Bool
 canPushCoe sg (TYPE    {}) _         = True