This page has moved to http://adam.chlipala.net/itp/lib.html.

You'll be redirectly automatically after two seconds.

Code library for Interactive Computer Theorem Proving class

This page lightly documents a Coq library meant to be built collaboratively by people involved with CS294-9. You can download the latest tarball.

Tactics Useful tactics
Nonterm Support for defining and reasoning about nonterminating programs
Esets The finite set ADT and implementations
Emaps The finite map ADT and implementations