Library MetaCoq.Erasure.EArities

Library MetaCoq.Erasure.EAst

• Extracted terms
  • Entries
    • Constant and axiom entries
    • Inductive entries
  • Declarations
    • The context of De Bruijn indices
    • Environments
    • Programs

Library MetaCoq.Erasure.EAstUtils

Library MetaCoq.Erasure.ECSubst

Library MetaCoq.Erasure.EConstructorsAsBlocks

Library MetaCoq.Erasure.EDeps

Library MetaCoq.Erasure.EEnvMap

Library MetaCoq.Erasure.EEtaExpanded

Library MetaCoq.Erasure.EEtaExpandedFix

Library MetaCoq.Erasure.EExtends

Library MetaCoq.Erasure.EGenericMapEnv

Library MetaCoq.Erasure.EGlobalEnv

• Global environments
  • Environment lookup
  • Reduction
    • Helper functions for reduction

Library MetaCoq.Erasure.EInduction

• Deriving a compact induction principle for terms

Library MetaCoq.Erasure.EInlineProjections

Library MetaCoq.Erasure.ELiftSubst

• Lifting and substitution for the AST

Library MetaCoq.Erasure.EOptimizePropDiscr

Library MetaCoq.Erasure.EPretty

• Pretty printing

Library MetaCoq.Erasure.EProgram

Library MetaCoq.Erasure.EReflect

Library MetaCoq.Erasure.ERemoveParams

Library MetaCoq.Erasure.ESpineView

Library MetaCoq.Erasure.ESubstitution

• • Global Weakening
  • Weakening

Library MetaCoq.Erasure.ETransform

Library MetaCoq.Erasure.EWcbvEval

• Weak-head call-by-value evaluation strategy.
  • Big step version of weak cbv beta-zeta-iota-fix-delta reduction.

Library MetaCoq.Erasure.EWcbvEvalEtaInd

Library MetaCoq.Erasure.EWcbvEvalInd

Library MetaCoq.Erasure.EWellformed

Library MetaCoq.Erasure.EWtAst

• Well-scoped and well-formed extracted terms

Library MetaCoq.Erasure.Erasure

Library MetaCoq.Erasure.ErasureCorrectness

• Correctness of erasure
  • The correctness proof

Library MetaCoq.Erasure.ErasureFunction

Library MetaCoq.Erasure.ErasureProperties

• • Erasure and applications
  • Preliminaries on arities and proofs
    • Erasure is stable under context conversion
  • isErasable is stable under universe instantiation
  • Erasure is stable under instantiation of universes

Library MetaCoq.Erasure.Extract

Library MetaCoq.Erasure.Extraction

• Extraction setup for the erasure phase of template-coq.

Library MetaCoq.Erasure.Loader

Library MetaCoq.Erasure.Prelim

• • on mkApps
  • Prelim on fixpoints
  • Prelim on typing

Library MetaCoq.PCUIC.Extraction

• Extraction setup for the pcuic phase of MetaCoq.

Library MetaCoq.PCUIC.PCUICAlpha

Library MetaCoq.PCUIC.PCUICArities

Library MetaCoq.PCUIC.PCUICAst

• AST of the Polymorphic Cumulative Calculus of Inductive Constructions
  • Entries
    • Constant and axiom entries
    • Inductive entries
• Universe substitution

Library MetaCoq.PCUIC.PCUICCSubst

• Closed single substitution:

Library MetaCoq.PCUIC.PCUICCanonicity

Library MetaCoq.PCUIC.PCUICCasesContexts

Library MetaCoq.PCUIC.PCUICConfluence

Library MetaCoq.PCUIC.PCUICContextConversion

Library MetaCoq.PCUIC.PCUICContextReduction

Library MetaCoq.PCUIC.PCUICContextSubst

• Substitution lemmas for typing derivations.

Library MetaCoq.PCUIC.PCUICContexts

Library MetaCoq.PCUIC.PCUICConvCumInversion

Library MetaCoq.PCUIC.PCUICConversion

Library MetaCoq.PCUIC.PCUICCumulProp

Library MetaCoq.PCUIC.PCUICCumulativity

