[ANN] rocq-typescript-extraction (experimental): Extract Rocq definitions to TypeScript ES modules
An experimental Rocq plugin called rocq-typescript-extraction converts definitions into TypeScript ES modules, generating erasable syntax checked under strict TypeScript settings. It includes benchmarks against handwritten JavaScript and TypeScript and targets Bun or Node with type stripping.
