Expression to nice looking nat

Stream: new members

[Fox Thomson]

I have an expression that I know is a nat and would like to print out using tactic.trace but when I do using tactic.trace ``(%%g) I get something like as_is (bit1.{0} nat nat.has_one nat.has_add (bit1.{0} nat nat.has_one nat.has_add (has_one.one.{0} nat nat.has_one))). Is there a way to turn this into 7.

[Reid Barton]

I think you want to use docs#expr.to_nat

[Fox Thomson]

Thank you