package coq-metacoq-translations
Translations built on top of MetaCoq
Install
Dune Dependency
Authors
-
AAbhishek Anand <aa755@cs.cornell.edu>
-
DDanil Annenkov <danil.v.annenkov@gmail.com>
-
SSimon Boulier <simon.boulier@inria.fr>
-
CCyril Cohen <cyril.cohen@inria.fr>
-
YYannick Forster <forster@ps.uni-saarland.de>
-
FFabian Kunze <fkunze@fakusb.de>
-
MMeven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>
-
KKenji Maillard <kenji.maillard@inria.fr>
-
GGregory Malecha <gmalecha@gmail.com>
-
JJakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>
-
MMatthieu Sozeau <matthieu.sozeau@inria.fr>
-
NNicolas Tabareau <nicolas.tabareau@inria.fr>
-
TThéo Winterhalter <theo.winterhalter@inria.fr>
Maintainers
Sources
metacoq-1.1-8.14.tar.gz
sha512=48edab0cfa08c45e2c691d2c01abce1b97a0d15d2d957e90ca8f08dbc0f20d7d8019fb4fb85cf968439cb991f3297e9c2abf0a113a518a2a46fa54814a7d4aea
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: 26 Sep 2022
Dependencies (1)
-
coq-metacoq-template
= version
Dev Dependencies
None
Used by (1)
-
coq-metacoq
= "1.1+8.14"
Conflicts
None
On This Page