max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: annotate instance

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-28 17:57:52 -08:00
parent 163cbbfe21
commit d0b8dc128b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Fin/Basic.lean
View file

@ -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 :=