kdrag.rewrite.lpo

kdrag.rewrite.lpo(vs: list[ExprRef], t1: ExprRef, t2: ExprRef) → Order

Lexicographic path ordering. Based on https://www21.in.tum.de/~nipkow/TRaAT/programs/termorders.ML TODO add ordering parameter.

Parameters:

• vs (list[ExprRef])

• t1 (ExprRef)

• t2 (ExprRef)

Return type:

Order