Module
Data.Typelevel.Num.Ops
- Package
- purescript-typelevel
- Repository
- bodil/purescript-typelevel
#SuccP Source
class SuccP xh xl yh yl yz | xh xl -> yh yl yz, yh yl yz -> xh xlInstances
(Failure (PredecessorOfZeroError x)) => SuccP (Tuple x x) (Tuple x x) D0 D0 TrueSuccP xi D0 xi D1 FalseSuccP xi D1 xi D2 FalseSuccP xi D2 xi D3 FalseSuccP xi D3 xi D4 FalseSuccP xi D4 xi D5 FalseSuccP xi D5 xi D6 FalseSuccP xi D6 xi D7 FalseSuccP xi D7 xi D8 FalseSuccP xi D8 xi D9 False(Succ xi yi) => SuccP xi D9 yi D0 False
#PredecessorOfZeroError Source
data PredecessorOfZeroError t#AddP Source
class (Nat x) <= AddP x y z | x y -> z, z x -> yInstances
(Nat y) => AddP D0 y y(Succ y z) => AddP D1 y z(Succ z z', AddP D1 y z) => AddP D2 y z'(Succ z z', AddP D2 y z) => AddP D3 y z'(Succ z z', AddP D3 y z) => AddP D4 y z'(Succ z z', AddP D4 y z) => AddP D5 y z'(Succ z z', AddP D5 y z) => AddP D6 y z'(Succ z z', AddP D6 y z) => AddP D7 y z'(Succ z z', AddP D7 y z) => AddP D8 y z'(Succ z z', AddP D8 y z) => AddP D9 y z'(Pos (NumCons xi xl), Nat z, AddP xi yi zi, DivMod10 y yi yl, AddP xl (NumCons zi yl) z) => AddP (NumCons xi xl) y z
#Mul Source
class (Nat x, Nat y) <= Mul x y z | x y -> zInstances
(Nat y) => Mul D0 y D0(Nat y) => Mul D1 y y(Add y y z) => Mul D2 y z(Add z y z', Mul D2 y z) => Mul D3 y z'(Add z y z', Mul D3 y z) => Mul D4 y z'(Add z y z', Mul D4 y z) => Mul D5 y z'(Add z y z', Mul D5 y z) => Mul D6 y z'(Add z y z', Mul D6 y z) => Mul D7 y z'(Add z y z', Mul D7 y z) => Mul D8 y z'(Add z y z', Mul D8 y z) => Mul D9 y z'(Pos (NumCons xi xl), Nat y, Mul xi y z, Mul10 z z10, Mul xl y dy, Add dy z10 z') => Mul (NumCons xi xl) y z'
#DivMod10 Source
class (Nat i, Nat x) <= DivMod10 x i l | i l -> x, x -> i lInstances
DivMod10 D0 D0 D0DivMod10 D1 D0 D1DivMod10 D2 D0 D2DivMod10 D3 D0 D3DivMod10 D4 D0 D4DivMod10 D5 D0 D5DivMod10 D6 D0 D6DivMod10 D7 D0 D7DivMod10 D8 D0 D8DivMod10 D9 D0 D9(Nat (NumCons D1 l)) => DivMod10 (NumCons D1 l) D1 l(Nat (NumCons D2 l)) => DivMod10 (NumCons D2 l) D2 l(Nat (NumCons D3 l)) => DivMod10 (NumCons D3 l) D3 l(Nat (NumCons D4 l)) => DivMod10 (NumCons D4 l) D4 l(Nat (NumCons D5 l)) => DivMod10 (NumCons D5 l) D5 l(Nat (NumCons D6 l)) => DivMod10 (NumCons D6 l) D6 l(Nat (NumCons D7 l)) => DivMod10 (NumCons D7 l) D7 l(Nat (NumCons D8 l)) => DivMod10 (NumCons D8 l) D8 l(Nat (NumCons D9 l)) => DivMod10 (NumCons D9 l) D9 l(Nat (NumCons x l), Nat (NumCons (NumCons x l) l')) => DivMod10 (NumCons (NumCons x l) l') (NumCons x l) l'
#LT Source
data LTInstances
(Nat x, Pos y) => DivModP x y D0 x LTShow LTTrich D0 D1 LTTrich D0 D2 LTTrich D0 D3 LTTrich D0 D4 LTTrich D0 D5 LTTrich D0 D6 LTTrich D0 D7 LTTrich D0 D8 LTTrich D0 D9 LT(Pos (NumCons yi yl)) => Trich D0 (NumCons yi yl) LTTrich D1 D2 LTTrich D1 D3 LTTrich D1 D4 LTTrich D1 D5 LTTrich D1 D6 LTTrich D1 D7 LTTrich D1 D8 LTTrich D1 D9 LT(Pos (NumCons yi yl)) => Trich D1 (NumCons yi yl) LTTrich D2 D3 LTTrich D2 D4 LTTrich D2 D5 LTTrich D2 D6 LTTrich D2 D7 LTTrich D2 D8 LTTrich D2 D9 LT(Pos (NumCons yi yl)) => Trich D2 (NumCons yi yl) LTTrich D3 D4 LTTrich D3 D5 LTTrich D3 D6 LTTrich D3 D7 LTTrich D3 D8 LTTrich D3 D9 LT(Pos (NumCons yi yl)) => Trich D3 (NumCons yi yl) LTTrich D4 D5 LTTrich D4 D6 LTTrich D4 D7 LTTrich D4 D8 LTTrich D4 D9 LT(Pos (NumCons yi yl)) => Trich D4 (NumCons yi yl) LTTrich D5 D6 LTTrich D5 D7 LTTrich D5 D8 LTTrich D5 D9 LT(Pos (NumCons yi yl)) => Trich D5 (NumCons yi yl) LTTrich D6 D7 LTTrich D6 D8 LTTrich D6 D9 LT(Pos (NumCons yi yl)) => Trich D6 (NumCons yi yl) LTTrich D7 D8 LTTrich D7 D9 LT(Pos (NumCons yi yl)) => Trich D7 (NumCons yi yl) LTTrich D8 D9 LT(Pos (NumCons yi yl)) => Trich D8 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich D9 (NumCons yi yl) LTCS LT r LTMaxP x y LT y(Nat x, Nat y, GCD y x gcd) => GCDP x y False LT gcd
#GT Source
data GTInstances
(Nat x, Pos y, Sub x y x', Pred q q', DivMod x' y q' r) => DivModP x y q r GTShow GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D0 GTTrich D1 D0 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D1 GTTrich D2 D0 GTTrich D2 D1 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D2 GTTrich D3 D0 GTTrich D3 D1 GTTrich D3 D2 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D3 GTTrich D4 D0 GTTrich D4 D1 GTTrich D4 D2 GTTrich D4 D3 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D4 GTTrich D5 D0 GTTrich D5 D1 GTTrich D5 D2 GTTrich D5 D3 GTTrich D5 D4 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D5 GTTrich D6 D0 GTTrich D6 D1 GTTrich D6 D2 GTTrich D6 D3 GTTrich D6 D4 GTTrich D6 D5 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D6 GTTrich D7 D0 GTTrich D7 D1 GTTrich D7 D2 GTTrich D7 D3 GTTrich D7 D4 GTTrich D7 D5 GTTrich D7 D6 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D7 GTTrich D8 D0 GTTrich D8 D1 GTTrich D8 D2 GTTrich D8 D3 GTTrich D8 D4 GTTrich D8 D5 GTTrich D8 D6 GTTrich D8 D7 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D8 GTTrich D9 D0 GTTrich D9 D1 GTTrich D9 D2 GTTrich D9 D3 GTTrich D9 D4 GTTrich D9 D5 GTTrich D9 D6 GTTrich D9 D7 GTTrich D9 D8 GT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D9 GTCS GT r GTMaxP x y GT x(Nat x, Nat y, Sub x y x', GCD x' y gcd) => GCDP x y False GT gcd
#Trich Source
class (Nat x, Nat y) <= Trich x y r | x y -> rInstances
Trich D0 D0 EQTrich D0 D1 LTTrich D0 D2 LTTrich D0 D3 LTTrich D0 D4 LTTrich D0 D5 LTTrich D0 D6 LTTrich D0 D7 LTTrich D0 D8 LTTrich D0 D9 LT(Pos (NumCons yi yl)) => Trich D0 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D0 GTTrich D1 D0 GTTrich D1 D1 EQTrich D1 D2 LTTrich D1 D3 LTTrich D1 D4 LTTrich D1 D5 LTTrich D1 D6 LTTrich D1 D7 LTTrich D1 D8 LTTrich D1 D9 LT(Pos (NumCons yi yl)) => Trich D1 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D1 GTTrich D2 D0 GTTrich D2 D1 GTTrich D2 D2 EQTrich D2 D3 LTTrich D2 D4 LTTrich D2 D5 LTTrich D2 D6 LTTrich D2 D7 LTTrich D2 D8 LTTrich D2 D9 LT(Pos (NumCons yi yl)) => Trich D2 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D2 GTTrich D3 D0 GTTrich D3 D1 GTTrich D3 D2 GTTrich D3 D3 EQTrich D3 D4 LTTrich D3 D5 LTTrich D3 D6 LTTrich D3 D7 LTTrich D3 D8 LTTrich D3 D9 LT(Pos (NumCons yi yl)) => Trich D3 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D3 GTTrich D4 D0 GTTrich D4 D1 GTTrich D4 D2 GTTrich D4 D3 GTTrich D4 D4 EQTrich D4 D5 LTTrich D4 D6 LTTrich D4 D7 LTTrich D4 D8 LTTrich D4 D9 LT(Pos (NumCons yi yl)) => Trich D4 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D4 GTTrich D5 D0 GTTrich D5 D1 GTTrich D5 D2 GTTrich D5 D3 GTTrich D5 D4 GTTrich D5 D5 EQTrich D5 D6 LTTrich D5 D7 LTTrich D5 D8 LTTrich D5 D9 LT(Pos (NumCons yi yl)) => Trich D5 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D5 GTTrich D6 D0 GTTrich D6 D1 GTTrich D6 D2 GTTrich D6 D3 GTTrich D6 D4 GTTrich D6 D5 GTTrich D6 D6 EQTrich D6 D7 LTTrich D6 D8 LTTrich D6 D9 LT(Pos (NumCons yi yl)) => Trich D6 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D6 GTTrich D7 D0 GTTrich D7 D1 GTTrich D7 D2 GTTrich D7 D3 GTTrich D7 D4 GTTrich D7 D5 GTTrich D7 D6 GTTrich D7 D7 EQTrich D7 D8 LTTrich D7 D9 LT(Pos (NumCons yi yl)) => Trich D7 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D7 GTTrich D8 D0 GTTrich D8 D1 GTTrich D8 D2 GTTrich D8 D3 GTTrich D8 D4 GTTrich D8 D5 GTTrich D8 D6 GTTrich D8 D7 GTTrich D8 D8 EQTrich D8 D9 LT(Pos (NumCons yi yl)) => Trich D8 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D8 GTTrich D9 D0 GTTrich D9 D1 GTTrich D9 D2 GTTrich D9 D3 GTTrich D9 D4 GTTrich D9 D5 GTTrich D9 D6 GTTrich D9 D7 GTTrich D9 D8 GTTrich D9 D9 EQ(Pos (NumCons yi yl)) => Trich D9 (NumCons yi yl) LT(Pos (NumCons yi yl)) => Trich (NumCons yi yl) D9 GT(Pos (NumCons xi xl), Pos (NumCons yi yl), Trich xl yl rl, Trich xi yi ri, CS ri rl r) => Trich (NumCons xi xl) (NumCons yi yl) r