Pattern matching without K

This page contains supplementary material for our ICFP 2014 submission titled "Pattern matching without K" (draft).


The current implementation of our criterion for pattern matching is part of the development version of Agda. It is part of Agda as of version 2.4. Installation instructions can be found in the Agda README.

Usage. Open a .agda file in emacs, add the line {-# OPTIONS --without-K #-} at the top, and load it by pressing C-c C-l. All definitions by pattern matching in this file will now be checked for hidden uses of the K axiom (in addition to the regular Agda typechecking).

Examples (Agda files)

The file Examples.agda contains various examples of definitions by pattern matching from the paper that are accepted by our criterion. Meanwhile, the file Fail.agda contains a number of examples that are rejected because they depend (directly or indirectly) on the K axiom.

Side notes to the proof (Agda files)

Some Agda files illustrating (parts of) the proof in our paper can be downloaded here.


Comments and questions are welcome at the following addresses: