| 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) |
D (definition)
d [in MetaRocq.Examples.demo]dapp_r [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dapp_l [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dcase_c [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dcase_preturn [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dearg [in MetaRocq.Erasure.Typed.Optimize]
dearg [in MetaRocq.ErasurePlugin.ETransform]
dearged_proj_arg [in MetaRocq.Erasure.Typed.Optimize]
dearged_npars [in MetaRocq.Erasure.Typed.Optimize]
dearged_ctor_arity [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearging_transform [in MetaRocq.ErasurePlugin.ETransform]
dearging_checks_transform [in MetaRocq.ErasurePlugin.ETransform]
dearging_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
dearging_checks_transform_mapping [in MetaRocq.ErasurePlugin.Erasure]
dearg_transform [in MetaRocq.Erasure.Typed.Optimize]
dearg_single_bt [in MetaRocq.Erasure.Typed.Optimize]
dearg_env [in MetaRocq.Erasure.Typed.Optimize]
dearg_decl [in MetaRocq.Erasure.Typed.Optimize]
dearg_mib [in MetaRocq.Erasure.Typed.Optimize]
dearg_oib [in MetaRocq.Erasure.Typed.Optimize]
dearg_ctor [in MetaRocq.Erasure.Typed.Optimize]
dearg_cst [in MetaRocq.Erasure.Typed.Optimize]
dearg_cst_type_top [in MetaRocq.Erasure.Typed.Optimize]
dearg_aux [in MetaRocq.Erasure.Typed.Optimize]
dearg_proj [in MetaRocq.Erasure.Typed.Optimize]
dearg_case [in MetaRocq.Erasure.Typed.Optimize]
dearg_case_branches [in MetaRocq.Erasure.Typed.Optimize]
dearg_case_branch [in MetaRocq.Erasure.Typed.Optimize]
dearg_branch_body [in MetaRocq.Erasure.Typed.Optimize]
dearg_branch_body_rec [in MetaRocq.Erasure.Typed.Optimize]
dearg_lambdas [in MetaRocq.Erasure.Typed.Optimize]
dearg_single [in MetaRocq.Erasure.Typed.Optimize]
dearg_term [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_env [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_sind [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_rec [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_ind [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
dearg_spec_rect [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
debox_env_types [in MetaRocq.Erasure.Typed.Optimize]
debox_type_decl [in MetaRocq.Erasure.Typed.Optimize]
debox_type_mib [in MetaRocq.Erasure.Typed.Optimize]
debox_type_oib [in MetaRocq.Erasure.Typed.Optimize]
debox_type_constant [in MetaRocq.Erasure.Typed.Optimize]
debox_box_type [in MetaRocq.Erasure.Typed.Optimize]
debox_box_type_aux [in MetaRocq.Erasure.Typed.Optimize]
DeclarationTyping.Forall_decls_typing [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.isType [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.type_local_decl [in MetaRocq.Common.EnvironmentTyping]
DeclarationTyping.wf_local_rel [in MetaRocq.Common.EnvironmentTyping]
declared [in MetaRocq.Common.uGraph]
declared_cstr_levels [in MetaRocq.Common.Universes]
declared_projection_constructor' [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_constructor_inductive' [in MetaRocq.PCUIC.PCUICGlobalEnv]
declared_kn [in MetaRocq.Erasure.ErasureFunctionProperties]
declared_projection [in MetaRocq.Erasure.EGlobalEnv]
declared_constructor [in MetaRocq.Erasure.EGlobalEnv]
declared_inductive [in MetaRocq.Erasure.EGlobalEnv]
declared_minductive [in MetaRocq.Erasure.EGlobalEnv]
declared_constant [in MetaRocq.Erasure.EGlobalEnv]
declare_and_uniquify_and_combine_levels [in MetaRocq.Common.UniversesDec]
declare_and_uniquify_levels [in MetaRocq.Common.UniversesDec]
decls_prefix [in MetaRocq.Erasure.ErasureFunctionProperties]
decl_deps [in MetaRocq.Erasure.Typed.Erasure]
decl_size [in MetaRocq.Examples.tauto]
decl_closed [in MetaRocq.Erasure.Typed.ClosedAux]
decl_size [in MetaRocq.PCUIC.utils.PCUICSize]
decl_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
decompose_stack_at [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_stack [in MetaRocq.PCUIC.Syntax.PCUICPosition]
decompose_prod_assum_graph_sind [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_rec [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_ind [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_prod_assum_graph_rect [in MetaRocq.PCUIC.PCUICSubstitution]
decompose_lam [in MetaRocq.Template.Pretty]
decompose_arr [in MetaRocq.Erasure.Typed.ExAst]
decompose_lam_n_assum [in MetaRocq.Template.AstUtils]
decompose_prod_n_assum [in MetaRocq.Template.AstUtils]
decompose_prod_assum [in MetaRocq.Template.AstUtils]
decompose_prod [in MetaRocq.Template.AstUtils]
decompose_app [in MetaRocq.Template.AstUtils]
decompose_TArr [in MetaRocq.Erasure.Typed.Optimize]
decompose_prod_n_assum [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod_assum [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_prod [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_app_rec [in MetaRocq.PCUIC.utils.PCUICAstUtils]
decompose_lam [in MetaRocq.PCUIC.utils.PCUICPretty]
decompose_lam [in MetaRocq.Erasure.Typed.CertifyingBeta]
decompose_cstr_concl [in MetaRocq.SafeChecker.PCUICSafeChecker]
decompose_lam [in MetaRocq.Erasure.EPretty]
decompose_body_masked [in MetaRocq.Erasure.Typed.OptimizeCorrectness]
decompose_app [in MetaRocq.Erasure.EAstUtils]
decompose_app_rec [in MetaRocq.Erasure.EAstUtils]
decomp_step [in MetaRocq.Examples.tauto]
dedup_grefs [in MetaRocq.Quotation.CommonUtils]
dedup_grefs' [in MetaRocq.Quotation.CommonUtils]
default_relevance [in MetaRocq.Template.AstUtils]
default_sort_family [in MetaRocq.Template.AstUtils]
default_inductive_quotation_of [in MetaRocq.Quotation.ToPCUIC.Init]
default_inductive_quotation_of [in MetaRocq.Quotation.ToTemplate.Init]
default_wcbv_flags [in MetaRocq.Erasure.EWcbvEval]
default_erasure_config [in MetaRocq.ErasurePlugin.Erasure]
default_unsafe_passes [in MetaRocq.ErasurePlugin.Erasure]
default_dearging_config [in MetaRocq.ErasurePlugin.Erasure]
default_fuel [in MetaRocq.Template.Checker]
def_sig [in MetaRocq.PCUIC.Syntax.PCUICPosition]
def_size [in MetaRocq.Examples.tauto]
def_size [in MetaRocq.PCUIC.utils.PCUICSize]
def_depth_gen [in MetaRocq.PCUIC.Syntax.PCUICDepth]
depth [in MetaRocq.PCUIC.Syntax.PCUICDepth]
deriv_length [in MetaRocq.Erasure.Typed.WcbvEvalAux]
destArity [in MetaRocq.PCUIC.PCUICAst]
destArity [in MetaRocq.Template.Ast]
destInd [in MetaRocq.Template.AstUtils]
destInd [in MetaRocq.PCUIC.PCUICTyping]
destInd [in MetaRocq.Template.Typing]
diamond [in MetaRocq.PCUIC.PCUICConfluence]
dirpath [in MetaRocq.Common.Kernames]
disable_box_term_flags [in MetaRocq.Erasure.EImplementBox]
disable_prop_cases [in MetaRocq.Erasure.EWcbvEval]
disable_prop_cases [in MetaRocq.Erasure.EInlineProjections]
disable_projections_env_flag [in MetaRocq.Erasure.EInlineProjections]
disable_projections_term_flags [in MetaRocq.Erasure.EInlineProjections]
discr_construct0_cofix [in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct_cofix [in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct [in MetaRocq.SafeChecker.PCUICSafeReduce]
discr_construct [in MetaRocq.Erasure.EEtaExpanded]
discr_expanded_head [in MetaRocq.Erasure.EEtaExpandedFix]
discr_construct0_cofix [in MetaRocq.PCUIC.Syntax.PCUICViews]
discr_construct_cofix [in MetaRocq.PCUIC.Syntax.PCUICViews]
discr_prod_letin [in MetaRocq.SafeChecker.PCUICSafeChecker]
dlam_tm [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlam_ty [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_in [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_ty [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlet_bd [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dlexmod_sind [in MetaRocq.PCUIC.utils.PCUICUtils]
dlexmod_ind [in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_sind [in MetaRocq.PCUIC.utils.PCUICUtils]
dlexprod_ind [in MetaRocq.PCUIC.utils.PCUICUtils]
do_check_ind_sorts [in MetaRocq.SafeChecker.PCUICSafeChecker]
dprod_r [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dprod_l [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dproj_c [in MetaRocq.PCUIC.Syntax.PCUICPosition]
dummy_branch [in MetaRocq.PCUIC.utils.PCUICOnOne]
dummy_decl [in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
dummy_branch [in MetaRocq.Template.Typing]
dupfree [in MetaRocq.Erasure.EWcbvEvalNamed]
| 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) |