Commit 2022-11-18 00:25 04e42dee
View on Github →feat: port data.num.basic (#607) Mathlib3 SHA: aab56fd783b265168f660d6b46709961153c4c20 Notes:
- This is the first file I've ported, so I'm sure I've made some errors somewhere; be on the lookout!
- The
deriving has_reflect
instances have been omitted because the corresponding classLean.ToExpr
has no default implementation currently, and these can safely be omitted for now. castPosNum
(and a few friends nearby) are marked as deprecated because it uses the deprecatedbit0
andbit1
in its implementation.Num.ofNat'
needed to be redefined from scratch because there is no corresponding declaration fornat.binary_rec
in Lean 4.