• Definition of cumulativity and conversion relations
  • Cumulativity

Library MetaCoq.PCUIC.PCUICCumulativitySpec

• Definition of cumulativity and conversion relations

Library MetaCoq.PCUIC.PCUICElimination

Library MetaCoq.PCUIC.PCUICEquality

• • Syntactic ws_cumul_pb up-to universes
  • Behavior on mkApps and it_mkLambda_or_LetIn **
  • Syntactic ws_cumul_pb up to printing anotations **
  • ws_cumul_pb on contexts **

Library MetaCoq.PCUIC.PCUICEtaExpand

Library MetaCoq.PCUIC.PCUICExpandLets

Library MetaCoq.PCUIC.PCUICExpandLetsCorrectness

Library MetaCoq.PCUIC.PCUICFirstorder

Library MetaCoq.PCUIC.PCUICGeneration

Library MetaCoq.PCUIC.PCUICGlobalEnv

Library MetaCoq.PCUIC.PCUICGuardCondition

Library MetaCoq.PCUIC.PCUICInductiveInversion

Library MetaCoq.PCUIC.PCUICInductives

• Projections

Library MetaCoq.PCUIC.PCUICInversion

Library MetaCoq.PCUIC.PCUICLoader

Library MetaCoq.PCUIC.PCUICNormal

Library MetaCoq.PCUIC.PCUICParallelReduction

Library MetaCoq.PCUIC.PCUICParallelReductionConfluence

Library MetaCoq.PCUIC.PCUICPrincipality

Library MetaCoq.PCUIC.PCUICProgram

• Definition of programs in template-coq, well-typed terms and provided transformations

Library MetaCoq.PCUIC.PCUICProgress

Library MetaCoq.PCUIC.PCUICRedTypeIrrelevance

Library MetaCoq.PCUIC.PCUICReduction

Library MetaCoq.PCUIC.PCUICSN

Library MetaCoq.PCUIC.PCUICSR

Library MetaCoq.PCUIC.PCUICSafeLemmata

Library MetaCoq.PCUIC.PCUICSigmaCalculus

• Theory of σ-calculus operations

Library MetaCoq.PCUIC.PCUICSpine

Library MetaCoq.PCUIC.PCUICSubstitution

• Substitution lemmas for typing derivations. Substitution is now derived from a general

Library MetaCoq.PCUIC.PCUICTelescopes

Library MetaCoq.PCUIC.PCUICToTemplate

Library MetaCoq.PCUIC.PCUICToTemplateCorrectness

Library MetaCoq.PCUIC.PCUICTransform

• Definition of programs in template-coq, well-typed terms and provided transformations
• Translation from Template to PCUIC, directly preserves evaluation

Library MetaCoq.PCUIC.PCUICTypedAst

Library MetaCoq.PCUIC.PCUICTyping

• Typing derivations
  • Typing relation
  • Typechecking of global environments
    • An induction principle ensuring the Σ declarations enjoy the same properties.
• Lemmas about All_local_env

Library MetaCoq.PCUIC.PCUICUnivLevels

Library MetaCoq.PCUIC.PCUICValidity

Library MetaCoq.PCUIC.PCUICWcbvEval

• Weak-head call-by-value evaluation strategy.
  • Big step version of weak cbv beta-zeta-iota-fix-delta reduction.

Library MetaCoq.PCUIC.PCUICWeakeningEnv

• Weakening lemmas w.r.t. the global environment
  • Constraints
  • Lookup
  • Back to universes

Library MetaCoq.PCUIC.PCUICWellScopedCumulativity

Library MetaCoq.PCUIC.PCUICWfCases

Library MetaCoq.PCUIC.PCUICWfUniverses

Library MetaCoq.PCUIC.PCUICWtCumulativity

Library MetaCoq.PCUIC.TemplateToPCUIC

Library MetaCoq.PCUIC.TemplateToPCUICCorrectness

Library MetaCoq.PCUIC.TemplateToPCUICExpanded

Library MetaCoq.PCUIC.TemplateToPCUICWcbvEval

Library MetaCoq.SafeChecker.Extraction

