Language.Copilot.Libs.Indexes

Queries into how long until properties hold or fail. We use Int16 to return the value, so your queries must not require looking more than 32,767 periods :) . Thus, in the following, the parameter n must be 0 <= n <= 32,767. -1 indicates the test failed.

Documentation

soonest :: Int -> Spec Bool -> Spec Int16

Returns the smallest m <= n such that drop m s is true, and -1 if no such m exists.

soonestFail :: Int -> Spec Bool -> Spec Int16

Returns the smallest m <= n such that drop m s is false, and -1 if no such m exists.

latest :: Int -> Spec Bool -> Spec Int16

Returns the largest m <= n such that drop m s is true, and -1 if no such m exists.

latestFail :: Int -> Spec Bool -> Spec Int16

Returns the largest m <= n such that drop m s is false, and -1 if no such m exists.