Library MetaRocq.Common.BasicAst

• • • The context of De Bruijn indices

Library MetaRocq.Common.EnvMap

Library MetaRocq.Common.Environment

• • Declarations
    • Environments
    • Programs

Library MetaRocq.Common.EnvironmentReflect

Library MetaRocq.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 MetaRocq.Common.Kernames

• • Reification of names **

Library MetaRocq.Common.MonadBasicAst

Library MetaRocq.Common.Primitive

Library MetaRocq.Common.Reflect

Library MetaRocq.Common.Transform

Library MetaRocq.Common.Universes

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

Library MetaRocq.Common.UniversesDec

Library MetaRocq.Common.config

Library MetaRocq.Common.uGraph

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

Library MetaRocq.ErasurePlugin.ETransform

Library MetaRocq.ErasurePlugin.Erasure

Library MetaRocq.ErasurePlugin.ErasureCorrectness

Library MetaRocq.ErasurePlugin.Extraction

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

Library MetaRocq.ErasurePlugin.Loader

Library MetaRocq.Erasure.EArities

Library MetaRocq.Erasure.EAst

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

Library MetaRocq.Erasure.EAstUtils

Library MetaRocq.Erasure.EBeta

Library MetaRocq.Erasure.ECSubst

Library MetaRocq.Erasure.ECoInductiveToInductive

Library MetaRocq.Erasure.EConstructorsAsBlocks

Library MetaRocq.Erasure.EDeps

Library MetaRocq.Erasure.EEnvMap

Library MetaRocq.Erasure.EEtaExpanded

Library MetaRocq.Erasure.EEtaExpandedFix

Library MetaRocq.Erasure.EExtends

Library MetaRocq.Erasure.EGenericGlobalMap

Library MetaRocq.Erasure.EGenericMapEnv

Library MetaRocq.Erasure.EGlobalEnv

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

Library MetaRocq.Erasure.EGlobalFragment

Library MetaRocq.Erasure.EImplementBox

Library MetaRocq.Erasure.EInduction

• Deriving a compact induction principle for terms

Library MetaRocq.Erasure.EInlineProjections

Library MetaRocq.Erasure.EInlining

Library MetaRocq.Erasure.ELiftSubst

• Lifting and substitution for the AST

Library MetaRocq.Erasure.EOptimizePropDiscr

Library MetaRocq.Erasure.EPretty

• Pretty printing

Library MetaRocq.Erasure.EPrimitive

Library MetaRocq.Erasure.EProgram

Library MetaRocq.Erasure.EReflect

Library MetaRocq.Erasure.ERemoveParams

Library MetaRocq.Erasure.EReorderCstrs

Library MetaRocq.Erasure.ESpineView

Library MetaRocq.Erasure.ESubstitution

• • Global Weakening
  • Weakening

Library MetaRocq.Erasure.EUnboxing

Library MetaRocq.Erasure.EWcbvEval

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

Library MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksFixLambdaInd

Library MetaRocq.Erasure.EWcbvEvalCstrsAsBlocksInd

Library MetaRocq.Erasure.EWcbvEvalEtaInd

Library MetaRocq.Erasure.EWcbvEvalInd

Library MetaRocq.Erasure.EWcbvEvalNamed

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

Library MetaRocq.Erasure.EWellformed

Library MetaRocq.Erasure.EWtAst

• Well-scoped and well-formed extracted terms

Library MetaRocq.Erasure.ErasureCorrectness

• Correctness of erasure
  • The correctness proof

Library MetaRocq.Erasure.ErasureFunction

Library MetaRocq.Erasure.ErasureFunctionProperties

Library MetaRocq.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 MetaRocq.Erasure.Extract

Library MetaRocq.Erasure.Prelim

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

Library MetaRocq.PCUIC.PCUICAlpha

Library MetaRocq.PCUIC.PCUICArities

Library MetaRocq.PCUIC.PCUICAst

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

Library MetaRocq.PCUIC.PCUICCSubst

• Closed single substitution:

Library MetaRocq.PCUIC.PCUICCanonicity

