A `QQ` about Nat

Stream: mathlib4

[Scott Morrison]

Another for @Gabriel Ebner, any ideas how to implement

def ofNatQ (α : Q(Type $u)) (_ : Q(Semiring $α)) (n : ℕ) : Q($α) := ...

[Mario Carneiro]

Here is an approximation, but it doesn't get all the raw literals correct

def ofNatQ (α : Q(Type $u)) (_ : Q(Semiring $α)) (n : ℕ) : Q($α) :=
  have : Q(OfNat $α $n) := match n with
  | 0 => (q(inferInstance) : Q(OfNat $α (nat_lit 0)))
  | 1 => (q(inferInstance) : Q(OfNat $α (nat_lit 1)))
  | _+2 => q(inferInstance)
  q(OfNat.ofNat $n)

[Mario Carneiro]

honestly I would just revert to expr construction for this

[Mario Carneiro]

I tried doing something like

def RawNat := ℕ
def mkRaw (n : ℕ) : RawNat := n
instance : ToExpr RawNat where
  toExpr := mkRawNatLit
  toTypeExpr := .const ``Nat []

in order to get raw literals in the QQ world but it seems to be doing some special magic for the type Nat