Building an `Expr` from a numeric literal

Stream: Is there code for X?

[Eric Wieser]

Do we have these hiding anywhere?

def _root_.Lean.Expr.ofNatQ (α : Q(Type u)) (_aα : Q(AddMonoidWithOne $α)) : ℕ → Q($α)
  | 0 => q(0)
  | 1 => q(1)
  | n + 2 =>
    have ne : Q(ℕ) := Lean.mkRawNatLit n
    have ne2 : Q(ℕ) := Lean.mkRawNatLit (n + 2)
    letI : $ne2 =Q $ne + 2 := ⟨⟩
    q(OfNat.ofNat $ne2)

def _root_.Lean.Expr.ofIntQ (α : Q(Type u)) (_aα : Q(AddGroupWithOne $α)) : ℤ → Q($α)
  | .ofNat n => Lean.Expr.ofNatQ α q(inferInstance) n
  | .negSucc n => q(-$(Lean.Expr.ofNatQ α q(inferInstance) (n + 1)))

def _root_.Lean.Expr.ofRatQ (α : Q(Type u)) (_aα : Q(AddGroupWithOne $α)) (_dα : Q(Div $α)) (q : Rat) :
    Q($α) :=
  if q.den = 1 then
    Lean.Expr.ofIntQ α q(inferInstance) q.num
  else
    q($(Lean.Expr.ofIntQ α q(inferInstance) q.num) / $(Lean.Expr.ofNatQ α q(inferInstance) q.den))

[Eric Wieser]

docs#Mathlib.Meta.NormNum.mkOfNat is close, but it only works for the first case, and (unecessarily) lives in MetaM