Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
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