Description
Integer singletons with flexible representation.
Description
This provides singletons-style witnesses for type-level integers, and some limited arithmetic operations on them. Instead of working with (invisible, implicitly-passed) KnownNat
instances, you can work with (visible, explicitly-mentioned) SNumber
values, and can freely convert between the two forms.
This primarily exists in support of dependent-literals-plugin.