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