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 |