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

chore: missing Fin instances

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-05 16:09:18 -07:00
parent c3bb948009
commit e4410cfbf8
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -103,6 +103,9 @@ instance : HMod (Fin n) Nat (Fin n) where
instance : OfNat (Fin (no_index (n+1))) i where
ofNat := Fin.ofNat i
instance : Inhabited (Fin (no_index (n+1))) where
default := 0
theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
fun h' => absurd (eq_of_val_eq h') h

3
src/Init/Data/Hashable.lean
View file

@ -36,6 +36,9 @@ instance : Hashable UInt64 where
instance : Hashable USize where
hash n := n.toUInt64
instance : Hashable (Fin n) where
hash v := v.val.toUInt64
instance : Hashable Int where
hash
| Int.ofNat n => UInt64.ofNat (2 * n)