package rocq-verified-extraction

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

Install

Dune Dependency

Authors

Maintainers

Sources

v1.0.0-9.1.tar.gz
sha512=65440c1ac351f99c7a0181feaf54614f0699a8ee55035133ed10de22ce8a8df5b3f2a7a216f86b6262ea1aa9940d5322957fe181c94f7d41a69ca3caa746bf5f

Description

Dependencies (6)

  1. malfunction >= "0.7.1"
  2. rocq-metarocq-erasure-plugin >= "1.5.1"
  3. rocq-ceres-bytestring >= "1.0.0"
  4. rocq-stdlib >= "9.0"
  5. rocq-core >= "9.1"
  6. ocaml >= "4.13"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover