Hedgehog.Internal.Shrink

Definitions

halvesInteger : Integer -> Colist Integer

Totality: total
Visibility: public export

halves : ToInteger a => a -> Colist a

Totality: total
Visibility: public export

towardsInteger : Integer -> Integer -> Colist Integer

Totality: total
Visibility: public export

towards : ToInteger a => a -> a -> Colist a

  Shrink an integral number by edging towards a destination.
  
  >>> towards 0 100
  [0,50,75,88,94,97,99]
  
  >>> towards 500 1000
  [500,750,875,938,969,985,993,997,999]
  
  >>> towards (-50) (-26)
  [-50,-38,-32,-29,-27]
  
  Note we always try the destination first, as that is the optimal shrink.

Totality: total
Visibility: public export

towardsDouble : Double -> Double -> Colist Double

Totality: total
Visibility: public export

removes : Nat -> List a -> Colist (List a)

Totality: total
Visibility: public export

splits : (a -> b) -> List a -> List (List a, (b, List a))

  All ways a list can be split
  
  Note: The first list in the triple will be in reverse order

Totality: total
Visibility: public export

list : Nat -> List a -> Colist (List a)

  Shrink a list by edging towards the empty list.
  
  >>> list [1,2,3]
  [[],[2,3],[1,3],[1,2]]
  
  >>> list "abcd"
  ["","cd","ab","bcd","acd","abd","abc"]
  
  Note we always try the empty list first, as that is the optimal shrink.

Totality: total
Visibility: public export

interleave : Nat -> List (Cotree a) -> Cotree (List a)

Totality: total
Visibility: public export