diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index d555b35..b71dba5 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -102,7 +102,7 @@ toFromNat (S k) (LTESucc x) = cong S $ toFromNat k x
 
 -- not using %transform like other things because weakSpec requires the proof
 -- to be relevant. but since only `LTESucc` is ever possible that seems
--- to be a bug?
+-- to be an instance of <https://github.com/idris-lang/Idris2/issues/1259>?
 export
 weak : (0 p : m `LTE` n) -> Var m -> Var n
 weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}