twee-lib-2.2: An equational theorem prover

Safe Haskell	None
Language	Haskell2010

Twee.KBO

Description

An implementation of Knuth-Bendix ordering.

Synopsis

lessEq :: Function f => Term f -> Term f -> Bool
lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness

Documentation

lessEq :: Function f => Term f -> Term f -> Bool Source #

Check if one term is less than another in KBO.

lessIn :: Function f => Model f -> Term f -> Term f -> Maybe Strictness Source #

Check if one term is less than another in a given model.