Library MetaRocq.PCUIC.PCUICCasesContexts

Library MetaRocq.PCUIC.PCUICCasesHelper

Library MetaRocq.PCUIC.PCUICClassification

Library MetaRocq.PCUIC.PCUICConfluence

Library MetaRocq.PCUIC.PCUICConsistency

Library MetaRocq.PCUIC.PCUICContextConversion

Library MetaRocq.PCUIC.PCUICContextReduction

Library MetaRocq.PCUIC.PCUICContextSubst

• Substitution lemmas for typing derivations.

Library MetaRocq.PCUIC.PCUICContexts

Library MetaRocq.PCUIC.PCUICConvCumInversion

Library MetaRocq.PCUIC.PCUICConversion

Library MetaRocq.PCUIC.PCUICCumulProp

Library MetaRocq.PCUIC.PCUICCumulativity

• Definition of cumulativity and conversion relations
  • Cumulativity

Library MetaRocq.PCUIC.PCUICCumulativitySpec

• Definition of cumulativity and conversion relations

Library MetaRocq.PCUIC.PCUICElimination

Library MetaRocq.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 MetaRocq.PCUIC.PCUICEtaExpand

Library MetaRocq.PCUIC.PCUICExpandLets

Library MetaRocq.PCUIC.PCUICExpandLetsCorrectness

Library MetaRocq.PCUIC.PCUICFirstorder

Library MetaRocq.PCUIC.PCUICGeneration

Library MetaRocq.PCUIC.PCUICGlobalEnv

Library MetaRocq.PCUIC.PCUICGuardCondition

Library MetaRocq.PCUIC.PCUICInductiveInversion

Library MetaRocq.PCUIC.PCUICInductives

• Projections

Library MetaRocq.PCUIC.PCUICInversion

Library MetaRocq.PCUIC.PCUICLoader

Library MetaRocq.PCUIC.PCUICMonadAst

Library MetaRocq.PCUIC.PCUICNormal

Library MetaRocq.PCUIC.PCUICNormalization

Library MetaRocq.PCUIC.PCUICParallelReduction

Library MetaRocq.PCUIC.PCUICParallelReductionConfluence

Library MetaRocq.PCUIC.PCUICPrincipality

Library MetaRocq.PCUIC.PCUICProgram

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

Library MetaRocq.PCUIC.PCUICProgress

Library MetaRocq.PCUIC.PCUICRedTypeIrrelevance

Library MetaRocq.PCUIC.PCUICReduction

Library MetaRocq.PCUIC.PCUICSN

Library MetaRocq.PCUIC.PCUICSR

Library MetaRocq.PCUIC.PCUICSafeLemmata

Library MetaRocq.PCUIC.PCUICSigmaCalculus

• Theory of σ-calculus operations

Library MetaRocq.PCUIC.PCUICSpine

Library MetaRocq.PCUIC.PCUICSubstitution

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

Library MetaRocq.PCUIC.PCUICTelescopes

Library MetaRocq.PCUIC.PCUICTypedAst

Library MetaRocq.PCUIC.PCUICTyping

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

Library MetaRocq.PCUIC.PCUICUnivLevels

Library MetaRocq.PCUIC.PCUICValidity

Library MetaRocq.PCUIC.PCUICWcbvEval

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

Library MetaRocq.PCUIC.PCUICWeakeningConfig

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

Library MetaRocq.PCUIC.PCUICWeakeningConfigSN

Library MetaRocq.PCUIC.PCUICWeakeningEnv

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

Library MetaRocq.PCUIC.PCUICWeakeningEnvSN

Library MetaRocq.PCUIC.PCUICWellScopedCumulativity

Library MetaRocq.PCUIC.PCUICWfCases

Library MetaRocq.PCUIC.PCUICWfUniverses

Library MetaRocq.PCUIC.PCUICWtCumulativity

Library MetaRocq.Quotation.CommonUtils

Library MetaRocq.SafeCheckerPlugin.Extraction

• Extraction setup for the safechecker phase of MetaRocq.

Library MetaRocq.SafeCheckerPlugin.Loader

