From e264a18e21eccbc50c8c204ee2259f6a9a61e28a Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 27 Feb 2022 01:48:37 +0100 Subject: [PATCH] i found an issue about that 0 bug --- src/Quox/Syntax/Var.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 ? export weak : (0 p : m `LTE` n) -> Var m -> Var n weak p i = fromNatWith i.nat $ transitive (toNatLT i) p {rel=LTE}