Crane

Install Crane, configure Rocq, and run your first extraction.

The goals and tradeoffs behind Crane's C++ extraction strategy.

Browse example Rocq projects and extracted C++ code.

Understand all Crane options, extraction rules, and flags.

Our Rocq library of types, monads, etc. used from extracted code.

Planned features and upcoming improvements.