Library MetaRocq.SafeCheckerPlugin.SafeTemplateChecker

Library MetaRocq.SafeChecker.PCUICEqualityDec

• • Boolean of equality **

Library MetaRocq.SafeChecker.PCUICErrors

Library MetaRocq.SafeChecker.PCUICRetypingEnvIrrelevance

Library MetaRocq.SafeChecker.PCUICSafeChecker

Library MetaRocq.SafeChecker.PCUICSafeConversion

• Conversion for PCUIC without fuel

Library MetaRocq.SafeChecker.PCUICSafeReduce

• Reduction machine for PCUIC without fuel

Library MetaRocq.SafeChecker.PCUICSafeRetyping

• Retyping

Library MetaRocq.SafeChecker.PCUICTypeChecker

Library MetaRocq.SafeChecker.PCUICWfEnv

Library MetaRocq.SafeChecker.PCUICWfEnvImpl

Library MetaRocq.SafeChecker.PCUICWfReduction

Library MetaRocq.TemplatePCUIC.Loader

Library MetaRocq.TemplatePCUIC.PCUICTemplateMonad

Library MetaRocq.TemplatePCUIC.PCUICToTemplate

Library MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness

Library MetaRocq.TemplatePCUIC.PCUICTransform

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

Library MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC

Library MetaRocq.TemplatePCUIC.TemplateToPCUIC

Library MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness

Library MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded

Library MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval

Library MetaRocq.Template.All

Library MetaRocq.Template.Ast

• AST of Rocq 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 MetaRocq.Template.AstUtils

• Traversal functions.

Library MetaRocq.Template.Checker

• Rocq type-checker for kernel terms

Library MetaRocq.Template.Constants

Library MetaRocq.Template.EtaExpand

• Eta-expansion and proof generation

Library MetaRocq.Template.ExtractableLoader

Library MetaRocq.Template.Extraction

• Extraction setup for template-rocq.

Library MetaRocq.Template.Induction

• Deriving a compact induction principle for terms

Library MetaRocq.Template.Lib

• Commands.
• Useful shortcuts.
• Monadic notations.
• Packed inductives and constructors.

Library MetaRocq.Template.LiftSubst

• Lifting and substitution for the AST

Library MetaRocq.Template.Loader

Library MetaRocq.Template.MonadAst

Library MetaRocq.Template.Normal

Library MetaRocq.Template.Pretty

• Pretty printing

Library MetaRocq.Template.Reduction

Library MetaRocq.Template.ReflectAst

Library MetaRocq.Template.TemplateCheckWf

Library MetaRocq.Template.TemplateEnvMap

Library MetaRocq.Template.TemplateMonad

Library MetaRocq.Template.TemplateProgram

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

Library MetaRocq.Template.TermEquality

• • Syntactic equality up-to universes

Library MetaRocq.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.

Library MetaRocq.Template.TypingWf

• Well-formedness of terms and types in typing derivations

Library MetaRocq.Template.UnivSubst

• Universe substitution

Library MetaRocq.Template.WcbvEval

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

Library MetaRocq.Template.WfAst

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

Library MetaRocq.Utils.All_Forall

Library MetaRocq.Utils.ByteCompare

Library MetaRocq.Utils.ByteCompareSpec

Library MetaRocq.Utils.ByteCompare_opt

Library MetaRocq.Utils.LibHypsNaming

• • The custom renaming tactic

Library MetaRocq.Utils.MRArith

Library MetaRocq.Utils.MRCompare

Library MetaRocq.Utils.MREquality

Library MetaRocq.Utils.MRFSets

Library MetaRocq.Utils.MRList

Library MetaRocq.Utils.MRListable

Library MetaRocq.Utils.MRMSets

Library MetaRocq.Utils.MROption

Library MetaRocq.Utils.MRPred

Library MetaRocq.Utils.MRPrelude

Library MetaRocq.Utils.MRProd

Library MetaRocq.Utils.MRReflect

• Notion of reflection for Type-based properties

Library MetaRocq.Utils.MRRelations

Library MetaRocq.Utils.MRSquash

Library MetaRocq.Utils.MRString

