Term.Builtin.Rules

Builtin rewriting rules.

Rewriting rules

data RRule a

A rewrite rule.

Constructors

RRule a a

Instances

Functor RRule

Applicative RRule

Foldable RRule

Traversable RRule

Eq a => Eq (RRule a)

Ord a => Ord (RRule a)

Show a => Show (RRule a)

Monoid a => Monoid (RRule a)

HasFrees a => HasFrees (RRule a)

dhRules :: Set (RRule LNTerm)

The rewriting rules for Diffie-Hellman. This is a presentation due to Lankford with the finite variant property.

bpRules :: Set (RRule LNTerm)

The rewriting rules for bilinear pairing. These rules extend the the rules for Diffie-Hellman.

msetRules :: Set (RRule LNTerm)

The rewriting rules for multisets.

pairRules :: Set StRule

The rewriting rules for standard subterm operators that are builtin.

symEncRules :: Set StRule

The rewriting rules for standard subterm operators that are builtin.

asymEncRules :: Set StRule

The rewriting rules for standard subterm operators that are builtin.

signatureRules :: Set StRule

The rewriting rules for standard subterm operators that are builtin.

Convenience export

module Term.Builtin.Signature