A Num instance for Type

NumType.idr

import Data.Vect

%default total

Num Type where
  (+) = Either
  (*) = Pair
  fromInteger 0 = Void
  fromInteger 1 = Unit
  fromInteger 2 = Bool
  fromInteger n = Vect (fromInteger n) Unit

-- Now you can use arithmetic expressions as type signatures:

a : 1
a = ()

b : 1 * 2
b = ((), True)

c : 0 + 2
c = Right False

me : String * Int
me = ("Leif", 36)

three : 3
three = [(), (), ()]

%default total

peanoType : Nat -> Type
peanoType Z = Void
peanoType (S Z) = Unit
peanoType (S (S Z)) = Bool
peanoType (S (S (S n))) = Maybe $ peanoType (S (S n))

Num Type where
  (+) = Either
  (*) = Pair
  fromInteger n = peanoType $ fromIntegerNat n


-- Now you can use arithmetic expressions as type signatures:

a : 1
a = ()

b : 1 * 2
b = ((), True)

c : 0 + 2
c = Right False

me : String * Int
me = ("Leif", 36)

wierd : 3
wierd = Just False