Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Documentation
data PeanoNatType t where Source #
ZeroType :: PeanoNatType 'Zero | |
SuccType :: PeanoNatType t -> PeanoNatType ('Succ t) |
Instances
data GreaterEqual a b where Source #
ZeroGreaterEqual :: GreaterEqual a 'Zero | |
SuccGreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) ('Succ b) |
greaterEqualIndex :: GreaterEqual a b -> PeanoNatType b Source #
samePeanoGreaterEqual :: PeanoNatType a -> GreaterEqual a a Source #
diff1GreaterEqual :: GreaterEqual a b -> GreaterEqual ('Succ a) b Source #
peanoGreaterEqual :: PeanoNatType a -> PeanoNatType b -> Maybe (GreaterEqual a b) Source #
addPeanoNatType :: PeanoNatType a -> PeanoNatType b -> PeanoNatType (Add a b) Source #
addZeroPeanoNatTypeEqual :: PeanoNatType a -> Add a 'Zero :~: a Source #
succAddPeanoNatTypeEqual' :: forall a b. PeanoNatType a -> 'Succ (Add a b) :~: Add a ('Succ b) Source #
succAddPeanoNatTypeEqual :: forall a b. PeanoNatType a -> PeanoNatType b -> 'Succ (Add a b) :~: Add a ('Succ b) Source #
addPeanoNatTypeGE :: PeanoNatType a -> PeanoNatType b -> GreaterEqual (Add a b) a Source #
data Greater a b where Source #
MkGreater :: GreaterEqual a b -> Greater ('Succ a) b |
greaterIndex :: Greater a b -> PeanoNatType b Source #
peanoGreater :: PeanoNatType a -> PeanoNatType b -> Maybe (Greater a b) Source #