Safe Haskell	None
Language	Haskell2010

Data.Type.Nat.Inequality

Documentation

data NatLT :: N -> N -> * where Source #

Constructors

LTZ :: NatLT Z (S y)
LTS :: !(NatLT x y) -> NatLT (S x) (S y)

Instances

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) :: Constraint) (NatLT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ y) (S y'), Known N Nat x, (Bool ~ lt) True, (Bool ~ eq) False, (Bool ~ gt) False) -> r) -> NatLT x y -> r Source #
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source #
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y))

data NatEQ :: N -> N -> * where Source #

Constructors

EQZ :: NatEQ Z Z
EQS :: !(NatEQ x y) -> NatEQ (S x) (S y)

Instances

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) :: Constraint) (NatEQ x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) y, Known N Nat x, (Bool ~ lt) False, (Bool ~ eq) True, (Bool ~ gt) False) -> r) -> NatEQ x y -> r Source #
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source #
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y))

data NatGT :: N -> N -> * where Source #

Constructors

GTZ :: NatGT (S x) Z
GTS :: !(NatGT x y) -> NatGT (S x) (S y)

Instances

((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source #
Associated Types type WitnessC (ØC :: Constraint) (((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) :: Constraint) (NatGT x y) :: Constraint Source # Methods (\\) :: ØC => (((N ~ x) (S x'), Known N Nat y, (Bool ~ lt) False, (Bool ~ eq) False, (Bool ~ gt) True) -> r) -> NatGT x y -> r Source #
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source #
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x))