From d0b8dc128b000fcc439d464260ea61055d68140f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Dec 2020 17:57:52 -0800 Subject: [PATCH] chore: annotate instance --- src/Init/Data/Fin/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean index b18756aedb..8bc19067ff 100644 --- a/src/Init/Data/Fin/Basic.lean +++ b/src/Init/Data/Fin/Basic.lean @@ -80,7 +80,7 @@ instance : Div (Fin n) where instance : HMod (Fin n) Nat (Fin n) where hMod := Fin.modn -instance : OfNat (Fin (n+1)) i where +instance : OfNat (Fin (noindex! (n+1))) i where ofNat := Fin.ofNat i theorem vneOfNe {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=