Library MetaCoq.Common.BasicAst

• • • The context of De Bruijn indices

Library MetaCoq.Common.config

Library MetaCoq.Common.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.Common.Environment

• • Declarations
    • Environments
    • Programs

Library MetaCoq.Common.EnvMap

Library MetaCoq.Common.Kernames

• • Reification of names **

Library MetaCoq.Common.MonadBasicAst

Library MetaCoq.Common.Primitive

Library MetaCoq.Common.Reflect

Library MetaCoq.Common.Transform

Library MetaCoq.Common.uGraph

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

Library MetaCoq.Common.UniversesDec

Library MetaCoq.Common.Universes

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

Library MetaCoq.ErasurePlugin.Erasure

Library MetaCoq.ErasurePlugin.ETransform

Library MetaCoq.ErasurePlugin.Extraction

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

Library MetaCoq.ErasurePlugin.Loader

Library MetaCoq.Erasure.EArities

Library MetaCoq.Erasure.EAstUtils

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.EConstructorsAsBlocks

Library MetaCoq.Erasure.ECSubst

Library MetaCoq.Erasure.EDeps

Library MetaCoq.Erasure.EEnvMap

Library MetaCoq.Erasure.EEtaExpandedFix

Library MetaCoq.Erasure.EEtaExpanded

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.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.EReflect

Library MetaCoq.Erasure.ERemoveParams

Library MetaCoq.Erasure.ESpineView

Library MetaCoq.Erasure.ESubstitution

• • Global Weakening
  • Weakening

Library MetaCoq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd

Library MetaCoq.Erasure.EWcbvEvalCstrsAsBlocksInd

Library MetaCoq.Erasure.EWcbvEvalEtaInd

Library MetaCoq.Erasure.EWcbvEvalInd

Library MetaCoq.Erasure.EWcbvEvalNamed

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

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.EWellformed

Library MetaCoq.Erasure.EWtAst

• Well-scoped and well-formed extracted terms

Library MetaCoq.Erasure.Extract

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
• Universe substitution
  • Entries
    • Constant and axiom entries
    • Inductive entries

Library MetaCoq.PCUIC.PCUICCanonicity

Library MetaCoq.PCUIC.PCUICCasesContexts

Library MetaCoq.PCUIC.PCUICCasesHelper

Library MetaCoq.PCUIC.PCUICClassification

Library MetaCoq.PCUIC.PCUICConfluence

Library MetaCoq.PCUIC.PCUICConsistency

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.PCUICCSubst

• Closed single substitution:

Library MetaCoq.PCUIC.PCUICCumulativitySpec

• Definition of cumulativity and conversion relations

Library MetaCoq.PCUIC.PCUICCumulativity

• Definition of cumulativity and conversion relations
  • Cumulativity

Library MetaCoq.PCUIC.PCUICCumulProp

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.PCUICExpandLetsCorrectness

Library MetaCoq.PCUIC.PCUICExpandLets

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.PCUICMonadAst

Library MetaCoq.PCUIC.PCUICNormalization

Library MetaCoq.PCUIC.PCUICNormal

Library MetaCoq.PCUIC.PCUICParallelReductionConfluence

Library MetaCoq.PCUIC.PCUICParallelReduction

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.PCUICSafeLemmata

Library MetaCoq.PCUIC.PCUICSigmaCalculus

• Theory of σ-calculus operations

Library MetaCoq.PCUIC.PCUICSN

Library MetaCoq.PCUIC.PCUICSpine

Library MetaCoq.PCUIC.PCUICSR

Library MetaCoq.PCUIC.PCUICSubstitution

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

Library MetaCoq.PCUIC.PCUICTelescopes

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.PCUICWeakeningConfigSN

Library MetaCoq.PCUIC.PCUICWeakeningConfig

• Weakening lemmas w.r.t. the checker configuration
  • Constraints

Library MetaCoq.PCUIC.PCUICWeakeningEnvSN

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.Quotation.CommonUtils

Library Extraction

• Extraction setup for the safechecker phase of MetaCoq.

Library Loader

Library SafeTemplateChecker

Library MetaCoq.SafeChecker.Loader

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.PCUICWfEnvImpl

Library MetaCoq.SafeChecker.PCUICWfEnv

Library MetaCoq.SafeChecker.PCUICWfReduction

Library MetaCoq.Template.All

Library MetaCoq.Template.AstUtils

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.Checker

• Coq type-checker for kernel terms

Library MetaCoq.Template.Constants

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.LiftSubst

• Lifting and substitution for the AST

Library MetaCoq.Template.Loader

Library MetaCoq.Template.MonadAst

Library MetaCoq.Template.Normal

Library MetaCoq.Template.Pretty

• Pretty printing

Library MetaCoq.Template.Reduction

Library MetaCoq.Template.ReflectAst

Library MetaCoq.Template.TemplateCheckWf

Library MetaCoq.Template.TemplateEnvMap

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.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.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.TemplatePCUIC.Loader

Library MetaCoq.TemplatePCUIC.PCUICTemplateMonad

Library MetaCoq.TemplatePCUIC.PCUICToTemplateCorrectness

Library MetaCoq.TemplatePCUIC.PCUICToTemplate

Library MetaCoq.TemplatePCUIC.PCUICTransform

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

