Zulip Chat Archive

Stream: Is there code for X?

Topic: int_to_expr


view this post on Zulip Chris Hughes (Dec 11 2020 at 13:02):

Is there a function with this type that makes something a bit nicer. I just want it to always make the string of bit1 $ bit0 $ ... with a potential minus in front.

meta def int.to_expr (n : int) : expr := reflect n

Last updated: May 17 2021 at 15:13 UTC