Safe Haskell	None
Language	Haskell2010

Data.Type.Nat.Inequality

Documentation

type family x < y :: Bool infix 4 Source

Equations

type family x > y :: Bool infix 4 Source

Equations

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
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)) Source

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
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)) Source

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
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)) Source