Data.Witness.Nat

Documentation

data Zero

Instances

Is Nat Zero

HasListElement Zero (a, r)

data Succ n

Instances

Is Nat n => Is Nat (Succ n)

HasListElement n r => HasListElement (Succ n) (a, r)

data Nat t where

Constructors

ZeroNat :: Nat Zero

SuccNat :: Nat t -> Nat (Succ t)

Instances

SimpleWitness Nat

Representative Nat

Eq1 Nat

Is Nat Zero

Is Nat n => Is Nat (Succ n)