Zulip Chat Archive

Stream: mathlib4

Topic: A `QQ` about Nat


Scott Morrison (Oct 11 2022 at 04:13):

Another for @Gabriel Ebner, any ideas how to implement

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

Mario Carneiro (Oct 11 2022 at 04:35):

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 (Oct 11 2022 at 04:35):

honestly I would just revert to expr construction for this

Mario Carneiro (Oct 11 2022 at 04:37):

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


Last updated: Dec 20 2023 at 11:08 UTC