Explanation of current proofs

clash-lang · Apr 21, 2022 · df1b8b5 · df1b8b5
1 parent a689583
commit df1b8b5
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/clash-prelude/src/Clash/Sized/Vector/Par.hs b/clash-prelude/src/Clash/Sized/Vector/Par.hs
@@ -58,7 +58,8 @@ scanlInductiveRTree
   -> RTree n a
   -> Vec (2^n) a
 scanlInductiveRTree op tr =
-  -- I have to use sameNat and compareSNat both; otherwise it doesn't compile
+  -- I have to use sameNat and compareSNat both; the proofs that n>=1 and n~0
+  -- don't work nicely together
   case (sameNat (Proxy @n) (Proxy @0), compareSNat (SNat @n) (SNat @0), tr) of
     (Just Refl, _, LR x) -> x :> Nil
     (_, SNatGT, BR x y) ->