Ring constants as a Expr

Stream: Is there code for X?

[Riyaz Ahuja]

Is there an easy way to get the Lean.Expr for 0:R and 1:R for a ring R?

[Edward van de Meent]

in what context?

[Kyle Miller]

docs#Lean.Meta.mkNumeral

[Edward van de Meent]

if you're doing Qq stuff, i imagine there is a more obvious way?

[Edward van de Meent]

i.e. something along the lines of one (R : Q(Type u)) : Q($R) := q(1:$R)? idk, i haven't used Qq that much yet

[Aaron Liu]

This works in the web editor

import Mathlib

open Qq

def one (R : Q(Type u)) (inst : Q(Ring $R)) : Q($R) := q(1:$R)

[Kyle Miller]

There's a difference between mkNumeral and this Qq-based one. The mkNumeral function resolves the instance at run time, getting the OfNat instance directly, but one causes the instance to go through the Ring instance.

import Mathlib

open Qq
open Lean

def one {u : Level} (R : Q(Type u)) (inst : Q(Ring $R)) : Q($R) := q(1:$R)

#eval do return one q(Int) (← synthInstanceQ q(Ring Int))
/-
(((Expr.const `OfNat.ofNat [Level.zero]).app (Expr.const `Int [])).app (Expr.lit (Literal.natVal 1))).app
  (((Expr.const `One.toOfNat1 [Level.zero]).app (Expr.const `Int [])).app
    (((Expr.const `AddMonoidWithOne.toOne [Level.zero]).app (Expr.const `Int [])).app
      (((Expr.const `AddGroupWithOne.toAddMonoidWithOne [Level.zero]).app (Expr.const `Int [])).app
        (((Expr.const `Ring.toAddGroupWithOne [Level.zero]).app (Expr.const `Int [])).app
          (Expr.const `Int.instRing [])))))
-/
#eval Meta.mkNumeral (mkConst ``Int) 1
/-
(((Expr.const `OfNat.ofNat [Level.zero]).app (Expr.const `Int [])).app (Expr.lit (Literal.natVal 1))).app
  ((Expr.const `instOfNat []).app (Expr.lit (Literal.natVal 1)))
-/

[Kyle Miller]

It probably doesn't matter in practice, but the fact the instance is resolved at compile time for one is worth knowing.