Main.purs

module Main where

import Data.Typelevel.Num (class LtEq, class Mod, class Pos, type (:*), D0, D2, D5, D6, D8, d8)

type D256 = D2 :* D5 :* D6

testPositive :: ∀ a . Pos a => a -> Boolean
testPositive _ = true

testLtEq256 :: ∀ a . LtEq a D256 => a -> Boolean
testLtEq256 _ = true

testMod8remainder0 :: ∀ a . Mod a D8 D0 => a -> Boolean
testMod8remainder0 _ = true



proove8isPositive :: Boolean
proove8isPositive = testPositive d8

proove8isLtEq256 :: Boolean
proove8isLtEq256 = testLtEq256 d8

proove8Mod8remainder0Ok :: Boolean
proove8Mod8remainder0Ok = testMod8remainder0 d8

class (Pos m, LtEq m D256, Mod m D8 D0) <= IsPowerOf2 m

instance isPowerOf2TypeLevel :: IsPowerOf2 D8

{-

Error found:
in module Main
at src/Main.purs line 29, column 1 - line 29, column 44

  No type class instance was found for

    Data.Typelevel.Num.Sets.Pos t0

  The instance head contains unknown type variables. Consider adding a type annotation.

while checking that expression #dict LtEq
  has type {}
in value declaration isPowerOf2TypeLevel

where t0 is an unknown type

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

-}