package coq-elm-extraction

  1. Overview
  2. Doc
Coq extraction to Elm

Install

Dune Dependency

Authors

Maintainers

Sources

v0.1.1.tar.gz
sha512=b6cb0c8c677cc37c8f4f9ae20fc64416db2d9703813e61cd865de16f4839902e53188eb5d3c4bd95de43886b3409b08a5e64fff912a68a75c2d2a2fe62503465

Description

A framework for extracting Coq programs to Elm

Dependencies (8)

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

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover