Zulip Chat Archive

Stream: new members

Topic: Expression to nice looking nat


view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 06 2020 at 14:30):

I think you want to use docs#expr.to_nat

view this post on Zulip Fox Thomson (Sep 06 2020 at 15:38):

Thank you


Last updated: May 14 2021 at 02:15 UTC