Expand description
The Rocq frontend for the portable core.
It reads the vernacular subset the core can represent faithfully:
modules, inductive types, Definition, Fixpoint and measure-based
Function declarations over nat, N, Z, bool and string,
theorems with their tactic structure, and a program
Definition main : list string whose elements are the lines the program
prints. Everything else is rejected with a precise obligation.
Mirrors js/src/translation/rocq.js.
Functionsยง
- parse_
rocq - Reads a Rocq program.