Reduce Nat

Stream: lean4

[Marcus Rossel]

Lean has various operations on Nat which are built into the kernel. Is there some function which reduces an Expr only according to those builtin operations? There's docs#Lean.Meta.reduceNat?, but that has rather strict requirements on the form of the expression. For example, if won't reduce 1 + 1, as that's actually HAdd.hAdd ... instead of Nat.add and OfNat.ofNat ... instead of nat_lit 1.

[Marcus Rossel]

It seems docs#Lean.Meta.evalNat is basically what I was looking for.