package coq-rust-extraction

  1. Overview
  2. Doc
Coq extraction to Rust

Install

Dune Dependency

Authors

Maintainers

Sources

v0.1.1.tar.gz
sha512=b78b7dfe69ecec76b8a9885affe6322c6854d346bcdea827e176593db57712fd54632aef902b745354b4803d7b1918ca33ae49d424b58caea9751f298433bff7

Description

A framework for extracting Coq programs to Rust

Dependencies (8)

  1. coq-metacoq-erasure >= "1.3.2" & < "1.4~"
  2. coq-metacoq-safechecker >= "1.3.2" & < "1.4~"
  3. coq-metacoq-pcuic >= "1.3.2" & < "1.4~"
  4. coq-metacoq-template-pcuic >= "1.3.2" & < "1.4~"
  5. coq-metacoq-template >= "1.3.2" & < "1.4~"
  6. coq-metacoq-common >= "1.3.2" & < "1.4~"
  7. coq-metacoq-utils >= "1.3.2" & < "1.4~"
  8. coq >= "8.20" & < "9.1~"

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover