# Pattern matching without K

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

The implementation of our criterion for pattern matching without K 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.
## Authors

Comments and questions are welcome at the following addresses: