From 123fbb7f334c1e5a645fef5d9cf5caf4c42d30dd Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Mon, 8 Feb 2021 23:37:14 +0300
Subject: [PATCH] `weakenN`'s `n` parameter was made to have zero quantity.

---
 libs/base/Data/Fin.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr
index c58069d4d..b2c9819f2 100644
--- a/libs/base/Data/Fin.idr
+++ b/libs/base/Data/Fin.idr
@@ -76,7 +76,7 @@ weaken (FS k) = FS $ weaken k
 
 ||| Weaken the bound on a Fin by some amount
 public export
-weakenN : (n : Nat) -> Fin m -> Fin (m + n)
+weakenN : (0 n : Nat) -> Fin m -> Fin (m + n)
 weakenN n FZ = FZ
 weakenN n (FS f) = FS $ weakenN n f