package rocq-verified-extraction

  1. Overview
  2. Homepage
Verified extraction from Rocq to OCaml

Install

Dune Dependency

Authors

Maintainers

Sources

rocq-verified-extraction-0.9.3-9.0.tar.gz
sha512=4b1ebcf5fb939b1506b265e4f224b16c20f312e13974222c2ebe20fefaee554324660fecdd2a96f05ac326705fc9c6f022effdb97d1eaa1a6896001cf92ce9b5

Description

Published: 24 Apr 2025

Dependencies (6)

  1. malfunction >= "0.7"
  2. rocq-metarocq-erasure-plugin = "1.4+9.0"
  3. coq-ceres >= "0.4.1"
  4. rocq-stdlib >= "9.0"
  5. rocq-core >= "9.0"
  6. ocaml >= "4.13"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover