## Stream: new members

### Topic: Expression to nice looking nat

#### Fox Thomson (Sep 06 2020 at 14:05):

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 (Sep 06 2020 at 14:30):

I think you want to use docs#expr.to_nat

#### Fox Thomson (Sep 06 2020 at 15:38):

Thank you

Last updated: May 14 2021 at 02:15 UTC