Library MetaRocq.Utils.MRUtils

Library MetaRocq.Utils.MR_ExtrOCamlInt63

Library MetaRocq.Utils.MR_ExtrOCamlNatInt

Library MetaRocq.Utils.MR_ExtrOCamlZPosInt

Library MetaRocq.Utils.ReflectEq

Library MetaRocq.Utils.Show

Library MetaRocq.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 MetaRocq.Utils.monad_utils

Library MetaRocq.Utils.utils

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

Library MetaRocq.Utils.wGraph

• • Main results about acyclicity

Library MetaRocq.Erasure.Typed.Annotations

• More utility functions

Library MetaRocq.Erasure.Typed.Certifying

• Term and proof generation for the certifying transforms

Library MetaRocq.Erasure.Typed.CertifyingBeta

Library MetaRocq.Erasure.Typed.CertifyingEta

• Eta-expansion and proof generation

Library MetaRocq.Erasure.Typed.CertifyingInlining

• Inlining pass on the Template Rocq representation

Library MetaRocq.Erasure.Typed.ClosedAux

Library MetaRocq.Erasure.Typed.Erasure

Library MetaRocq.Erasure.Typed.ErasureCorrectness

Library MetaRocq.Erasure.Typed.ExAst

Library MetaRocq.Erasure.Typed.Extraction

Library MetaRocq.Erasure.Typed.ExtractionCorrectness

Library MetaRocq.Erasure.Typed.Optimize

Library MetaRocq.Erasure.Typed.OptimizeCorrectness

Library MetaRocq.Erasure.Typed.OptimizePropDiscr

Library MetaRocq.Erasure.Typed.ResultMonad

Library MetaRocq.Erasure.Typed.Transform

Library MetaRocq.Erasure.Typed.TypeAnnotations

Library MetaRocq.Erasure.Typed.Utils

Library MetaRocq.Erasure.Typed.WcbvEvalAux

Library MetaRocq.PCUIC.Bidirectional.BDFromPCUIC

Library MetaRocq.PCUIC.Bidirectional.BDStrengthening

Library MetaRocq.PCUIC.Bidirectional.BDToPCUIC

Library MetaRocq.PCUIC.Bidirectional.BDTyping

Library MetaRocq.PCUIC.Bidirectional.BDUnique

Library MetaRocq.PCUIC.Conversion.PCUICClosedConv

Library MetaRocq.PCUIC.Conversion.PCUICInstConv

• Type preservation for σ-calculus instantiation

Library MetaRocq.PCUIC.Conversion.PCUICNamelessConv

Library MetaRocq.PCUIC.Conversion.PCUICOnFreeVarsConv

Library MetaRocq.PCUIC.Conversion.PCUICRenameConv

• Type preservation for σ-calculus operations

Library MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv

• Universe Substitution lemmas for typing derivations.

Library MetaRocq.PCUIC.Conversion.PCUICWeakeningConfigConv

Library MetaRocq.PCUIC.Conversion.PCUICWeakeningConv

• Weakening lemmas for typing derivations.

Library MetaRocq.PCUIC.Conversion.PCUICWeakeningEnvConv

Library MetaRocq.PCUIC.Syntax.PCUICCases

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

Library MetaRocq.PCUIC.Syntax.PCUICClosed

• Lemmas about the closedn predicate

Library MetaRocq.PCUIC.Syntax.PCUICDepth

Library MetaRocq.PCUIC.Syntax.PCUICInduction

• Deriving a compact induction principle for terms

Library MetaRocq.PCUIC.Syntax.PCUICInstDef

• Type preservation for σ-calculus instantiation

Library MetaRocq.PCUIC.Syntax.PCUICLiftSubst

• Commutation lemmas for the lifting and substitution operations.

Library MetaRocq.PCUIC.Syntax.PCUICNamelessDef

Library MetaRocq.PCUIC.Syntax.PCUICOnFreeVars

• Preservation of free variables

Library MetaRocq.PCUIC.Syntax.PCUICPosition

Library MetaRocq.PCUIC.Syntax.PCUICReflect

