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

Agda.TypeChecking.Rewriting.Confluence

Description

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

Synopsis

# Documentation

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