package coq-metacoq-translations

  1. Overview
  2. Homepage

Description

MetaCoq is a meta-programming framework for Coq.

The Translations modules provides implementation of standard translations from type theory to type theory, e.g. parametricity and the cross-bool translation that invalidates functional extensionality.

Published: 28 Jan 2025

Dependencies (1)

  1. coq-metacoq-template = version

Dev Dependencies

None

Used by (1)

  1. coq-metacoq = "1.3.3+8.19"

Conflicts

None

Rocq

Interactive Theorem Prover