A package for a more flexible `numLit`

Stream: lean4

[Mac]

I just published a small package called BetterNumLits that provides an alternative macro expansion of numLits . It has type classes for single digits (ex. Zero and One), expands multi-digit literals to array of digit (making it easier to support types that work better with positional notation), and preserves the radix of a literal when pretty printing. Some of its ideas may be of use to the #mathlib4 community based on what I gleaned from the discussions in mathport:numbers.

Regardless, I felt these kinds of tiny metaprogramming package might be something worth sharing on here, so I am doing just that. I also do hope that this kind of self-promotion is okay. If not, my apologies!

[Mac]

I'm sorry, I may be out of touch with some key lingo, but what does the :working_on_it: emoji mean as a reaction?

[Iocta]

mousing over :working_on_it: says "working on it"

[Johan Commelin]

Mac said:

I'm sorry, I may be out of touch with some key lingo, but what does the :working_on_it: emoji mean as a reaction?

Something along the lines of "Great! You're building some useful tools. Thanks for doing this."

[Daniel Fabian]

looks cool ;-)

[Scott Morrison]

The mouse-over says "working on it", but I think historically here it has more been: "you have been working on something and I'm happy/impressed"