• Extraction setup for the safechecker phase of MetaCoq.

Library MetaCoq.SafeChecker.Loader

Library MetaCoq.SafeChecker.PCUICConsistency

Library MetaCoq.SafeChecker.PCUICEqualityDec

• • Boolean of equality **

Library MetaCoq.SafeChecker.PCUICErrors

Library MetaCoq.SafeChecker.PCUICRetypingEnvIrrelevance

Library MetaCoq.SafeChecker.PCUICSafeChecker

Library MetaCoq.SafeChecker.PCUICSafeConversion

• Conversion for PCUIC without fuel

Library MetaCoq.SafeChecker.PCUICSafeReduce

• Reduction machine for PCUIC without fuel

Library MetaCoq.SafeChecker.PCUICSafeRetyping

• Retyping

Library MetaCoq.SafeChecker.PCUICTypeChecker

Library MetaCoq.SafeChecker.PCUICWfEnv

Library MetaCoq.SafeChecker.PCUICWfEnvImpl

Library MetaCoq.SafeChecker.PCUICWfReduction

Library MetaCoq.SafeChecker.SafeTemplateChecker

Library MetaCoq.Template.All

Library MetaCoq.Template.Ast

• AST of Coq kernel terms and kernel data structures
  • Basic data-types:
  • Terms:
  • Kernel interface: entries and declarations
  • Environments of declarations
  • Entries
    • Constant and axiom entries
    • Inductive entries

Library MetaCoq.Template.AstUtils

Library MetaCoq.Template.BasicAst

• • • The context of De Bruijn indices

Library MetaCoq.Template.Checker

• Coq type-checker for kernel terms

Library MetaCoq.Template.Constants

Library MetaCoq.Template.EnvMap

Library MetaCoq.Template.Environment

• • Declarations
    • Environments
    • Programs

Library MetaCoq.Template.EnvironmentTyping

• • Environment lookup
    • Typing of inductive declarations
    • Typing of constant declarations
    • Typing of global environment
    • Typing of local environments
  • Induction principle for typing up-to a global environment

Library MetaCoq.Template.EtaExpand

• Eta-expansion and proof generation

Library MetaCoq.Template.ExtractableLoader

Library MetaCoq.Template.Extraction

• Extraction setup for template-coq.

Library MetaCoq.Template.Induction

• Deriving a compact induction principle for terms

Library MetaCoq.Template.Kernames

• • Reification of names **

Library MetaCoq.Template.LiftSubst

• Lifting and substitution for the AST

Library MetaCoq.Template.Loader

Library MetaCoq.Template.Normal

Library MetaCoq.Template.Pretty

• Pretty printing

Library MetaCoq.Template.Reduction

Library MetaCoq.Template.Reflect

Library MetaCoq.Template.ReflectAst

Library MetaCoq.Template.TemplateCheckWf

Library MetaCoq.Template.TemplateMonad

Library MetaCoq.Template.TemplateProgram

• Definition of programs in template-coq, well-typed terms and provided transformations

Library MetaCoq.Template.TermEquality

• • Syntactic equality up-to universes

Library MetaCoq.Template.Transform

Library MetaCoq.Template.Typing

• Typing derivations
  • Reduction
    • Helper functions for reduction
    • One step strong beta-zeta-iota-fix-delta reduction
    • Reduction
  • Term equality and cumulativity
  • Cumulativity:
    • Conversion
  • Typing relation
  • Typechecking of global environments
    • An induction principle ensuring the Σ declarations enjoy the same properties.
• Lemmas about All_local_env

Library MetaCoq.Template.TypingWf

• Well-formedness of terms and types in typing derivations

Library MetaCoq.Template.UnivSubst

• Universe substitution

Library MetaCoq.Template.Universes

• Valuations
  • • • Lemmas about eq and leq ****
• Universe substitution

Library MetaCoq.Template.WcbvEval

• Weak-head call-by-value evaluation strategy.
  • Big step version of weak cbv beta-zeta-iota-fix-delta reduction.

Library MetaCoq.Template.WfAst

• Well-formedness of terms and types in typing derivations
• Inversion lemmas for the well-formedness judgement

