3 ms·
With TypeLits, idk if that’s possible without some cheating. But that’s because (as the module name implies) these are type literals and mostly focused on havin
by whateveracct 9y ago
With TypeLits, idk if that’s possible without some cheating. But that’s because (as the module name implies) these are type literals and mostly focused on having Integers that can go from type to term and vice-versa.
I can definitely do that with Singleton peano Nats pretty easily. I’ll end up with a function of type
SNat n -> Maybe (IsEven n)
Where IsEven n is some structural proof of even-ness
data IsEven (n :: Nat) where
ZEven :: IsEven Z
SEven :: forall (n ::Nat). IsEven n -> IsEven (S (S n))
I wrote this on my phone, but I’m sure it’s possible and kinda easy to work with at that.