Commit 2022-11-18 00:25 04e42dee

View on Github →

feat: port data.num.basic (#607) Mathlib3 SHA: aab56fd783b265168f660d6b46709961153c4c20 Notes:

  1. This is the first file I've ported, so I'm sure I've made some errors somewhere; be on the lookout!
  2. The deriving has_reflect instances have been omitted because the corresponding class Lean.ToExpr has no default implementation currently, and these can safely be omitted for now.
  3. castPosNum (and a few friends nearby) are marked as deprecated because it uses the deprecated bit0 and bit1 in its implementation.
  4. Num.ofNat' needed to be redefined from scratch because there is no corresponding declaration for nat.binary_rec in Lean 4.

Estimated changes

added def Num.bit
added def Num.cmp
added def Num.div2
added def Num.div
added def Num.gcd
added def Num.gcdAux
added def Num.mod
added def Num.natSize
added def Num.ofNat'
added def Num.ofZNum'
added def Num.ofZNum
added def Num.ppred
added def Num.pred
added def Num.psub
added def Num.size
added def Num.sub'
added def Num.succ'
added def Num.succ
added def Num.toZNum
added def Num.toZNumNeg
added inductive Num
added def PosNum.bit
added def PosNum.cmp
added def PosNum.div'
added def PosNum.divMod
added def PosNum.divModAux
added def PosNum.isOne
added def PosNum.mod'
added def PosNum.natSize
added def PosNum.ofNat
added def PosNum.ofNatSucc
added def PosNum.ofZNum'
added def PosNum.ofZNum
added def PosNum.pred'
added def PosNum.pred
added def PosNum.size
added def PosNum.sub'
added def PosNum.succ
added inductive PosNum
added def ZNum.abs
added def ZNum.cmp
added def ZNum.div
added def ZNum.gcd
added def ZNum.mod
added def ZNum.ofInt'
added def ZNum.pred
added def ZNum.succ
added def ZNum.zNeg
added inductive ZNum
added def castNum
added def castPosNum
added def castZNum