twee-lib-2.1.5: An equational theorem prover
Twee.KBO
Description
An implementation of Knuth-Bendix ordering.
Synopsis
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.