Agda-2.6.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone



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₂.



checkConfluenceOfRules :: [RewriteRule] -> TCM () Source #

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).