Hedgehog.Internal.Util

Definitions

interface SafeDiv : (a : Type) -> (a -> Type) -> Type

  Interface providing a safe (total) division operation
  by proving that the divisor is non-zero.

Parameters: a, pred
Constraints: Neg a
Methods:

safeDiv' : a -> (d : a) -> (0 _ : pred d) -> a

Implementations:

SafeDiv Int (\d => d == 0 = False)

SafeDiv Integer (\d => d == 0 = False)

SafeDiv Double (\d => d == 0 = False)

safeDiv' : SafeDiv a pred => a -> (d : a) -> (0 _ : pred d) -> a

Totality: total
Visibility: public export

safeDiv : SafeDiv a pred => a -> (d : a) -> {auto 0 _ : pred d} -> a

Totality: total
Visibility: public export

fromPred : (a -> Bool) -> a -> Maybe a

Totality: total
Visibility: public export

interface ToInteger : Type -> Type

Parameters: a
Constraints: Num a
Methods:

toInteger : a -> Integer

toNat : a -> Nat

Implementations:

ToInteger Size

ToInteger Integer

ToInteger Int8

ToInteger Int16

ToInteger Int32

ToInteger Int64

ToInteger Int

ToInteger Bits8

ToInteger Bits16

ToInteger Bits32

ToInteger Bits64

ToInteger Nat

ToInteger Double

toInteger : ToInteger a => a -> Integer

Totality: total
Visibility: public export

toNat : ToInteger a => a -> Nat

Totality: total
Visibility: public export

fromIntegral : ToInteger a => Num b => a -> b

Totality: total
Visibility: public export

round : Num a => Double -> a

Totality: total
Visibility: public export

iterateBefore : (a -> Bool) -> (a -> a) -> a -> Colist a

Totality: total
Visibility: public export

iterateBefore0 : Eq a => Num a => (a -> a) -> a -> Colist a

Totality: total
Visibility: public export

prepRev : List a -> List a -> List a

  Prepends the first list in reverse order to the
  second list.

Totality: total
Visibility: public export

signum : Ord a => Neg a => a -> a

Totality: total
Visibility: public export

consNub : Eq a => a -> Colist a -> Colist a

  Cons an element on to the front of a list unless it is already there.

Totality: total
Visibility: public export

concatColist : Colist (Colist a) -> Colist a

Totality: total
Visibility: public export

concatMapColist : (a -> Colist b) -> Colist a -> Colist b

Totality: total
Visibility: public export

fromFoldable : Foldable f => f a -> Colist a

Totality: total
Visibility: public export