C | |
| Coqbool | |
| Coqbyte | |
| Coqi63 | |
| Coqlist | |
| Coqprod | |
| Coqsum | |
| Coqunit | |
E | |
| Extends | Extend FreeSpec.Exec by associating primitives constructor names to effectful semantics. |
H | |
| Heap | This module provides the means to encode a form of “pointers” in Coq. |
I | |
| Interfaces | |
R | |
| Refs | |
| Resources | |
S | |
| Store |