package coq-freespec-exec

  1. Overview
  2. No Docs
A framework for implementing and certifying impure computations in Coq

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. T
    Thomas Letan
  2. Y
    Yann Régis-Gianas

Maintainers

  1. T
    Thomas Letan <lthms@soap.coffee>

Sources

freespec.0.3.tar.gz
sha512=a4321066ef6267fc87a27b7b4ce7bd75db9878dcf33f7463ee3d11bdedb6a13f30008f7c20ca972c18e7d6f3bf8b0857409caf7fad60ecbd186e83b45fa1b7a1

Description

FreeSpec is a framework for the Coq proof assistant which allows to implement and specify impure computations. This is the “exec” plugin, which allows from executing impure computations from with Coq thanks to a dedicated vernacular command.

Tags

date:2021-03-01 keyword:plugin category:Miscellaneous/Coq Extensions logpath:FreeSpec.Exec

Published: 04 Mar 2021

Dependencies (5)

  1. coq-freespec-ffi = "0.3"
  2. coq-freespec-core = "0.3"
  3. coq >= "8.12" & < "8.14~"
  4. dune >= "2.5"
  5. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None