package coq-metacoq-safechecker

  1. Overview
  2. Homepage

Description

MetaCoq is a meta-programming framework for Coq.

The SafeChecker modules provides a correct implementation of weak-head reduction, conversion and typechecking of Coq definitions and global environments.

Published: 27 Jan 2021

Dependencies (4)

  1. coq-metacoq-pcuic = version
  2. coq-metacoq-template = version
  3. coq >= "8.12~" & < "8.13~"
  4. ocaml >= "4.07.1" & < "4.10~"

Dev Dependencies

None

Used by (2)

  1. coq-metacoq = "1.0~beta2+8.12"
  2. coq-metacoq-erasure = "1.0~beta2+8.12"

Conflicts

None

Rocq

Interactive Theorem Prover