Library MetaCoq.Template.config

Library MetaCoq.Template.monad_utils

Library MetaCoq.Template.utils

• • This file exports utilities and notations used in MetaCoq.

Library MetaCoq.PCUIC.Bidirectional.BDFromPCUIC

Library MetaCoq.PCUIC.Bidirectional.BDStrengthening

Library MetaCoq.PCUIC.Bidirectional.BDToPCUIC

Library MetaCoq.PCUIC.Bidirectional.BDTyping

Library MetaCoq.PCUIC.Bidirectional.BDUnique

Library MetaCoq.PCUIC.Conversion.PCUICClosedConv

Library MetaCoq.PCUIC.Conversion.PCUICInstConv

• Type preservation for σ-calculus instantiation

Library MetaCoq.PCUIC.Conversion.PCUICNamelessConv

Library MetaCoq.PCUIC.Conversion.PCUICOnFreeVarsConv

Library MetaCoq.PCUIC.Conversion.PCUICRenameConv

• Type preservation for σ-calculus operations

Library MetaCoq.PCUIC.Conversion.PCUICUnivSubstitutionConv

• Universe Substitution lemmas for typing derivations.

Library MetaCoq.PCUIC.Conversion.PCUICWeakeningConv

• Weakening lemmas for typing derivations.

Library MetaCoq.PCUIC.Conversion.PCUICWeakeningEnvConv

Library MetaCoq.PCUIC.Syntax.PCUICCases

• Functions related to the "compact" case representation
  • • Helper functions for reduction/conversion

Library MetaCoq.PCUIC.Syntax.PCUICClosed

• Lemmas about the closedn predicate

Library MetaCoq.PCUIC.Syntax.PCUICDepth

Library MetaCoq.PCUIC.Syntax.PCUICInduction

• Deriving a compact induction principle for terms

Library MetaCoq.PCUIC.Syntax.PCUICInstDef

• Type preservation for σ-calculus instantiation

Library MetaCoq.PCUIC.Syntax.PCUICLiftSubst

• Commutation lemmas for the lifting and substitution operations.

Library MetaCoq.PCUIC.Syntax.PCUICNamelessDef

Library MetaCoq.PCUIC.Syntax.PCUICOnFreeVars

• Preservation of free variables

Library MetaCoq.PCUIC.Syntax.PCUICPosition

Library MetaCoq.PCUIC.Syntax.PCUICReflect

Library MetaCoq.PCUIC.Syntax.PCUICRenameDef

• Type preservation for σ-calculus operations

Library MetaCoq.PCUIC.Syntax.PCUICTactics

Library MetaCoq.PCUIC.Syntax.PCUICUnivSubst

Library MetaCoq.PCUIC.Syntax.PCUICViews

Library MetaCoq.PCUIC.Typing.PCUICClosedTyp

Library MetaCoq.PCUIC.Typing.PCUICContextConversionTyp

Library MetaCoq.PCUIC.Typing.PCUICInstTyp

• Type preservation for σ-calculus instantiation

Library MetaCoq.PCUIC.Typing.PCUICNamelessTyp

Library MetaCoq.PCUIC.Typing.PCUICRenameTyp

• Type preservation for σ-calculus operations

Library MetaCoq.PCUIC.Typing.PCUICUnivSubstitutionTyp

• Universe Substitution lemmas for typing derivations.

Library MetaCoq.PCUIC.Typing.PCUICWeakeningEnvTyp

Library MetaCoq.PCUIC.Typing.PCUICWeakeningTyp

• Weakening lemmas for typing derivations.

Library MetaCoq.PCUIC.utils.PCUICAstUtils

Library MetaCoq.PCUIC.utils.PCUICOnOne

• • Reduction
    • One step strong beta-zeta-iota-fix-delta reduction

Library MetaCoq.PCUIC.utils.PCUICPretty

• Pretty printing

Library MetaCoq.PCUIC.utils.PCUICPrimitive

Library MetaCoq.PCUIC.utils.PCUICSize

Library MetaCoq.PCUIC.utils.PCUICUtils

Library MetaCoq.Template.TemplateMonad.Common