Library MetaCoq.TemplatePCUIC.TemplateMonadToPCUIC

Library MetaCoq.TemplatePCUIC.TemplateToPCUICCorrectness

Library MetaCoq.TemplatePCUIC.TemplateToPCUICExpanded

Library MetaCoq.TemplatePCUIC.TemplateToPCUIC

Library MetaCoq.TemplatePCUIC.TemplateToPCUICWcbvEval

Library MetaCoq.Utils.All_Forall

Library MetaCoq.Utils.ByteCompare_opt

Library MetaCoq.Utils.ByteCompareSpec

Library MetaCoq.Utils.ByteCompare

Library MetaCoq.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.Utils.LibHypsNaming

• • The custom renaming tactic

Library MetaCoq.Utils.MCArith

Library MetaCoq.Utils.MCCompare

Library MetaCoq.Utils.MCEquality

Library MetaCoq.Utils.MC_ExtrOCamlInt63

Library MetaCoq.Utils.MC_ExtrOCamlNatInt

Library MetaCoq.Utils.MC_ExtrOCamlZPosInt

Library MetaCoq.Utils.MCFSets

Library MetaCoq.Utils.MCList

Library MetaCoq.Utils.MCMSets

Library MetaCoq.Utils.MCOption

Library MetaCoq.Utils.MCPred

Library MetaCoq.Utils.MCPrelude

Library MetaCoq.Utils.MCProd

Library MetaCoq.Utils.MCReflect

• Notion of reflection for Type-based properties

Library MetaCoq.Utils.MCRelations

Library MetaCoq.Utils.MCSquash

Library MetaCoq.Utils.MCString

Library MetaCoq.Utils.MCUtils

Library MetaCoq.Utils.monad_utils

Library MetaCoq.Utils.ReflectEq

Library MetaCoq.Utils.utils

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

Library MetaCoq.Utils.wGraph

• • Main results about acyclicity

Library MetaCoq.Erasure.Typed.Annotations

• More utility functions

Library MetaCoq.Erasure.Typed.CertifyingBeta

Library MetaCoq.Erasure.Typed.CertifyingEta

• Eta-expansion and proof generation

Library MetaCoq.Erasure.Typed.CertifyingInlining

• Inlining pass on the Template Coq representation

Library MetaCoq.Erasure.Typed.Certifying

• Term and proof generation for the certifying transforms

Library MetaCoq.Erasure.Typed.ClosedAux

Library MetaCoq.Erasure.Typed.ErasureCorrectness

Library MetaCoq.Erasure.Typed.Erasure

Library MetaCoq.Erasure.Typed.ExAst

Library MetaCoq.Erasure.Typed.ExtractionCorrectness

Library MetaCoq.Erasure.Typed.Extraction

Library MetaCoq.Erasure.Typed.OptimizeCorrectness

Library MetaCoq.Erasure.Typed.OptimizePropDiscr

Library MetaCoq.Erasure.Typed.Optimize

Library MetaCoq.Erasure.Typed.ResultMonad

Library MetaCoq.Erasure.Typed.Transform

Library MetaCoq.Erasure.Typed.TypeAnnotations

Library MetaCoq.Erasure.Typed.Utils

Library MetaCoq.Erasure.Typed.WcbvEvalAux

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.PCUICWeakeningConfigConv

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.PCUICWeakeningConfigTyp

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.Quotation.ToPCUIC.All

Library MetaCoq.Quotation.ToPCUIC.Equations

Library MetaCoq.Quotation.ToPCUIC.Init

Library MetaCoq.Quotation.ToTemplate.All

Library MetaCoq.Quotation.ToTemplate.Equations

Library MetaCoq.Quotation.ToTemplate.Init

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.TemplatePCUIC.PCUICTemplateMonad.Core

Library MetaCoq.Utils.canonicaltries.CanonicalTries

• The extensional binary tries based on a canonical representation
  • Representation of tries
  • Basic operations: empty, get, set, remove
  • Good variable properties for the basic operations
  • The map_filter collective operation over tries
  • Custom case analysis principles and induction principles
    • A case analysis principle
    • A recursion principle
    • An induction principle
  • The combine collective operation over pairs of tries
  • Extensionality property

Library MetaCoq.Utils.canonicaltries.String2pos

Library MetaCoq.Utils.MCTactics.DestructHead

Library MetaCoq.Utils.MCTactics.DestructHyps

Library MetaCoq.Utils.MCTactics.FindHyp

Library MetaCoq.Utils.MCTactics.GeneralizeOverHoles

Library MetaCoq.Utils.MCTactics.Head

Library MetaCoq.Utils.MCTactics.InHypUnderBindersDo

Library MetaCoq.Utils.MCTactics.SpecializeAllWays

Library MetaCoq.Utils.MCTactics.SpecializeBy

Library MetaCoq.Utils.MCTactics.SpecializeUnderBindersBy

Library MetaCoq.Utils.MCTactics.SplitInContext

Library MetaCoq.Utils.MCTactics.UniquePose

Library MetaCoq.Utils.MCTactics.Zeta1

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.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.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_fun2

Library MetaCoq.Translations.times_bool_fun

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_prelude

Library MetaCoq.Examples.metacoq_tour

Library MetaCoq.Examples.tauto

Library MetaCoq.Examples.typing_correctness