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

Language.REST.Internal.MultisetOrder

Description

This module defines a constraint generator for a multiset quasi-ordering. For more details, please see the definition of mul in section 4.2.1 of the paper.

Synopsis

Documentation

multisetOrder :: forall oc base lifted m. (Ord lifted, Ord base, Show base, Eq base, Hashable base, Hashable lifted, Eq lifted, Show (oc base), Eq (oc base), Monad m) => ConstraintGen oc base lifted m -> ConstraintGen oc base (MultiSet lifted) m Source #

Given a constraint generator cgen that generates constraints a WQO on base implied by a relation between elements of lifted, multisetOrder cgen yields a constraint generator on elements of base implied by a relation between multisets of lifted.