rest-rewrite-0.4.1: Rewriting library with online termination checking
Safe HaskellSafe-Inferred
LanguageHaskell2010

Language.REST.OCToAbstract

Synopsis

Documentation

lift :: forall impl base lifted m. (ToSMTVar base Int, Ord base, Eq base, Hashable base, Show lifted, Show base, Show (impl base)) => WQOConstraints impl m -> ConstraintGen impl base lifted Identity -> OCAlgebra (impl base) lifted m Source #

lift takes a representation of constraints on a WQO over base, alongside a function used to generate constraints to permit a relation on terms lifted, and returns the corresponding Ordering Constraints Algebra