Library MetaCoq.Template.TemplateMonad.Core

• The Template Monad
  • • The TemplateMonad type

Library MetaCoq.Template.TemplateMonad.Extractable

• The Extractable Template Monad

Library MetaCoq.Template.common.uGraph

• • Check of consistency **
  • Check of leq **

Library MetaCoq.Template.utils.All_Forall

Library MetaCoq.Template.utils.ByteCompare

Library MetaCoq.Template.utils.ByteCompareSpec

Library MetaCoq.Template.utils.ByteCompare_opt

Library MetaCoq.Template.utils.LibHypsNaming

• • The custom renaming tactic

Library MetaCoq.Template.utils.MCArith

Library MetaCoq.Template.utils.MCCompare

Library MetaCoq.Template.utils.MCEquality

Library MetaCoq.Template.utils.MCList

Library MetaCoq.Template.utils.MCOption

Library MetaCoq.Template.utils.MCPred

Library MetaCoq.Template.utils.MCPrelude

Library MetaCoq.Template.utils.MCProd

Library MetaCoq.Template.utils.MCReflect

• Notion of reflection for Type-based properties

Library MetaCoq.Template.utils.MCRelations

Library MetaCoq.Template.utils.MCSquash

Library MetaCoq.Template.utils.MCString

Library MetaCoq.Template.utils.MCUtils

Library MetaCoq.Template.utils.MC_ExtrOCamlInt63

Library MetaCoq.Template.utils.MC_ExtrOCamlNatInt

Library MetaCoq.Template.utils.MC_ExtrOCamlZPosInt

Library MetaCoq.Template.utils.ReflectEq

Library MetaCoq.Template.utils.bytestring

• Copyright (C) 2020 BedRock Systems, Inc.
• All rights reserved.
• SPDX-License-Identifier: LGPL-2.1 WITH BedRock Exception for use over network,
• see repository root for details.
  • • Substrings

Library MetaCoq.Template.utils.wGraph

• • Main results about acyclicity

Library MetaCoq.Translations.MiniHoTT

• • Path operations are equivalences
    • Dependent paths
  • Universal mapping property
  • Paths
  • Path algebra
  • Transport
  • Maps on paths
  • Dependent paths
  • Functorial action
  • Equivalences
  • Truncatedness: any dependent product of n-types is an n-type
  • Contractibility: A product over a contractible type is equivalent to the fiber over the center.
  • Symmetry of curried arguments
  • Unpacking
  • Eta conversion
  • Paths
  • Transport
  • Functorial action
  • Equivalences
  • Associativity

Library MetaCoq.Translations.MiniHoTT_paths

• • Path operations are equivalences
    • Dependent paths
  • Universal mapping property
  • Paths
  • Path algebra
  • Transport
  • Maps on paths
  • Dependent paths
  • Functorial action
  • Equivalences
  • Truncatedness: any dependent product of n-types is an n-type
  • Contractibility: A product over a contractible type is equivalent to the fiber over the center.
  • Symmetry of curried arguments
  • Unpacking
  • Eta conversion
  • Paths
  • Transport
  • Functorial action
  • Equivalences
  • Associativity

Library MetaCoq.Translations.param_binary

Library MetaCoq.Translations.param_cheap_packed

Library MetaCoq.Translations.param_generous_packed

Library MetaCoq.Translations.param_generous_unpacked

Library MetaCoq.Translations.param_original

Library MetaCoq.Translations.sigma

Library MetaCoq.Translations.standard_model

• ****************** WARNING : WIP ! ****************** *

Library MetaCoq.Translations.times_bool_fun

Library MetaCoq.Translations.times_bool_fun2

Library MetaCoq.Translations.translation_utils

Library MetaCoq.Examples.add_constructor

• • Auxiliary functions
• Plugin
• Examples

Library MetaCoq.Examples.constructor_tac

Library MetaCoq.Examples.demo

Library MetaCoq.Examples.metacoq_tour

Library MetaCoq.Examples.metacoq_tour_prelude

Library MetaCoq.Examples.tauto

Library MetaCoq.Examples.typing_correctness