lean4-htt/src/Init/Data/FloatArray
2022-07-09 16:18:29 -07:00
..
Basic.lean feat: add instance GetElem (Array α) USize α fun xs i => LT.lt i.toNat xs.size where 2022-07-09 16:18:29 -07:00