| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |
T
T [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]T [inductive, in MetaRocq.Examples.demo]
T [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Tags [section, in MetaRocq.Erasure.EReorderCstrs]
tAnd [definition, in MetaRocq.Examples.tauto]
TAny [constructor, in MetaRocq.Erasure.Typed.ExAst]
TApp [constructor, in MetaRocq.Erasure.Typed.ExAst]
tApp [constructor, in MetaRocq.PCUIC.PCUICAst]
tApp [constructor, in MetaRocq.Erasure.EAst]
tApp [constructor, in MetaRocq.Template.Ast]
tApp_mkApps [lemma, in MetaRocq.Erasure.EImplementBox]
tApp_mkApps [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
tApp_mkApps_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
tApp_mkApps [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
target_wcbv_flags [definition, in MetaRocq.Erasure.EWcbvEval]
target_edge_of_level [lemma, in MetaRocq.Common.uGraph]
TArr [constructor, in MetaRocq.Erasure.Typed.ExAst]
tArray [constructor, in MetaRocq.Template.Ast]
tauto [library]
tauto_sound [lemma, in MetaRocq.Examples.tauto]
tauto_s [definition, in MetaRocq.Examples.tauto]
tauto_proc [definition, in MetaRocq.Examples.tauto]
TBox [constructor, in MetaRocq.Erasure.Typed.ExAst]
tBox [constructor, in MetaRocq.Erasure.EAst]
tCase [constructor, in MetaRocq.PCUIC.PCUICAst]
tCase [constructor, in MetaRocq.Erasure.EAst]
tCase [constructor, in MetaRocq.Template.Ast]
tCaseBrsProp [definition, in MetaRocq.PCUIC.PCUICAst]
tCaseBrsProp [definition, in MetaRocq.Template.Ast]
tCaseBrsProp_k [definition, in MetaRocq.PCUIC.PCUICAst]
tCaseBrsType [definition, in MetaRocq.Template.AstUtils]
tCasePredProp [definition, in MetaRocq.PCUIC.PCUICAst]
tCasePredProp [definition, in MetaRocq.Template.Ast]
tCasePredProp_k [definition, in MetaRocq.PCUIC.PCUICAst]
tCast [constructor, in MetaRocq.Template.Ast]
tCoFix [constructor, in MetaRocq.PCUIC.PCUICAst]
tCoFix [constructor, in MetaRocq.Erasure.EAst]
tCoFix [constructor, in MetaRocq.Template.Ast]
tCoFix_no_Type [lemma, in MetaRocq.Erasure.EArities]
TConst [constructor, in MetaRocq.Erasure.Typed.ExAst]
tConst [constructor, in MetaRocq.PCUIC.PCUICAst]
tConst [constructor, in MetaRocq.Erasure.EAst]
tConst [constructor, in MetaRocq.Template.Ast]
tConstruct [constructor, in MetaRocq.PCUIC.PCUICAst]
tConstruct [constructor, in MetaRocq.Erasure.EAst]
tConstruct [constructor, in MetaRocq.Template.Ast]
tConstruct_no_Type [lemma, in MetaRocq.Erasure.EArities]
Tcontext [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
tCtxApp_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxApp_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_branch [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_discr [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_pred [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxCase_pars [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxEvar [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxHead [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxHead_nat [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxHole [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxLambda_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxLambda_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_b [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxLetIn_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxProd_r [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxProd_l [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxProj [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxTail [constructor, in MetaRocq.PCUIC.PCUICReduction]
tCtxTail_nat [constructor, in MetaRocq.PCUIC.PCUICReduction]
tDummy [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
tDummy [definition, in MetaRocq.Template.Ast]
telescope [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_cons_def [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_cons_abs [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope_n_nil [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_def [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_cons_abs [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
telescope2_nil [constructor, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
TemplateCheckWf [library]
TemplateConversion [module, in MetaRocq.Template.Typing]
TemplateConversionPar [module, in MetaRocq.Template.Typing]
TemplateConversionPar.cumul_gen [definition, in MetaRocq.Template.Typing]
TemplateDeclarationTyping [module, in MetaRocq.Template.Typing]
TemplateEnvMap [library]
TemplateEnvTyping [module, in MetaRocq.Template.Typing]
TemplateGlobalMaps [module, in MetaRocq.Template.Typing]
TemplateLookup [module, in MetaRocq.Template.Ast]
TemplateMonad [inductive, in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad [projection, in MetaRocq.Template.TemplateMonad.Common]
TemplateMonad [library]
TemplateMonadNotations [module, in MetaRocq.Template.Lib]
_ ;; _ (tm_scope) [notation, in MetaRocq.Template.Lib]
' _ <- _ ;; _ (tm_scope) [notation, in MetaRocq.Template.Lib]
_ <- _ ;; _ (tm_scope) [notation, in MetaRocq.Template.Lib]
mlet ' _ <- _ ;; _ (tm_scope) [notation, in MetaRocq.Template.Lib]
mlet _ <- _ ;; _ (tm_scope) [notation, in MetaRocq.Template.Lib]
_ =<< _ (tm_scope) [notation, in MetaRocq.Template.Lib]
_ >>= _ (tm_scope) [notation, in MetaRocq.Template.Lib]
TemplateMonadToPCUIC [library]
TemplateMonad_Monad [definition, in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_OptimizedMonad [definition, in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_UnoptimizedMonad [definition, in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_sind [definition, in MetaRocq.Template.TemplateMonad.Core]
TemplateMonad_ind [definition, in MetaRocq.Template.TemplateMonad.Core]
TemplateProgram [library]
TemplateTerm [module, in MetaRocq.Template.Ast]
TemplateTermDecide [module, in MetaRocq.Template.ReflectAst]
TemplateTermDecide.term_eq_dec [instance, in MetaRocq.Template.ReflectAst]
TemplateTermUtils [module, in MetaRocq.Template.Ast]
TemplateTermUtils.destArity [definition, in MetaRocq.Template.Ast]
TemplateTermUtils.inds [definition, in MetaRocq.Template.Ast]
TemplateTerm.closedn [definition, in MetaRocq.Template.Ast]
TemplateTerm.lift [definition, in MetaRocq.Template.Ast]
TemplateTerm.mkApps [definition, in MetaRocq.Template.Ast]
TemplateTerm.noccur_between [definition, in MetaRocq.Template.Ast]
TemplateTerm.subst [definition, in MetaRocq.Template.Ast]
TemplateTerm.subst_instance_constr [definition, in MetaRocq.Template.Ast]
TemplateTerm.term [definition, in MetaRocq.Template.Ast]
TemplateTerm.tInd [definition, in MetaRocq.Template.Ast]
TemplateTerm.tLambda [definition, in MetaRocq.Template.Ast]
TemplateTerm.tLetIn [definition, in MetaRocq.Template.Ast]
TemplateTerm.tProd [definition, in MetaRocq.Template.Ast]
TemplateTerm.tProj [definition, in MetaRocq.Template.Ast]
TemplateTerm.tRel [definition, in MetaRocq.Template.Ast]
TemplateTerm.tSort [definition, in MetaRocq.Template.Ast]
TemplateToPCUIC [library]
TemplateToPCUICCorrectness [library]
TemplateToPCUICExpanded [library]
TemplateToPCUICWcbvEval [library]
TemplateTransform [definition, in MetaRocq.Erasure.Typed.Transform]
TemplateTyping [module, in MetaRocq.Template.Typing]
TemplateTyping.typing [definition, in MetaRocq.Template.Typing]
template_program_env [definition, in MetaRocq.Template.TemplateProgram]
template_program [definition, in MetaRocq.Template.TemplateProgram]
template_transforms [projection, in MetaRocq.Erasure.Typed.Extraction]
template_eta [definition, in MetaRocq.Erasure.Typed.CertifyingEta]
template_betared [definition, in MetaRocq.Erasure.Typed.CertifyingBeta]
template_to_pcuic_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
template_to_pcuic_typing [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env_ext [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic_env [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_to_pcuic [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
template_wf_cons_inv [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
template_to_pcuic_transform [definition, in MetaRocq.TemplatePCUIC.PCUICTransform]
template_inline [definition, in MetaRocq.Erasure.Typed.CertifyingInlining]
Term [module, in MetaRocq.Common.Environment]
term [inductive, in MetaRocq.PCUIC.PCUICAst]
term [inductive, in MetaRocq.Erasure.EAst]
Term [constructor, in MetaRocq.SafeChecker.PCUICSafeConversion]
term [inductive, in MetaRocq.Template.Ast]
TermDecide [module, in MetaRocq.Common.Environment]
TermDecideReflectInstances [module, in MetaRocq.Common.Environment]
TermDecide.term_eq_dec [instance, in MetaRocq.Common.Environment]
TermEquality [library]
TermoptTyp [abbreviation, in MetaRocq.Common.BasicAst]
TermSpineView [module, in MetaRocq.Erasure.ESpineView]
TermSpineView.t [inductive, in MetaRocq.Erasure.ESpineView]
TermSpineView.tApp [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tBox [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tCase [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tCoFix [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tConst [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tConstruct [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tEvar [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tFix [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tForce [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tLambda [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tLazy [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tLetIn [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tPrim [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tProj [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tRel [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.tVar [constructor, in MetaRocq.Erasure.ESpineView]
TermSpineView.t_sind [definition, in MetaRocq.Erasure.ESpineView]
TermSpineView.t_rec [definition, in MetaRocq.Erasure.ESpineView]
TermSpineView.t_ind [definition, in MetaRocq.Erasure.ESpineView]
TermSpineView.t_rect [definition, in MetaRocq.Erasure.ESpineView]
TermSpineView.view [definition, in MetaRocq.Erasure.ESpineView]
TermSpineView.view_mkApps [lemma, in MetaRocq.Erasure.ESpineView]
terms_global_deps_gen [abbreviation, in MetaRocq.Erasure.ErasureFunction]
terms_global_deps_skipn [lemma, in MetaRocq.Erasure.ErasureFunction]
terms_global_deps_rev [lemma, in MetaRocq.Erasure.ErasureFunction]
terms_global_deps [abbreviation, in MetaRocq.Erasure.ErasureFunction]
TermTyp [abbreviation, in MetaRocq.Common.BasicAst]
TermTypUniv [abbreviation, in MetaRocq.Common.BasicAst]
TermUtils [module, in MetaRocq.Common.Environment]
TermUtils.destArity [axiom, in MetaRocq.Common.Environment]
TermUtils.inds [axiom, in MetaRocq.Common.Environment]
term_sub_ctx_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
term_sub_ctx_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
term_sub_ctx [inductive, in MetaRocq.Erasure.Typed.Erasure]
term_rel [definition, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cunfold_cofix [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cofix_subst [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_cunfold_fix [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_fix_subst [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_repeat [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_iota_red [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_substl [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_mkApps [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_fresh [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_csubst [lemma, in MetaRocq.Erasure.ErasureFunction]
term_global_deps_spec [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
term_flags [definition, in MetaRocq.Erasure.EWcbvEvalEtaInd]
term_wf_forall_list_ind [lemma, in MetaRocq.Template.WfAst]
term_ind_size_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_ctx_list_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_mkApps_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_forall_list_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICInduction]
term_sind [definition, in MetaRocq.PCUIC.PCUICAst]
term_rec [definition, in MetaRocq.PCUIC.PCUICAst]
term_ind [definition, in MetaRocq.PCUIC.PCUICAst]
term_rect [definition, in MetaRocq.PCUIC.PCUICAst]
term_ind_depth_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
term_forall_ctx_list_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
term_forall_list_rect [lemma, in MetaRocq.Template.Induction]
term_forall_list_ind [lemma, in MetaRocq.Template.Induction]
term_sind [definition, in MetaRocq.Erasure.EAst]
term_rec [definition, in MetaRocq.Erasure.EAst]
term_ind [definition, in MetaRocq.Erasure.EAst]
term_rect [definition, in MetaRocq.Erasure.EAst]
term_context_sind [definition, in MetaRocq.PCUIC.PCUICReduction]
term_context_rec [definition, in MetaRocq.PCUIC.PCUICReduction]
term_context_ind [definition, in MetaRocq.PCUIC.PCUICReduction]
term_context_rect [definition, in MetaRocq.PCUIC.PCUICReduction]
term_context [inductive, in MetaRocq.PCUIC.PCUICReduction]
term_switches [projection, in MetaRocq.Erasure.EWellformed]
term_subterm_redp [lemma, in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm_red1 [lemma, in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm_wf [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm_context [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_subterm [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_context [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_sind [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_rec [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_ind [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_rect [definition, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_12_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_2 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_11_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_2 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_7_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_3 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_2 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_6_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_2 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_5_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_2 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm_4_1 [constructor, in MetaRocq.SafeChecker.PCUICWfReduction]
term_direct_subterm [inductive, in MetaRocq.SafeChecker.PCUICWfReduction]
term_forall_list_ind [lemma, in MetaRocq.Erasure.EInduction]
term_eqb [definition, in MetaRocq.Template.Lib]
term_on_free_vars_ind [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
term_noccur_between_list_ind [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
term_closedn_list_ind [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
term_sind [definition, in MetaRocq.Template.Ast]
term_rec [definition, in MetaRocq.Template.Ast]
term_ind [definition, in MetaRocq.Template.Ast]
term_rect [definition, in MetaRocq.Template.Ast]
term_global_deps [definition, in MetaRocq.Erasure.EAstUtils]
Term.closedn [axiom, in MetaRocq.Common.Environment]
Term.lift [axiom, in MetaRocq.Common.Environment]
Term.lift0 [abbreviation, in MetaRocq.Common.Environment]
Term.mkApps [axiom, in MetaRocq.Common.Environment]
Term.noccur_between [axiom, in MetaRocq.Common.Environment]
Term.subst [axiom, in MetaRocq.Common.Environment]
Term.subst_instance_constr [axiom, in MetaRocq.Common.Environment]
Term.term [axiom, in MetaRocq.Common.Environment]
Term.tInd [axiom, in MetaRocq.Common.Environment]
Term.tLambda [axiom, in MetaRocq.Common.Environment]
Term.tLetIn [axiom, in MetaRocq.Common.Environment]
Term.tProd [axiom, in MetaRocq.Common.Environment]
Term.tProj [axiom, in MetaRocq.Common.Environment]
Term.tRel [axiom, in MetaRocq.Common.Environment]
Term.tSort [axiom, in MetaRocq.Common.Environment]
test [lemma, in MetaRocq.Examples.tauto]
test [definition, in MetaRocq.Examples.add_constructor]
test [definition, in MetaRocq.Examples.metarocq_tour]
test_branches_k_pars [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICPosition]
test_branch_k_pars [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
test_context_k_map [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_mapi [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_decl_map_decl [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_app [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
test_context_k_impl [lemma, in MetaRocq.PCUIC.utils.PCUICOnOne]
test_decl_conv_decls_map [lemma, in MetaRocq.PCUIC.PCUICConversion]
test_decl_map_decl [lemma, in MetaRocq.Common.BasicAst]
test_decl_impl [lemma, in MetaRocq.Common.BasicAst]
test_context_k_proper [instance, in MetaRocq.Common.BasicAst]
test_context_k [definition, in MetaRocq.Common.BasicAst]
test_context_proper [instance, in MetaRocq.Common.BasicAst]
test_context [definition, in MetaRocq.Common.BasicAst]
test_decl_proper [instance, in MetaRocq.Common.BasicAst]
test_decl [definition, in MetaRocq.Common.BasicAst]
test_def [definition, in MetaRocq.Common.BasicAst]
test_context_app [lemma, in MetaRocq.PCUIC.PCUICAst]
test_context_map [lemma, in MetaRocq.PCUIC.PCUICAst]
test_branch_k_Proper [instance, in MetaRocq.PCUIC.PCUICAst]
test_predicate_ku_Proper [instance, in MetaRocq.PCUIC.PCUICAst]
test_predicate_k_Proper [instance, in MetaRocq.PCUIC.PCUICAst]
test_context_k_Proper [instance, in MetaRocq.PCUIC.PCUICAst]
test_context_k_eq [lemma, in MetaRocq.PCUIC.PCUICAst]
test_context_k_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
test_context_k_eqP_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
test_context_k_eqP_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
test_prim_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
test_prim_mapu [lemma, in MetaRocq.PCUIC.PCUICAst]
test_primu_test_primu_tPrimProp [lemma, in MetaRocq.PCUIC.PCUICAst]
test_prim_primProp [lemma, in MetaRocq.PCUIC.PCUICAst]
test_branches_nlict [definition, in MetaRocq.PCUIC.PCUICAst]
test_branch_nlict [definition, in MetaRocq.PCUIC.PCUICAst]
test_context_nlict [definition, in MetaRocq.PCUIC.PCUICAst]
test_branches_k [abbreviation, in MetaRocq.PCUIC.PCUICAst]
test_branch_k [definition, in MetaRocq.PCUIC.PCUICAst]
test_branch [definition, in MetaRocq.PCUIC.PCUICAst]
test_predicate_ku [definition, in MetaRocq.PCUIC.PCUICAst]
test_predicate_k [definition, in MetaRocq.PCUIC.PCUICAst]
test_predicate [definition, in MetaRocq.PCUIC.PCUICAst]
test_def [definition, in MetaRocq.Erasure.EAst]
test_snd [definition, in MetaRocq.Utils.MRProd]
test_primu_test_primu_tPrimProp [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_k_ctx [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_mapi [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
test_primu_primProp [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
test_primu_mapu [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
test_context_k_closed_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_context_k_ctx [lemma, in MetaRocq.PCUIC.Syntax.PCUICOnFreeVars]
test_branches_k [abbreviation, in MetaRocq.Template.Ast]
test_branch [definition, in MetaRocq.Template.Ast]
test_predicate_k [definition, in MetaRocq.Template.Ast]
test_predicate [definition, in MetaRocq.Template.Ast]
test_primIn_spec [lemma, in MetaRocq.Erasure.EPrimitive]
test_primIn [definition, in MetaRocq.Erasure.EPrimitive]
test_prim_eq_prop [lemma, in MetaRocq.Erasure.EPrimitive]
test_prim_map [lemma, in MetaRocq.Erasure.EPrimitive]
test_prim_impl_primProp [lemma, in MetaRocq.Erasure.EPrimitive]
test_prim_primProp [lemma, in MetaRocq.Erasure.EPrimitive]
test_prim [definition, in MetaRocq.Erasure.EPrimitive]
test_array_model [definition, in MetaRocq.Erasure.EPrimitive]
test_primu [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
test_prim [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
test' [definition, in MetaRocq.Examples.add_constructor]
test2 [lemma, in MetaRocq.Examples.tauto]
test2 [definition, in MetaRocq.Examples.add_constructor]
test3 [definition, in MetaRocq.Examples.add_constructor]
test4 [definition, in MetaRocq.Examples.add_constructor]
tEvar [constructor, in MetaRocq.PCUIC.PCUICAst]
tEvar [constructor, in MetaRocq.Erasure.EAst]
tEvar [constructor, in MetaRocq.Template.Ast]
tFix [constructor, in MetaRocq.PCUIC.PCUICAst]
tFix [constructor, in MetaRocq.Erasure.EAst]
tFix [constructor, in MetaRocq.Template.Ast]
tFixCoFix [definition, in MetaRocq.PCUIC.PCUICGuardCondition]
tFixProp [definition, in MetaRocq.Common.BasicAst]
tFixType [definition, in MetaRocq.Template.AstUtils]
tfix_map_spec [lemma, in MetaRocq.Common.BasicAst]
tfix_forallb_map_spec [lemma, in MetaRocq.Template.Ast]
tFloat [abbreviation, in MetaRocq.PCUIC.PCUICAst]
tFloat [constructor, in MetaRocq.Template.Ast]
tForce [constructor, in MetaRocq.Erasure.EAst]
throwIf [definition, in MetaRocq.Erasure.Typed.Optimize]
time [definition, in MetaRocq.Common.Transform]
timed [definition, in MetaRocq.Erasure.Typed.Utils]
times_bool_fun [library]
times_bool_fun2 [library]
Times10 [constructor, in MetaRocq.Utils.MRProd]
Times3 [constructor, in MetaRocq.Utils.MRProd]
Times4 [constructor, in MetaRocq.Utils.MRProd]
Times5 [constructor, in MetaRocq.Utils.MRProd]
Times6 [constructor, in MetaRocq.Utils.MRProd]
Times7 [constructor, in MetaRocq.Utils.MRProd]
Times8 [constructor, in MetaRocq.Utils.MRProd]
Times9 [constructor, in MetaRocq.Utils.MRProd]
tImpl [definition, in MetaRocq.Examples.tauto]
tImpl [definition, in MetaRocq.Examples.typing_correctness]
tImpl [definition, in MetaRocq.Examples.metarocq_tour_prelude]
TInd [constructor, in MetaRocq.Erasure.Typed.ExAst]
tInd [constructor, in MetaRocq.PCUIC.PCUICAst]
tInd [constructor, in MetaRocq.Template.Ast]
tInt [abbreviation, in MetaRocq.PCUIC.PCUICAst]
tInt [constructor, in MetaRocq.Template.Ast]
TL [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TL [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
tLam [abbreviation, in MetaRocq.Template.Lib]
tLambda [constructor, in MetaRocq.PCUIC.PCUICAst]
tLambda [constructor, in MetaRocq.Erasure.EAst]
tLambda [constructor, in MetaRocq.Template.Ast]
tLazy [constructor, in MetaRocq.Erasure.EAst]
tLet [abbreviation, in MetaRocq.Template.Lib]
tLetIn [constructor, in MetaRocq.PCUIC.PCUICAst]
tLetIn [constructor, in MetaRocq.Erasure.EAst]
tLetIn [constructor, in MetaRocq.Template.Ast]
tm [inductive, in MetaRocq.Examples.add_constructor]
TM [inductive, in MetaRocq.Template.TemplateMonad.Extractable]
tmAxiom [definition, in MetaRocq.Template.TemplateMonad.Core]
tmAxiom [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmAxiomRed [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmAxiomRed [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmBind [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmBind [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmBind [projection, in MetaRocq.Template.TemplateMonad.Common]
tmCurrentModPath [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmCurrentModPath [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmCurrentModPath [projection, in MetaRocq.Template.TemplateMonad.Common]
tmDeclareQuotationOfConstants [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmDeclareQuotationOfConstants [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmDeclareQuotationOfModule [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmDeclareQuotationOfModule [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmDefinition [definition, in MetaRocq.Template.TemplateMonad.Core]
tmDefinition [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmDefinitionRed [definition, in MetaRocq.Template.TemplateMonad.Core]
tmDefinitionRed [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmDefinitionRed_ [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmDefinition_ [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmEval [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmEval [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmExistingInstance [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmExistingInstance [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmExistingInstance [projection, in MetaRocq.Template.TemplateMonad.Common]
tmFail [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmFail [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmFail [projection, in MetaRocq.Template.TemplateMonad.Common]
tmFix [definition, in MetaRocq.Template.TemplateMonad.Core]
tmFix' [definition, in MetaRocq.Template.TemplateMonad.Core]
tmFreshName [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmFreshName [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmFreshName [projection, in MetaRocq.Template.TemplateMonad.Common]
tmInductive [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmInductive' [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmInferInstance [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmInferInstance [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmInferInstanceRed [definition, in MetaRocq.Template.TemplateMonad.Extractable]
TMInstance [record, in MetaRocq.Template.TemplateMonad.Common]
tmLemma [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmLemma [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmLemmaRed [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmLocate [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmLocate [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmLocate [projection, in MetaRocq.Template.TemplateMonad.Common]
tmLocateInd [definition, in MetaRocq.Examples.tauto]
tmLocateModType [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmLocateModType [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmLocateModType [projection, in MetaRocq.Template.TemplateMonad.Common]
tmLocateModType1 [definition, in MetaRocq.Template.TemplateMonad.Core]
tmLocateModule [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmLocateModule [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmLocateModule [projection, in MetaRocq.Template.TemplateMonad.Common]
tmLocateModule1 [definition, in MetaRocq.Template.TemplateMonad.Core]
tmLocate1 [definition, in MetaRocq.Template.TemplateMonad.Core]
tmMakeQuotationOfConstants [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstants [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfConstantsWorkAroundRocqBug17303 [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstantsWorkAroundRocqBug17303 [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfConstants_gen [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfConstants_gen [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfModule [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfModule [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmMakeQuotationOfModuleWorkAroundRocqBug17303 [definition, in MetaRocq.Quotation.ToPCUIC.Init]
tmMakeQuotationOfModuleWorkAroundRocqBug17303 [definition, in MetaRocq.Quotation.ToTemplate.Init]
tmMaybeEval [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmMkDefinition [definition, in MetaRocq.Template.TemplateMonad.Core]
tmMkDefinition [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmMkInductive [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmMkInductive [projection, in MetaRocq.Template.TemplateMonad.Common]
tmMkInductive [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmMkInductive' [definition, in MetaRocq.Template.TemplateMonad.Core]
tmMsg [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmMsg [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmOpaqueDefinition [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tmOpaqueDefinitionRed [definition, in MetaRocq.Template.TemplateMonad.Core]
tmOptimize [definition, in MetaRocq.Template.TemplateMonad.Core]
tmOptimizedBind [definition, in MetaRocq.Template.TemplateMonad.Core]
tmOptimize' [definition, in MetaRocq.Template.TemplateMonad.Core]
tmPrint [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmPrint [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuote [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuote [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteConstant [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteConstant [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteConstant [projection, in MetaRocq.Template.TemplateMonad.Common]
tmQuoteConstant [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteDefinition [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteDefinitionRed [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteInductive [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmQuoteInductive [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteInductive [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteInductive [projection, in MetaRocq.Template.TemplateMonad.Common]
tmQuoteInductive [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteInductive' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
tmQuoteLevel [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModFunctor [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModFunctor [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteModType [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModType [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteModule [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteModule [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteRec [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRec [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteRecDefinition [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRecTransp [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteRecTransp [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmQuoteSort [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverse [definition, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverses [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmQuoteUniverses [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmQuoteUniverses [projection, in MetaRocq.Template.TemplateMonad.Common]
tmReturn [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmReturn [constructor, in MetaRocq.Template.TemplateMonad.Extractable]
tmReturn [projection, in MetaRocq.Template.TemplateMonad.Common]
tmTestQuote [definition, in MetaRocq.Template.TemplateMonad.Core]
tmTestUnquote [definition, in MetaRocq.Template.TemplateMonad.Core]
tmUnquote [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmUnquote [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmUnquoteTyped [constructor, in MetaRocq.Template.TemplateMonad.Core]
tmUnquoteTyped [definition, in MetaRocq.TemplatePCUIC.PCUICTemplateMonad.Core]
tmVariable [constructor, in MetaRocq.Template.TemplateMonad.Core]
tm_sind [definition, in MetaRocq.Examples.add_constructor]
tm_rec [definition, in MetaRocq.Examples.add_constructor]
tm_ind [definition, in MetaRocq.Examples.add_constructor]
tm_rect [definition, in MetaRocq.Examples.add_constructor]
TM_sind [definition, in MetaRocq.Template.TemplateMonad.Extractable]
TM_rec [definition, in MetaRocq.Template.TemplateMonad.Extractable]
TM_ind [definition, in MetaRocq.Template.TemplateMonad.Extractable]
TM_rect [definition, in MetaRocq.Template.TemplateMonad.Extractable]
tm1 [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
tm2 [projection, in MetaRocq.SafeChecker.PCUICSafeConversion]
todo [axiom, in MetaRocq.Utils.MRUtils]
toplevel_and_submodules [constructor, in MetaRocq.Quotation.ToPCUIC.Init]
toplevel_and_submodules [constructor, in MetaRocq.Quotation.ToTemplate.Init]
tOr [definition, in MetaRocq.Examples.tauto]
toto [constructor, in MetaRocq.Examples.demo]
to_extended_list_case_branch_context [lemma, in MetaRocq.PCUIC.PCUICSR]
to_extended_list_set_binder_name [lemma, in MetaRocq.PCUIC.PCUICSR]
to_extended_list_k_subst [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
to_extended_list_k_map_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
to_Z_bounded_bool [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
to_extended_list_k_cons [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_lift_above [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_spec [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_length [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
to_extended_list_k_map_subst [lemma, in MetaRocq.Template.EtaExpand]
to_extended_list_smash_context_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
to_kername [definition, in MetaRocq.Erasure.Typed.Utils]
to_extended_list_rename [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
to_extended_list_subst_context_let_expand [lemma, in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_length [lemma, in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_lift_context [lemma, in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_fold_context_k [lemma, in MetaRocq.PCUIC.PCUICContexts]
to_extended_list_k_app [lemma, in MetaRocq.PCUIC.PCUICContexts]
to_program [definition, in MetaRocq.ErasurePlugin.ETransform]
to_extended_list_k_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductives]
to_extended_list_k_map_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
to_extended_list_map_lift [lemma, in MetaRocq.PCUIC.Conversion.PCUICWeakeningConv]
to_extended_list_subst_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
to_N_inj [lemma, in MetaRocq.Utils.bytestring]
tPrim [constructor, in MetaRocq.PCUIC.PCUICAst]
tPrim [constructor, in MetaRocq.Erasure.EAst]
tPrimArray [abbreviation, in MetaRocq.SafeChecker.PCUICSafeConversion]
tPrimProp [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
tPrimProp_prod [lemma, in MetaRocq.PCUIC.PCUICAst]
tPrimProp_impl [lemma, in MetaRocq.PCUIC.PCUICAst]
tPro [abbreviation, in MetaRocq.Template.Lib]
tProd [constructor, in MetaRocq.PCUIC.PCUICAst]
tProd [constructor, in MetaRocq.Template.Ast]
tProd_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICConversion]
tProj [constructor, in MetaRocq.PCUIC.PCUICAst]
tProj [constructor, in MetaRocq.Erasure.EAst]
tProj [constructor, in MetaRocq.Template.Ast]
Tr [constructor, in MetaRocq.Examples.tauto]
trans [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Trans [section, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans [section, in MetaRocq.Erasure.ECoInductiveToInductive]
Transform [module, in MetaRocq.Common.Transform]
Transform [definition, in MetaRocq.Erasure.Typed.Transform]
Transform [library]
Transform [library]
TransformExt [module, in MetaRocq.Erasure.EProgram]
TransformExt.Comp [section, in MetaRocq.Erasure.EProgram]
TransformExt.compose [instance, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.env [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.env' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.env'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.eval'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.extends'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.term'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Comp.value'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt [section, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.env'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.eval'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.extends [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.extends' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.o [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.term'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.Opt.value'' [variable, in MetaRocq.Erasure.EProgram]
TransformExt.preserves_obs [projection, in MetaRocq.Erasure.EProgram]
TransformExt.preserves_obs [constructor, in MetaRocq.Erasure.EProgram]
TransformExt.t [record, in MetaRocq.Erasure.EProgram]
TransformExt.t [inductive, in MetaRocq.Erasure.EProgram]
transform_wellformed_decl' [lemma, in MetaRocq.Erasure.EImplementBox]
transform_wellformed' [lemma, in MetaRocq.Erasure.EImplementBox]
transform_erasure_pipeline_function' [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_erasure_pipeline_function [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_erase_pres_term [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambdabox_pres_term [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambda_box_eta_app [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_lambda_box_firstorder [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_compose_assoc [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
transform_blocks_eval [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wf_global [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_env_extends [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decl_extends [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_extends [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wellformed_decl [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_wellformed [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_declared_constant [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isLazyApp [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isPrimApp [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_isConstructApp [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_tApp [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_program [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_env [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decl [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_constant_decl [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_nth [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_cofix [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cunfold_fix [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_cofix_subst [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_fix_subst [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_iota_red [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_substl [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_csubst [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta_fn [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps_eta [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_decompose [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks_mkApps [lemma, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks [definition, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks.Def [section, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks.Σ [variable, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_blocks [section, in MetaRocq.Erasure.EConstructorsAsBlocks]
transform_compose [definition, in MetaRocq.ErasurePlugin.Erasure]
Transform.Comp [section, in MetaRocq.Common.Transform]
Transform.compose [definition, in MetaRocq.Common.Transform]
Transform.Comp.env [variable, in MetaRocq.Common.Transform]
Transform.Comp.env' [variable, in MetaRocq.Common.Transform]
Transform.Comp.env'' [variable, in MetaRocq.Common.Transform]
Transform.Comp.eval [variable, in MetaRocq.Common.Transform]
Transform.Comp.eval' [variable, in MetaRocq.Common.Transform]
Transform.Comp.eval'' [variable, in MetaRocq.Common.Transform]
Transform.Comp.term [variable, in MetaRocq.Common.Transform]
Transform.Comp.term' [variable, in MetaRocq.Common.Transform]
Transform.Comp.term'' [variable, in MetaRocq.Common.Transform]
Transform.Comp.value [variable, in MetaRocq.Common.Transform]
Transform.Comp.value' [variable, in MetaRocq.Common.Transform]
Transform.Comp.value'' [variable, in MetaRocq.Common.Transform]
Transform.correctness [projection, in MetaRocq.Common.Transform]
Transform.name [projection, in MetaRocq.Common.Transform]
Transform.obseq [projection, in MetaRocq.Common.Transform]
Transform.Opt [section, in MetaRocq.Common.Transform]
Transform.Opt.env [variable, in MetaRocq.Common.Transform]
Transform.Opt.env' [variable, in MetaRocq.Common.Transform]
Transform.Opt.eval [variable, in MetaRocq.Common.Transform]
Transform.Opt.eval' [variable, in MetaRocq.Common.Transform]
Transform.Opt.term [variable, in MetaRocq.Common.Transform]
Transform.Opt.term' [variable, in MetaRocq.Common.Transform]
Transform.Opt.value [variable, in MetaRocq.Common.Transform]
Transform.Opt.value' [variable, in MetaRocq.Common.Transform]
Transform.post [projection, in MetaRocq.Common.Transform]
Transform.pre [projection, in MetaRocq.Common.Transform]
Transform.preservation [projection, in MetaRocq.Common.Transform]
Transform.preserves_eval [definition, in MetaRocq.Common.Transform]
Transform.program [abbreviation, in MetaRocq.Common.Transform]
Transform.program [definition, in MetaRocq.Common.Transform]
Transform.program' [abbreviation, in MetaRocq.Common.Transform]
Transform.run [definition, in MetaRocq.Common.Transform]
Transform.self_transform [definition, in MetaRocq.Common.Transform]
Transform.t [record, in MetaRocq.Common.Transform]
Transform.transform [projection, in MetaRocq.Common.Transform]
_ ▷ _ (transform_scope) [notation, in MetaRocq.Common.Transform]
Translation [section, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
translation_utils [library]
Translation.Σ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
TransLookup [module, in MetaRocq.PCUIC.PCUICProgram]
TransLookup_lookup_inductive' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
TransLookup.lookup_inductive [definition, in MetaRocq.PCUIC.PCUICProgram]
TransLookup.lookup_minductive [definition, in MetaRocq.PCUIC.PCUICProgram]
transport [definition, in MetaRocq.Utils.MREquality]
transport_ws_term [definition, in MetaRocq.PCUIC.PCUICConfluence]
transport_on_free_vars [definition, in MetaRocq.PCUIC.PCUICConfluence]
trans_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICEquality]
trans_env_repr [projection, in MetaRocq.PCUIC.PCUICProgram]
trans_env_map [projection, in MetaRocq.PCUIC.PCUICProgram]
trans_env_env [projection, in MetaRocq.PCUIC.PCUICProgram]
trans_env [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_global_decl [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_mib [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_oib [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_ctors [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_cst [definition, in MetaRocq.Erasure.Typed.ExAst]
trans_lookup_projection [lemma, in MetaRocq.Erasure.ErasureProperties]
trans_lookup_constructor [lemma, in MetaRocq.Erasure.ErasureProperties]
trans_lookup_inductive [lemma, in MetaRocq.Erasure.ErasureProperties]
trans_lookup_constant [lemma, in MetaRocq.Erasure.ErasureProperties]
trans_lookups.g [variable, in MetaRocq.Erasure.ErasureProperties]
trans_lookups.Σ' [variable, in MetaRocq.Erasure.ErasureProperties]
trans_lookups.Σ [variable, in MetaRocq.Erasure.ErasureProperties]
trans_lookups [section, in MetaRocq.Erasure.ErasureProperties]
trans_template_program [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_env [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_decls [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global_decl [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_minductive_body [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_constant_body [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_one_ind_body [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_projection_body [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_constructor_body [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_local [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_decl [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_branch [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_predicate [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans_global [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_env [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_decls [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_global_decl [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_constant_body [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_minductive_body [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_one_ind_body [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_projection_body [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_constructor_body [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_cstr_concl [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_cstr_concl_head [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_local [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_decl [abbreviation, in MetaRocq.PCUIC.PCUICExpandLets]
trans_branch [definition, in MetaRocq.PCUIC.PCUICExpandLets]
trans_env_remove_match_on_box_env [lemma, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_env_fresh_globals [lemma, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_env_fresh_global [lemma, in MetaRocq.Erasure.Typed.OptimizePropDiscr]
trans_firstorder_ind [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_firstorder_env [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_firstorder_mutind [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_axiom_free [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ne_nf [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_case_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isFix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isRel [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isConstruct [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wcbveval [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_closedn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_csubst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_ext [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_udecl [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_projs [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_local_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel' [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec' [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv' [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul' [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul_ctx_rel [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_convSpec [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumulSpec [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_realargs [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destArity [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_concl_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ctx_inst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_subst_telescope [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_constraints [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_levels [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_prim_ty [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_telescope [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_arities_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_predicate [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_annots [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_type_of_constructor [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_branch_type [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_cofixpoint [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_fixpoint [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_rec_kind [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_cofix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_check_one_fix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_app [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destInd [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_nisApp [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isApp [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decompose_prod_assum [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mfix_All [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_branches [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local_env [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wf_local' [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cumul [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_conv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_leq_term [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_compare_term [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_term_upto_univ [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_upto_names [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_context_upto_names_eq_binder_annot [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cmp_global_instance [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_red1 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_untyped_subslet [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_closed_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_bbody [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_bcontext [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_eq_binder_annot [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_case_predicate_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder_name_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_set_binder [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_set_binder [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_predicate_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_reln [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inst_case_branch_context_gen [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_assumption_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context_inst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cstr_branch_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_extended_subst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_smash_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift_decl [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_decl [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_fix_context [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_is_constructor [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_cofix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_unfold_fix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_isLambda [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_nth [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_destr_arity [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_projection [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_inds [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_dbody [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_dtype [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_ind_type [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_cst_type [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_instance [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst10 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_subst [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_decl_type [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mkApps [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constructor [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_inductive [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_consistent_instance_ext [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_constraintSet_in [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_declared_constant [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lookup [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_in_level_set [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_mem_level_set [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_constraints [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_global_ext_levels [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_def [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_lift [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars_ctx [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_on_free_vars [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_local_app [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
trans_wcbvEval [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_cofix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cunfold_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_cofix_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_fix_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_substl [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_csubst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICWcbvEval]
trans_program [definition, in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
trans_env_erase_global_decls [lemma, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
trans_red [constructor, in MetaRocq.Template.Typing]
trans_ex_prog [definition, in MetaRocq.ErasurePlugin.ETransform]
trans_redl [constructor, in MetaRocq.PCUIC.PCUICReduction]
trans_red [lemma, in MetaRocq.PCUIC.PCUICReduction]
trans_eq_univ_prop [instance, in MetaRocq.PCUIC.PCUICCumulProp]
trans_mutual_inductive_entry [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_one_inductive_entry [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_env [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_decls [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_global_decl [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_minductive_body [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_constant_body [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_one_ind_body [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_projection_body [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_constructor_body [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_local [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_decl [abbreviation, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_branch [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_predicate [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_prim [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplate]
trans_env_debox [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
trans_subst_instance_decl [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_case_branch_type [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_it_mkLambda_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_cofixpoint [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_fixpoint [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_rec_kind [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_one_cofix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_check_one_fix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decompose_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_destInd [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_nisApp [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_isApp [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decompose_prod_assum [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mfix_All2 [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mfix_All [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_branches [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_local_env [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf_local' [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cumul [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_leq_term [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_term_upto_univ [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_context_gen_eq_binder_annot [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cmp_global_instance [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_red1 [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_bcontext [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_eq_binder_annot [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_case_predicate_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder_name_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_set_binder [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_set_binder [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_wf [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_predicate_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_to_extended_list [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_reln [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_inst_case_branch_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context_inst [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cstr_branch_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_inds [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_ctx [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_expand_lets_k [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_extended_subst [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_smash_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lift_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_fix_context [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_is_constructor [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_unfold_cofix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_unfold_fix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_isLambda [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_nth [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_it_mkProd_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mkProd_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_destr_arity [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_projection [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_dbody [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_dtype [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_type_of_constructor [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_ind_type [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_cst_type [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_instance_ctx [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst_instance [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst10 [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_subst [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_decl_type [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mkApps [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_constructor [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_inductive [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_consistent_instance_ext [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_constraintSet_in [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_declared_constant [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lookup [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_in_level_set [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_mem_level_set [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_global_ext_constraints [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_global_ext_levels [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_def [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_lift [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_local_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
trans_on_global_env [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext_gen [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_env_retroknowledge [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_env_universes [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_projs [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_ind_sorts [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_type_local_ctx [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_respects_variance [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_respects_variance [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_arities [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumul_ctx_rel [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_closedn [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_telescope [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_arities_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_env_retroknowledge [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_sort [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_branch_type [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec_typed [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumulSpec [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_consistent_instance_ext [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decl_universes [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_cofixpoint [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_fixpoint [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_rec_kind [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_one_cofix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_check_one_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decompose_prod_assum [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decompose_app [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_local_env [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_wf_local [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cumul_gen [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_red1 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ' [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_branch_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context_alpha [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_predicate_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_case_predicate_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_app [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_inst_case_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_is_constructor [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_unfold_cofix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_unfold_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_isLambda [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_iota_red [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cstr_branch_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_smash_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_ctx [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lift_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_context [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_expand_lets_k [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_extended_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_nth [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global [section, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term_list [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_leq_term [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_eq_term_upto_univ [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_cmp_global_instance [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ' [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global [section, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ' [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.wfΣ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.Σ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global.cf [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
Trans_Global [section, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_to_extended_list [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_reln [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_npars [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_params_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_bodies [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_params [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_subst_instance [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_it_mkLambda_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_it_mkProd_or_LetIn [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_inds [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_destArity [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst_instance [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_subst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_mkApps [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_mkApp [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lift [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decl [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decl_weaken [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_ind_body_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_local_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_decl_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_weakening [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_env [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_decls_app [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_inductive [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_lookup_minductive [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
trans_global_env_cons [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
trans_expanded [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICExpanded]
trans_template_program_wt [lemma, in MetaRocq.TemplatePCUIC.PCUICTransform]
trans_program_expanded [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_program_wf [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_program [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_wf [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_decl_wf [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed_decl_irrel [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed_irrel [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_wellformed [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_expanded [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_eq [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env_extends' [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_decl_irrel [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_decl [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded_irrel [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_expanded [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_correct [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env' [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_env [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_decl [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_constant_decl [definition, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_nth [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_cunfold_fix [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_fix_subst [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_iota_red [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_substl [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_csubst [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
trans_mkApps [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
Trans.Σ [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
trans.Σ [variable, in MetaRocq.Erasure.ECoInductiveToInductive]
TraverseWithBinders [section, in MetaRocq.Template.AstUtils]
TraverseWithBindersM [section, in MetaRocq.Template.AstUtils]
TraverseWithBindersM.a [variable, in MetaRocq.Template.AstUtils]
TraverseWithBindersM.A [variable, in MetaRocq.Template.AstUtils]
TraverseWithBindersM.Acc [variable, in MetaRocq.Template.AstUtils]
TraverseWithBindersM.liftM [variable, in MetaRocq.Template.AstUtils]
TraverseWithBindersM.M [variable, in MetaRocq.Template.AstUtils]
TraverseWithBinders.a [variable, in MetaRocq.Template.AstUtils]
TraverseWithBinders.A [variable, in MetaRocq.Template.AstUtils]
TraverseWithBinders.Acc [variable, in MetaRocq.Template.AstUtils]
TraverseWithBinders.lift [variable, in MetaRocq.Template.AstUtils]
traverse_env [definition, in MetaRocq.Erasure.Typed.Certifying]
Tree [module, in MetaRocq.Utils.bytestring]
Tree.append [constructor, in MetaRocq.Utils.bytestring]
Tree.concat [definition, in MetaRocq.Utils.bytestring]
Tree.parens [definition, in MetaRocq.Utils.bytestring]
Tree.print_list [definition, in MetaRocq.Utils.bytestring]
Tree.string [constructor, in MetaRocq.Utils.bytestring]
Tree.string_of_list [definition, in MetaRocq.Utils.bytestring]
Tree.string_of_list_aux [definition, in MetaRocq.Utils.bytestring]
Tree.t [inductive, in MetaRocq.Utils.bytestring]
Tree.to_string [definition, in MetaRocq.Utils.bytestring]
Tree.to_string_acc [definition, in MetaRocq.Utils.bytestring]
Tree.to_rev_list_aux [definition, in MetaRocq.Utils.bytestring]
Tree.t_sind [definition, in MetaRocq.Utils.bytestring]
Tree.t_rec [definition, in MetaRocq.Utils.bytestring]
Tree.t_ind [definition, in MetaRocq.Utils.bytestring]
Tree.t_rect [definition, in MetaRocq.Utils.bytestring]
_ ++ _ [notation, in MetaRocq.Utils.bytestring]
tRel [constructor, in MetaRocq.PCUIC.PCUICAst]
tRel [constructor, in MetaRocq.Erasure.EAst]
tRel [constructor, in MetaRocq.Template.Ast]
tRel_kind_sind [definition, in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_rec [definition, in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_ind [definition, in MetaRocq.Erasure.Typed.Erasure]
tRel_kind_rect [definition, in MetaRocq.Erasure.Typed.Erasure]
tRel_kind [inductive, in MetaRocq.Erasure.Typed.Erasure]
Trel_sig [abbreviation, in MetaRocq.Utils.MRRelations]
Trel_conj [abbreviation, in MetaRocq.Utils.MRRelations]
triangle [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
triangle_gen [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
trim_ind_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
trim_mib_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
trim_ctor_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
trim_const_masks [definition, in MetaRocq.Erasure.Typed.Optimize]
trim_end [definition, in MetaRocq.Erasure.Typed.Optimize]
trim_start [definition, in MetaRocq.Erasure.Typed.Optimize]
trivial_hyp [definition, in MetaRocq.Examples.tauto]
True_FinitelyListablePackage [instance, in MetaRocq.Utils.MRListable]
trust_inline_transformation_ext' [axiom, in MetaRocq.Erasure.EInlining]
trust_inline_transformation_ext [axiom, in MetaRocq.Erasure.EInlining]
trust_inlining_pres [axiom, in MetaRocq.Erasure.EInlining]
trust_inlining_wf [axiom, in MetaRocq.Erasure.EInlining]
trust_betared_pres [axiom, in MetaRocq.Erasure.EBeta]
trust_betared_wf [axiom, in MetaRocq.Erasure.EBeta]
trust_unbox_transformation_ext' [axiom, in MetaRocq.ErasurePlugin.ETransform]
trust_unbox_transformation_ext [axiom, in MetaRocq.ErasurePlugin.ETransform]
trust_unboxing_pres [axiom, in MetaRocq.ErasurePlugin.ETransform]
trust_unboxing_wf [axiom, in MetaRocq.ErasurePlugin.ETransform]
trust_cofix [axiom, in MetaRocq.Erasure.ECoInductiveToInductive]
try_remove_n_lambdas [definition, in MetaRocq.Examples.add_constructor]
try_reduce [definition, in MetaRocq.Template.Checker]
trΣ [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
tsize [definition, in MetaRocq.Examples.tauto]
tsize_downlift_le [lemma, in MetaRocq.Examples.tauto]
tsize_downlift [lemma, in MetaRocq.Examples.tauto]
tsize_lift [lemma, in MetaRocq.Examples.tauto]
tsize_decompose_app [lemma, in MetaRocq.Examples.tauto]
tsize_nonzero [lemma, in MetaRocq.Examples.tauto]
TslIdent [record, in MetaRocq.Examples.add_constructor]
tsl_constructor_body [definition, in MetaRocq.Examples.add_constructor]
tsl_ident [projection, in MetaRocq.Examples.add_constructor]
tSort [constructor, in MetaRocq.PCUIC.PCUICAst]
tSort [constructor, in MetaRocq.Template.Ast]
tString [abbreviation, in MetaRocq.PCUIC.PCUICAst]
tString [constructor, in MetaRocq.Template.Ast]
TT [module, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TT [module, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
TTconv [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TTconv [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Tterm [abbreviation, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
TTwf_local [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
TTwf_local [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
TTy_wf_local [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
TT_typing_spine_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
TVar [constructor, in MetaRocq.Erasure.Typed.ExAst]
tVar [constructor, in MetaRocq.PCUIC.PCUICAst]
tVar [constructor, in MetaRocq.Erasure.EAst]
tVar [constructor, in MetaRocq.Template.Ast]
tvar_is_sort [projection, in MetaRocq.Erasure.Typed.ExAst]
tvar_is_arity [projection, in MetaRocq.Erasure.Typed.ExAst]
tvar_is_logical [projection, in MetaRocq.Erasure.Typed.ExAst]
tvar_name [projection, in MetaRocq.Erasure.Typed.ExAst]
tybranches [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
tybranches [definition, in MetaRocq.PCUIC.PCUICTyping]
Typ [abbreviation, in MetaRocq.Common.BasicAst]
TypeAliasDecl [constructor, in MetaRocq.Erasure.Typed.ExAst]
TypeAnnotations [library]
Typecheck [section, in MetaRocq.Template.Checker]
Typecheck [section, in MetaRocq.Template.Checker]
Typecheck [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
typechecking [definition, in MetaRocq.Template.Checker]
typecheck_program [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
typecheck_program [definition, in MetaRocq.Template.Checker]
typecheck_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
Typecheck.cf [variable, in MetaRocq.Template.Checker]
Typecheck.cf [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.wfΓ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.Γ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive.infer [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_primitive [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.wfΓ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.Γ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix.infer [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_mfix [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.hpctx [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ptm [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfpret [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.predctx [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfp [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.hty [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.isdecl [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.args [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.p [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.idecl [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.mdecl [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ci [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.ps [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.wfΓ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.Γ [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs.infer [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.check_brs [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.F [variable, in MetaRocq.Template.Checker]
Typecheck.F [variable, in MetaRocq.Template.Checker]
Typecheck.G [variable, in MetaRocq.Template.Checker]
Typecheck.InferAux [section, in MetaRocq.Template.Checker]
Typecheck.InferAux [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.InferAux.infer [variable, in MetaRocq.Template.Checker]
Typecheck.InferAux.infer [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.f [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.B [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All.A [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.make_All [section, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.nor [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.normalization_in [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.X [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.X_type [variable, in MetaRocq.SafeChecker.PCUICTypeChecker]
_ ;; _ [notation, in MetaRocq.SafeChecker.PCUICTypeChecker]
_ <- _ ;; _ [notation, in MetaRocq.SafeChecker.PCUICTypeChecker]
Typecheck.Σ [variable, in MetaRocq.Template.Checker]
Typecheck.Σ [variable, in MetaRocq.Template.Checker]
typed_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
typed_term [record, in MetaRocq.Template.TemplateMonad.Common]
typed_erase_transform [definition, in MetaRocq.ErasurePlugin.ETransform]
typed_erasure_pre [definition, in MetaRocq.ErasurePlugin.ETransform]
typed_erase_and_print_template_program [definition, in MetaRocq.ErasurePlugin.Erasure]
typed_erasure_config [definition, in MetaRocq.ErasurePlugin.Erasure]
typed_erasure_pipeline [definition, in MetaRocq.ErasurePlugin.Erasure]
typed_erase_transform_mapping [definition, in MetaRocq.ErasurePlugin.Erasure]
typed_subst_abstract_instance [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
typed_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
TypeError [constructor, in MetaRocq.SafeChecker.PCUICErrors]
TypeError [constructor, in MetaRocq.Template.Checker]
TypeError_comp [constructor, in MetaRocq.SafeChecker.PCUICErrors]
TypeInstance [definition, in MetaRocq.Template.TemplateMonad.Core]
TypeInstance [definition, in MetaRocq.Template.TemplateMonad.Extractable]
TypeInstanceOptimized [definition, in MetaRocq.Template.TemplateMonad.Core]
TypeInstanceUnoptimized [definition, in MetaRocq.Template.TemplateMonad.Core]
TypeOf [section, in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.cf [variable, in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.nor [variable, in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.normalization_in [variable, in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.X [variable, in MetaRocq.SafeChecker.PCUICSafeRetyping]
TypeOf.X_type [variable, in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_var_info_of_flag [definition, in MetaRocq.Erasure.Typed.Erasure]
type_flag [record, in MetaRocq.Erasure.Typed.Erasure]
type_local_ctx_Pclosed [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
type_local_ctx_All_local_env [lemma, in MetaRocq.PCUIC.Conversion.PCUICClosedConv]
type_reduction_closed [lemma, in MetaRocq.PCUIC.PCUICSR]
type_reduction [lemma, in MetaRocq.PCUIC.PCUICSR]
type_Cumul_alt [lemma, in MetaRocq.PCUIC.PCUICSR]
type_in_type [instance, in MetaRocq.Common.config]
type_it_mkLambda_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICGeneration]
type_mkApps [lemma, in MetaRocq.PCUIC.PCUICGeneration]
type_spine_cons [constructor, in MetaRocq.PCUIC.PCUICGeneration]
type_spine_nil [constructor, in MetaRocq.PCUIC.PCUICGeneration]
type_mkApps [lemma, in MetaRocq.PCUIC.PCUICSpine]
type_it_mkProd_or_LetIn_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
type_var_info [record, in MetaRocq.Erasure.Typed.ExAst]
type_Cumul' [lemma, in MetaRocq.PCUIC.PCUICTyping]
type_Prop [lemma, in MetaRocq.PCUIC.PCUICTyping]
type_Prop_wf [lemma, in MetaRocq.PCUIC.PCUICTyping]
type_Cumul [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Prim [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_CoFix [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Fix [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Proj [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Case [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Construct [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Ind [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Const [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_App [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_LetIn [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Lambda [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Prod [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Sort [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_Rel [constructor, in MetaRocq.PCUIC.PCUICTyping]
type_of_constructor [definition, in MetaRocq.PCUIC.PCUICTyping]
type_closed_subst [lemma, in MetaRocq.Erasure.ErasureProperties]
type_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
type_of_impl [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
type_flag_to_tRel_kind [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
type_error_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
type_error_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
type_error_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
type_error_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
type_error [inductive, in MetaRocq.SafeChecker.PCUICErrors]
type_of_subtype [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_of_typing [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_of [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
type_mkApps_arity [lemma, in MetaRocq.PCUIC.PCUICValidity]
type_App' [lemma, in MetaRocq.PCUIC.PCUICValidity]
type_ctx_wf_univ [lemma, in MetaRocq.PCUIC.PCUICValidity]
type_ctx [abbreviation, in MetaRocq.PCUIC.PCUICValidity]
type_it_mkProd_or_LetIn_smash_middle [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
type_mkApps_napp [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
type_tCoFix_inv [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
type_tFix_inv [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
type_it_mkProd_or_LetIn_sorts [lemma, in MetaRocq.PCUIC.PCUICArities]
type_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICArities]
type_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICArities]
type_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICArities]
type_spine_cons [constructor, in MetaRocq.PCUIC.PCUICArities]
type_spine_nil [constructor, in MetaRocq.PCUIC.PCUICArities]
type_local_ctx_instantiate [lemma, in MetaRocq.PCUIC.PCUICContexts]
type_local_ctx_wf_local [lemma, in MetaRocq.PCUIC.PCUICContexts]
type_smash [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
type_spine_pred_cons [constructor, in MetaRocq.PCUIC.PCUICProgress]
type_spine_pred_nil [constructor, in MetaRocq.PCUIC.PCUICProgress]
type_Prop_wf [lemma, in MetaRocq.Template.Typing]
type_Prop [lemma, in MetaRocq.Template.Typing]
type_spine_cons [constructor, in MetaRocq.Template.Typing]
type_spine_nil [constructor, in MetaRocq.Template.Typing]
type_Conv [constructor, in MetaRocq.Template.Typing]
type_Array [constructor, in MetaRocq.Template.Typing]
type_String [constructor, in MetaRocq.Template.Typing]
type_Float [constructor, in MetaRocq.Template.Typing]
type_Int [constructor, in MetaRocq.Template.Typing]
type_CoFix [constructor, in MetaRocq.Template.Typing]
type_Fix [constructor, in MetaRocq.Template.Typing]
type_Proj [constructor, in MetaRocq.Template.Typing]
type_Case [constructor, in MetaRocq.Template.Typing]
type_Construct [constructor, in MetaRocq.Template.Typing]
type_Ind [constructor, in MetaRocq.Template.Typing]
type_Const [constructor, in MetaRocq.Template.Typing]
type_App [constructor, in MetaRocq.Template.Typing]
type_LetIn [constructor, in MetaRocq.Template.Typing]
type_Lambda [constructor, in MetaRocq.Template.Typing]
type_Prod [constructor, in MetaRocq.Template.Typing]
type_Cast [constructor, in MetaRocq.Template.Typing]
type_Sort [constructor, in MetaRocq.Template.Typing]
type_Rel [constructor, in MetaRocq.Template.Typing]
type_of_constructor [definition, in MetaRocq.Template.Typing]
type_error_sind [definition, in MetaRocq.Template.Checker]
type_error_rec [definition, in MetaRocq.Template.Checker]
type_error_ind [definition, in MetaRocq.Template.Checker]
type_error_rect [definition, in MetaRocq.Template.Checker]
type_error [inductive, in MetaRocq.Template.Checker]
type_local_ctx_wf [lemma, in MetaRocq.PCUIC.PCUICInductives]
type_local_ctx_cum [lemma, in MetaRocq.PCUIC.PCUICInductives]
type_mkApps_tConstruct_n_conv_arity [lemma, in MetaRocq.Erasure.EArities]
type_local_ctx_wf [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
type_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_spine_cons [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_spine_nil [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_spine_eq [constructor, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_mkApps_napp [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
type_is_open_term [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
type_closed [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
type_Case_simple_subst_helper [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
type_Case_subst_helper [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
type_Case_helper [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
typing [inductive, in MetaRocq.PCUIC.PCUICTyping]
Typing [module, in MetaRocq.Common.EnvironmentTyping]
typing [inductive, in MetaRocq.Template.Typing]
Typing [library]
TypingWf [section, in MetaRocq.Template.TypingWf]
TypingWf [library]
TypingWf.cf [variable, in MetaRocq.Template.TypingWf]
typing_renaming_cond_P [lemma, in MetaRocq.PCUIC.Bidirectional.BDStrengthening]
typing_closed_red [lemma, in MetaRocq.PCUIC.PCUICSR]
typing_closed_red1 [lemma, in MetaRocq.PCUIC.PCUICSR]
typing_spine_eval [lemma, in MetaRocq.Erasure.Prelim]
typing_spine_wt [lemma, in MetaRocq.Erasure.Prelim]
typing_spine_inv [lemma, in MetaRocq.Erasure.Prelim]
typing_sum_size [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_sind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_rec [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_ind [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum_rect [definition, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_sum [inductive, in MetaRocq.PCUIC.Bidirectional.BDTyping]
typing_spine_proofs [lemma, in MetaRocq.PCUIC.PCUICElimination]
typing_spine_it_mkProd_or_LetIn_full_inv [lemma, in MetaRocq.PCUIC.PCUICElimination]
typing_spine_case_predicate [lemma, in MetaRocq.PCUIC.PCUICElimination]
typing_spine_sind [definition, in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_rec [definition, in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_ind [definition, in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_rect [definition, in MetaRocq.PCUIC.PCUICGeneration]
typing_spine [inductive, in MetaRocq.PCUIC.PCUICGeneration]
typing_spine_ctx_inst_smash [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_nth_error [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_app [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_ctx_inst [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_inv [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_wf_local [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_close_make_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn' [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_it_mkProd_or_LetIn_gen [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_refl [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_strengthen [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_eq [lemma, in MetaRocq.PCUIC.PCUICSpine]
typing_spine_arity_spine [lemma, in MetaRocq.PCUIC.PCUICFirstorder]
typing_ind_env [lemma, in MetaRocq.PCUIC.PCUICTyping]
typing_ind_env_app_size [lemma, in MetaRocq.PCUIC.PCUICTyping]
typing_wf_local_size [lemma, in MetaRocq.PCUIC.PCUICTyping]
typing_wf_local [lemma, in MetaRocq.PCUIC.PCUICTyping]
typing_size_pos [lemma, in MetaRocq.PCUIC.PCUICTyping]
typing_size [definition, in MetaRocq.PCUIC.PCUICTyping]
typing_sind [definition, in MetaRocq.PCUIC.PCUICTyping]
typing_rec [definition, in MetaRocq.PCUIC.PCUICTyping]
typing_ind [definition, in MetaRocq.PCUIC.PCUICTyping]
typing_rect [definition, in MetaRocq.PCUIC.PCUICTyping]
typing_wellformed [lemma, in MetaRocq.Erasure.ErasureProperties]
typing_inst [lemma, in MetaRocq.PCUIC.Typing.PCUICInstTyp]
typing_monad [instance, in MetaRocq.SafeChecker.PCUICErrors]
typing_error_forget [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_comp [inductive, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_sind [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_rec [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_ind [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result_rect [definition, in MetaRocq.SafeChecker.PCUICErrors]
typing_result [inductive, in MetaRocq.SafeChecker.PCUICErrors]
typing_rename [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_P [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_rename_prop [lemma, in MetaRocq.PCUIC.Typing.PCUICRenameTyp]
typing_wf_fixpoint [lemma, in MetaRocq.Template.EtaExpand]
typing_spine_wt [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
typing_subst_instance_decl [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_ctx [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance'' [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance_wf_local [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance' [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_subst_instance [lemma, in MetaRocq.PCUIC.Typing.PCUICUnivSubstitutionTyp]
typing_spine_to_extended_list_k_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
typing_spine_to_extended_list_app [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
typing_spine_isType_dom [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_WAT_concl [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_prod [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_weaken_concl [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_letin [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_letin_inv [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_isType_codom [lemma, in MetaRocq.PCUIC.PCUICArities]
typing_spine_sind [definition, in MetaRocq.PCUIC.PCUICArities]
typing_spine_rec [definition, in MetaRocq.PCUIC.PCUICArities]
typing_spine_ind [definition, in MetaRocq.PCUIC.PCUICArities]
typing_spine_rect [definition, in MetaRocq.PCUIC.PCUICArities]
typing_spine [inductive, in MetaRocq.PCUIC.PCUICArities]
typing_alpha [lemma, in MetaRocq.PCUIC.PCUICAlpha]
typing_alpha_prop [lemma, in MetaRocq.PCUIC.PCUICAlpha]
typing_spine_isArity [lemma, in MetaRocq.ErasurePlugin.ErasureCorrectness]
typing_expand_lets [lemma, in MetaRocq.PCUIC.PCUICContexts]
typing_spine_it_mkProd_or_LetIn_ext_list_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_ext_list_inv_gen [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_prod_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_letin_inv' [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_spine_it_mkProd_or_LetIn_inv [lemma, in MetaRocq.SafeChecker.PCUICSafeChecker]
typing_value_head [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_value_head_napp [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_prim_type [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_axiom [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_sort [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_constructor_arity [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_constructor_arity_exact [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_length [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env_app_size [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_strengthen [lemma, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_sind [definition, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_rec [definition, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_ind [definition, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred_rect [definition, in MetaRocq.PCUIC.PCUICProgress]
typing_spine_pred [inductive, in MetaRocq.PCUIC.PCUICProgress]
typing_ind_env [lemma, in MetaRocq.Template.Typing]
typing_wf_local_size [lemma, in MetaRocq.Template.Typing]
typing_wf_local [lemma, in MetaRocq.Template.Typing]
typing_size_pos [lemma, in MetaRocq.Template.Typing]
typing_size [definition, in MetaRocq.Template.Typing]
typing_spine_size [definition, in MetaRocq.Template.Typing]
Typing_Spine_size.Γ [variable, in MetaRocq.Template.Typing]
Typing_Spine_size.Σ [variable, in MetaRocq.Template.Typing]
Typing_Spine_size.fn [variable, in MetaRocq.Template.Typing]
Typing_Spine_size [section, in MetaRocq.Template.Typing]
typing_spine_sind [definition, in MetaRocq.Template.Typing]
typing_spine_rec [definition, in MetaRocq.Template.Typing]
typing_spine_ind [definition, in MetaRocq.Template.Typing]
typing_spine_rect [definition, in MetaRocq.Template.Typing]
typing_sind [definition, in MetaRocq.Template.Typing]
typing_rec [definition, in MetaRocq.Template.Typing]
typing_ind [definition, in MetaRocq.Template.Typing]
typing_rect [definition, in MetaRocq.Template.Typing]
typing_spine [inductive, in MetaRocq.Template.Typing]
typing_ws_cumul_pb [lemma, in MetaRocq.PCUIC.PCUICInversion]
typing_closed_ctx [lemma, in MetaRocq.PCUIC.PCUICInversion]
typing_monad [instance, in MetaRocq.Template.Checker]
typing_result_sind [definition, in MetaRocq.Template.Checker]
typing_result_rec [definition, in MetaRocq.Template.Checker]
typing_result_ind [definition, in MetaRocq.Template.Checker]
typing_result_rect [definition, in MetaRocq.Template.Checker]
typing_result [inductive, in MetaRocq.Template.Checker]
typing_infer_ind [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infer_prod [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering_sort [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_checking [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_infering [lemma, in MetaRocq.PCUIC.Bidirectional.BDFromPCUIC]
typing_expand_lets_gen [lemma, in MetaRocq.PCUIC.PCUICInductives]
typing_spine_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICInductives]
typing_cumul_term_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
typing_leq_term_prop [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
typing_leq_term_prop_gen [lemma, in MetaRocq.PCUIC.PCUICCumulProp]
typing_wf [lemma, in MetaRocq.Template.TypingWf]
typing_wf_sigma [lemma, in MetaRocq.Template.TypingWf]
typing_all_wf_decl [lemma, in MetaRocq.Template.TypingWf]
typing_wf_gen [lemma, in MetaRocq.Template.TypingWf]
typing_cofix_coind [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_evar [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_var [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error_None_prod [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error_None [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_more_inv [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_all_inv [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_nth_error [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_smash [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_arity_mkApps_Ind [lemma, in MetaRocq.PCUIC.PCUICClassification]
typing_spine_inj [lemma, in MetaRocq.Erasure.EArities]
typing_spine_wat [lemma, in MetaRocq.Erasure.EArities]
typing_spine_Is_conv_to_Arity [lemma, in MetaRocq.Erasure.EArities]
typing_spine_mkApps_Ind_ex [lemma, in MetaRocq.Erasure.EArities]
typing_spine_red [lemma, in MetaRocq.Erasure.EArities]
typing_wf_sort [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
typing_wf_universes [lemma, in MetaRocq.PCUIC.PCUICWfUniverses]
typing_eq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
typing_leq_term [lemma, in MetaRocq.PCUIC.PCUICPrincipality]
typing_spine_app [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl_size [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_weaken_concl [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_size [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Typing_Spine_size.Γ [variable, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Typing_Spine_size.Σ [variable, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
Typing_Spine_size [section, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_sind [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_rec [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_ind [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine_rect [definition, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_spine [inductive, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
typing_wf_wf [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
typing_closed_context [lemma, in MetaRocq.PCUIC.Typing.PCUICClosedTyp]
typing_correctness [library]
Typing.typing [axiom, in MetaRocq.Common.EnvironmentTyping]
Typing.wf_local [abbreviation, in MetaRocq.Common.EnvironmentTyping]
_ ;;; _ |- _ : _ (type_scope) [notation, in MetaRocq.Common.EnvironmentTyping]
TypUniv [abbreviation, in MetaRocq.Common.BasicAst]
typwt [lemma, in MetaRocq.Erasure.Typed.Erasure]
tywt [lemma, in MetaRocq.Erasure.Typed.Erasure]
t_ne [projection, in MetaRocq.Common.Universes]
t_set [projection, in MetaRocq.Common.Universes]
T_sind [definition, in MetaRocq.Examples.demo]
T_rec [definition, in MetaRocq.Examples.demo]
T_ind [definition, in MetaRocq.Examples.demo]
T_rect [definition, in MetaRocq.Examples.demo]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19204 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (228 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (298 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1273 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (313 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8163 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1514 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (52 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (534 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (727 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (402 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (333 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4833 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (182 entries) |