Examples for IJCAR 2016 paper: Congruence Closure in Intensional Type Theory

Remark: all examples can be browsed directly at github.

The two examples from the Applications section are available here:

The following two files use the congruence closure procedure to discharge goals in Group theory and Lists.

The following list contains small files used to test the congruence closure procedure.