Zulip Chat Archive

Stream: lean4

Topic: expr.of_nat


Scott Morrison (Oct 06 2022 at 04:57):

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 (Oct 06 2022 at 05:00):

This requires type class synthesis. I would do

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

Gabriel Ebner (Oct 06 2022 at 05:00):

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

Scott Morrison (Oct 06 2022 at 06:15):

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


Last updated: Dec 20 2023 at 11:08 UTC