Documentation

List all possible valuations of an expression (potentially infinite). In pseudo-Haskell:

take 3 $ grounds preludeInstances ((x + x) + y)
  == [(0 + 0) + 0, (0 + 0) + 1, (1 + 1) + 0]

List all possible variable bindings to an expression

take 3 $ groundBinds preludeInstances ((x + x) + y)
  == [ [("x",0),("y",0)]
     , [("x",0),("y",1)]
     , [("x",1),("y",0)] ]

List all possible variable bindings and valuations to an expression

groundAndBinds ti e == zipWith (,) (grounds ti e) (groundBinds ti e)

Are two expressions equal for a given number of tests?

Are two expressions less-than-or-equal for a given number of tests?

Are two expressions less-than for a given number of tests?

Are two expressions inequal for *all* variable assignments? Note this is different than not . equal.

Is a boolean expression true for all variable assignments?

Is an expression ALWAYS false? This is *NOT* the same as not true

Are two expressions equal under a given condition for a given number of tests?

Are two expressions equal under a given condition for a given number of tests and a minimum amount of tests

List variable bindings for which an expression holds true.

Under a maximum number of tests, returns the ratio for which an expression holds true.