cognimeta-utils-0.1.2: Utilities for Cognimeta products (such as perdure). API may change often.

Safe HaskellNone

Cgm.Data.Nat.Base

Documentation

data D0 Source

Instances

class Nat n whereSource

Methods

onNat :: (n ~ D0 => c) -> (forall n'. (Succ n' ~ n, Nat n') => Tagged n' c) -> Tagged n cSource

Instances

Nat D0 
Nat n => Nat (Succ n) 

data Succ n Source

Instances

Typeable1 Succ 
Nat n => Nat (Succ n) 

type family a :+: b Source

addZ :: Nat b => (((D0 :+: b) ~ b, (b :+: D0) ~ b) => c) -> Tagged b cSource

addS :: forall a b z. (Nat a, Nat b) => ((Succ a :+: b) ~ Succ (a :+: b) => z) -> Tagged2 a b zSource

addSC :: forall a b z. (Nat a, Nat b) => (((Succ a :+: b) ~ Succ (a :+: b), Nat (a :+: b)) => z) -> Tagged2 a b zSource

addC :: forall a b z. (Nat a, Nat b) => (Nat (a :+: b) => z) -> Tagged2 a b zSource

addComm :: forall a b z. (Nat a, Nat b) => ((a :+: b) ~ (b :+: a) => z) -> Tagged2 a b zSource

type family a :-: b Source

subZ :: Nat b => ((b :-: D0) ~ b => z) -> Tagged b zSource

subS :: forall a b z. (Nat a, Nat b, Nat (a :-: b)) => ((Succ a :-: b) ~ Succ (a :-: b) => z) -> Tagged2 a b zSource

subI :: Nat b => ((b :-: b) ~ D0 => z) -> Tagged b zSource

addSub :: forall a b c z. (Nat a, Nat b, Nat c, Nat (b :-: c)) => ((((a :+: b) :-: c) ~ (a :+: (b :-: c)), Nat (a :+: (b :-: c))) => z) -> Tagged3 a b c zSource

geTrans :: forall a b c z. (Nat a, Nat b, Nat c, Nat (a :-: b), Nat (b :-: c)) => (Nat (a :-: c) => z) -> Tagged3 a b c zSource