Zulip Chat Archive

Stream: Is there code for X?

Topic: int_to_expr


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: Dec 20 2023 at 11:08 UTC