expr.of_nat

Stream: lean4

[Scott Morrison]

If I have a t : Expr representing a type that I hope supports numerals, and an n : Nat, how do I generate the Expr with type t corresponding to n?

In mathlib3 this is provided as expr.of_nat.

[Gabriel Ebner]

This requires type class synthesis. I would do

mkAppOptM ``OfNat.ofNat #[type, mkRawNatLit n, none]

[Gabriel Ebner]

But it makes sense to bundle that up in a function somewhere.

[Scott Morrison]

Thanks. It will eventually appear in a linarith related PR, as Expr.ofNat in Mathlib/Lean/Expr/Basic.lean.