Agda.TypeChecking.Rewriting.Confluence

Checking confluence of rewrite rules.

Given a rewrite rule f ps ↦ v, we construct critical pairs involving this as the main rule by searching for:

1. *Different* rules f ps' ↦ v' where ps and ps' can be unified@.
2. Subpatterns g qs of ps and rewrite rules g qs' ↦ w where qs and qs' can be unified.

Each of these leads to a *critical pair* v₁ u -- v₂, which should satisfy v₁ = v₂.

Documentation

checkConfluenceOfRules :: [RewriteRule] -> TCM ()

Check confluence of the given clause wrt rewrite rules of the constructors it matches against

Check confluence of the given rewrite rules wrt all other rewrite rules (also amongst themselves).

checkConfluenceOfClause :: QName -> Int -> Clause -> TCM ()