Library MetaRocq.PCUIC.Syntax.PCUICRenameDef

• Type preservation for σ-calculus operations

Library MetaRocq.PCUIC.Syntax.PCUICTactics

Library MetaRocq.PCUIC.Syntax.PCUICUnivSubst

Library MetaRocq.PCUIC.Syntax.PCUICViews

Library MetaRocq.PCUIC.Typing.PCUICClosedTyp

Library MetaRocq.PCUIC.Typing.PCUICContextConversionTyp

Library MetaRocq.PCUIC.Typing.PCUICInstTyp

• Type preservation for σ-calculus instantiation

Library MetaRocq.PCUIC.Typing.PCUICNamelessTyp

Library MetaRocq.PCUIC.Typing.PCUICRenameTyp

• Type preservation for σ-calculus operations

Library MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp

• Universe Substitution lemmas for typing derivations.

Library MetaRocq.PCUIC.Typing.PCUICWeakeningConfigTyp

Library MetaRocq.PCUIC.Typing.PCUICWeakeningEnvTyp

Library MetaRocq.PCUIC.Typing.PCUICWeakeningTyp

• Weakening lemmas for typing derivations.

Library MetaRocq.PCUIC.utils.PCUICAstUtils

Library MetaRocq.PCUIC.utils.PCUICOnOne

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

Library MetaRocq.PCUIC.utils.PCUICPretty

• Pretty printing

Library MetaRocq.PCUIC.utils.PCUICPrimitive

Library MetaRocq.PCUIC.utils.PCUICSize

Library MetaRocq.PCUIC.utils.PCUICUtils

Library MetaRocq.Quotation.ToPCUIC.All

Library MetaRocq.Quotation.ToPCUIC.Equations

Library MetaRocq.Quotation.ToPCUIC.Init

Library MetaRocq.Quotation.ToTemplate.All

Library MetaRocq.Quotation.ToTemplate.Equations

Library MetaRocq.Quotation.ToTemplate.Init

Library MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core

Library MetaRocq.Template.TemplateMonad.Common

Library MetaRocq.Template.TemplateMonad.Core

• The Template Monad
  • • The TemplateMonad type

Library MetaRocq.Template.TemplateMonad.Extractable

• The Extractable Template Monad

Library MetaRocq.Utils.MRTactics.DestructHead

Library MetaRocq.Utils.MRTactics.DestructHyps

Library MetaRocq.Utils.MRTactics.FindHyp

Library MetaRocq.Utils.MRTactics.GeneralizeOverHoles

Library MetaRocq.Utils.MRTactics.Head

Library MetaRocq.Utils.MRTactics.InHypUnderBindersDo

Library MetaRocq.Utils.MRTactics.SpecializeAllWays

Library MetaRocq.Utils.MRTactics.SpecializeBy

Library MetaRocq.Utils.MRTactics.SpecializeUnderBindersBy

Library MetaRocq.Utils.MRTactics.SplitInContext

Library MetaRocq.Utils.MRTactics.UniquePose

Library MetaRocq.Utils.MRTactics.Zeta1

Library MetaRocq.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 MetaRocq.Utils.canonicaltries.String2pos

Library MetaRocq.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 MetaRocq.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 MetaRocq.Translations.param_binary

Library MetaRocq.Translations.param_cheap_packed

Library MetaRocq.Translations.param_generous_packed

Library MetaRocq.Translations.param_generous_unpacked

Library MetaRocq.Translations.param_original

Library MetaRocq.Translations.sigma

Library MetaRocq.Translations.standard_model

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

Library MetaRocq.Translations.times_bool_fun

Library MetaRocq.Translations.times_bool_fun2

Library MetaRocq.Translations.translation_utils

Library MetaRocq.Examples.add_constructor

• • Auxiliary functions
• Plugin
• Examples

Library MetaRocq.Examples.constructor_tac

Library MetaRocq.Examples.demo

Library MetaRocq.Examples.metarocq_tour

Library MetaRocq.Examples.metarocq_tour_prelude

Library MetaRocq.Examples.tauto

Library MetaRocq.Examples.typing_correctness