term-rewriting-0.3.0.1: Term Rewriting Library

Safe HaskellNone
LanguageHaskell98

Data.Rewriting.CriticalPair.Type

Synopsis

Documentation

data CP f v v' Source #

A critical pair. Critical pairs (should) have the following properties:

top   == Context.ofTerm top pos (Term.map Left id (Rule.lhs leftRule))
left  == Context.ofTerm top pos (Term.map Left id (Rule.rhs leftRule))
top   == Substitution.apply subst (Term.map Right id (Rule.lhs rightRule))
right == Substitution.apply subst (Term.map Right id (Rule.rhs rightRule))

Furthermore, pos is a non-variable position of (lhs rightRule) and subst is a most general substitution with these properties.

Constructors

CP 

Fields