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)

---

M

MakeGraph [section, in MetaRocq.Common.uGraph]
MakeGraph.ctrs [variable, in MetaRocq.Common.uGraph]
MakeGraph.G [variable, in MetaRocq.Common.uGraph]
MakeGraph.Huctx [variable, in MetaRocq.Common.uGraph]
MakeGraph.uctx [variable, in MetaRocq.Common.uGraph]
make_context_subst_context_assumptions [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_spec_inv [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_recP [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_spec [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst_rec_spec [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
make_context_subst [definition, in MetaRocq.PCUIC.PCUICContextSubst]
make_template_program_env [definition, in MetaRocq.Template.TemplateProgram]
make_context_subst_length [lemma, in MetaRocq.PCUIC.PCUICSpine]
make_context_subst_tele [lemma, in MetaRocq.PCUIC.PCUICSpine]
make_context_subst_skipn [lemma, in MetaRocq.PCUIC.PCUICSpine]
make_wf_env_ext [definition, in MetaRocq.Examples.typing_correctness]
make_inductive_body [definition, in MetaRocq.Template.AstUtils]
make_constructor_body [definition, in MetaRocq.Template.AstUtils]
make_quotation_of [definition, in MetaRocq.Quotation.ToPCUIC.Init]
make_env [definition, in MetaRocq.Erasure.Typed.ExtractionCorrectness]
make_abstract_env_ext [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
make_graph_proper [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
make_quotation_of [definition, in MetaRocq.Quotation.ToTemplate.Init]
make_All_All [definition, in MetaRocq.Utils.All_Forall]
make_All_All.f [variable, in MetaRocq.Utils.All_Forall]
make_All_All.C [variable, in MetaRocq.Utils.All_Forall]
make_All_All.B [variable, in MetaRocq.Utils.All_Forall]
make_All_All.A [variable, in MetaRocq.Utils.All_Forall]
make_All_All [section, in MetaRocq.Utils.All_Forall]
make_All [definition, in MetaRocq.Utils.All_Forall]
make_All.f [variable, in MetaRocq.Utils.All_Forall]
make_All.B [variable, in MetaRocq.Utils.All_Forall]
make_All.A [variable, in MetaRocq.Utils.All_Forall]
make_All [section, in MetaRocq.Utils.All_Forall]
make_unsafe_passes [definition, in MetaRocq.ErasurePlugin.Erasure]
make_wf_env_ext [definition, in MetaRocq.Examples.metarocq_tour_prelude]
make_graph_proper [instance, in MetaRocq.Common.uGraph]
make_graph_spec2 [lemma, in MetaRocq.Common.uGraph]
make_graph_spec' [lemma, in MetaRocq.Common.uGraph]
make_graph_spec [lemma, in MetaRocq.Common.uGraph]
make_graph_invariants [instance, in MetaRocq.Common.uGraph]
make_graph_E [lemma, in MetaRocq.Common.uGraph]
make_graph [definition, in MetaRocq.Common.uGraph]
make_All [definition, in MetaRocq.SafeChecker.PCUICTypeChecker]
make_typing_spine [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
make_case [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
make_br [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
make_case_pred [definition, in MetaRocq.PCUIC.PCUICCasesHelper]
make_wf_env_ext [definition, in MetaRocq.SafeChecker.PCUICWfEnvImpl]
mapi [definition, in MetaRocq.Utils.MRList]
MapInP [section, in MetaRocq.Utils.MRList]
MapInP [section, in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.A [variable, in MetaRocq.Utils.MRList]
MapInP.A [variable, in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.B [variable, in MetaRocq.Utils.MRList]
MapInP.B [variable, in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.f [variable, in MetaRocq.PCUIC.utils.PCUICAstUtils]
MapInP.P [variable, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mapi_map2 [lemma, in MetaRocq.Utils.MRList]
mapi_unfold [lemma, in MetaRocq.Utils.MRList]
mapi_irrel_list [lemma, in MetaRocq.Utils.MRList]
mapi_nth [lemma, in MetaRocq.Utils.MRList]
mapi_cons [lemma, in MetaRocq.Utils.MRList]
mapi_length [lemma, in MetaRocq.Utils.MRList]
mapi_rec_length [lemma, in MetaRocq.Utils.MRList]
mapi_rev [lemma, in MetaRocq.Utils.MRList]
mapi_rec_rev [lemma, in MetaRocq.Utils.MRList]
mapi_app [lemma, in MetaRocq.Utils.MRList]
mapi_rec_app [lemma, in MetaRocq.Utils.MRList]
mapi_rec_add [lemma, in MetaRocq.Utils.MRList]
mapi_rec_Sk [lemma, in MetaRocq.Utils.MRList]
mapi_ext [lemma, in MetaRocq.Utils.MRList]
mapi_rec_ext [lemma, in MetaRocq.Utils.MRList]
mapi_cst_map [lemma, in MetaRocq.Utils.MRList]
mapi_mapi [lemma, in MetaRocq.Utils.MRList]
mapi_map [lemma, in MetaRocq.Utils.MRList]
mapi_rec_eqn [lemma, in MetaRocq.Utils.MRList]
mapi_compose [lemma, in MetaRocq.Utils.MRList]
mapi_rec_compose [lemma, in MetaRocq.Utils.MRList]
mapi_ext_size [lemma, in MetaRocq.Utils.MRList]
mapi_rec [definition, in MetaRocq.Utils.MRList]
mapi_length_transparent [definition, in MetaRocq.Erasure.Typed.TypeAnnotations]
mapi_context_compose [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
mapi_context_map_context [lemma, in MetaRocq.Common.BasicAst]
mapi_context_map [lemma, in MetaRocq.Common.BasicAst]
mapi_context_In_spec [lemma, in MetaRocq.Common.BasicAst]
mapi_context_In [definition, in MetaRocq.Common.BasicAst]
mapi_context_fold [lemma, in MetaRocq.Common.BasicAst]
mapi_context_length [lemma, in MetaRocq.Common.BasicAst]
mapi_context_proper [instance, in MetaRocq.Common.BasicAst]
mapi_context [definition, in MetaRocq.Common.BasicAst]
mapi_context_eqP_test_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
mapi_context_eqP_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
mapi_context_eqP_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
mapi_context_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
mapi_context_lift [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
mapi_context_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
mapi_context_fold_context [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
mapi_context_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
mapi_context_eqP_onctx_k_spec [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
mapOne [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
mapOne [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
mapopt [definition, in MetaRocq.Utils.monad_utils]
MapOpt [section, in MetaRocq.Utils.monad_utils]
mapopt_option_map [lemma, in MetaRocq.Erasure.EReorderCstrs]
mapopt_ext [instance, in MetaRocq.Erasure.EReorderCstrs]
mapopt_inv_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
mapopt_spec [lemma, in MetaRocq.Erasure.EReorderCstrs]
MapOpt.A [variable, in MetaRocq.Utils.monad_utils]
MapOpt.B [variable, in MetaRocq.Utils.monad_utils]
MapOpt.f [variable, in MetaRocq.Utils.monad_utils]
mapu_array_model_proper_cond [lemma, in MetaRocq.PCUIC.PCUICAst]
mapu_array_model_proper [lemma, in MetaRocq.PCUIC.PCUICAst]
mapu_prim_compose_rew [lemma, in MetaRocq.PCUIC.PCUICAst]
mapu_prim_compose [lemma, in MetaRocq.PCUIC.PCUICAst]
mapu_prim [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
mapu_array_model [definition, in MetaRocq.PCUIC.utils.PCUICPrimitive]
map_annots [definition, in MetaRocq.Erasure.Typed.Annotations]
map_annot [definition, in MetaRocq.Erasure.Typed.Annotations]
map_squash [lemma, in MetaRocq.Utils.MRSquash]
map_const [lemma, in MetaRocq.PCUIC.Syntax.PCUICPosition]
map_subst_lift0_subst [lemma, in MetaRocq.PCUIC.PCUICSR]
map_expand_lets_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICSR]
map_map2 [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_anon_fold_context_k [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_def_sig_nl [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map_subst_instance_to_extended_list_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_app_simpl [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_subst_lift_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_ext [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id_eq [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_subst_lift_id [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_lift_lift [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_vass_map_def [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_lift0 [lemma, in MetaRocq.PCUIC.Syntax.PCUICLiftSubst]
map_repeat [lemma, in MetaRocq.Utils.MRList]
map_InP_spec [lemma, in MetaRocq.Utils.MRList]
map_InP [definition, in MetaRocq.Utils.MRList]
map_mapIn_eq [lemma, in MetaRocq.Utils.MRList]
map_In_ext [lemma, in MetaRocq.Utils.MRList]
map_map_In [lemma, in MetaRocq.Utils.MRList]
map_In_spec [lemma, in MetaRocq.Utils.MRList]
map_In [definition, in MetaRocq.Utils.MRList]
map_inj [lemma, in MetaRocq.Utils.MRList]
map_mapi [lemma, in MetaRocq.Utils.MRList]
map_nil [lemma, in MetaRocq.Utils.MRList]
map_skipn [lemma, in MetaRocq.Utils.MRList]
map_ext [lemma, in MetaRocq.Utils.MRList]
map_ext_size [lemma, in MetaRocq.Utils.MRList]
map_id_f [lemma, in MetaRocq.Utils.MRList]
map_cst_repeat [lemma, in MetaRocq.Utils.MRList]
map_map_compose [lemma, in MetaRocq.Utils.MRList]
map_option_out_impl [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
map_vass_map_def_subst [lemma, in MetaRocq.PCUIC.PCUICSubstitution]
map_subst_closedn [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
map_decl_closed_ext [lemma, in MetaRocq.PCUIC.Syntax.PCUICClosed]
map_subst_lift1 [lemma, in MetaRocq.PCUIC.PCUICSpine]
map_subst_extended_subst [lemma, in MetaRocq.PCUIC.PCUICSpine]
map_subst_extended_subst_lift_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICSpine]
map_termM [definition, in MetaRocq.Template.AstUtils]
map_term [definition, in MetaRocq.Template.AstUtils]
map_term_with_bindersM [definition, in MetaRocq.Template.AstUtils]
map_branch_with_bindersM [definition, in MetaRocq.Template.AstUtils]
map_predicate_with_bindersM [definition, in MetaRocq.Template.AstUtils]
map_defM [definition, in MetaRocq.Template.AstUtils]
map_term_with_binders [definition, in MetaRocq.Template.AstUtils]
map_branch_with_binders [definition, in MetaRocq.Template.AstUtils]
map_predicate_with_binders [definition, in MetaRocq.Template.AstUtils]
map_decl_na [definition, in MetaRocq.PCUIC.utils.PCUICOnOne]
map_unbox_repeat_box [lemma, in MetaRocq.Erasure.EUnboxing]
map_repeat [lemma, in MetaRocq.Erasure.EUnboxing]
map_subterms [definition, in MetaRocq.Erasure.Typed.Optimize]
map_typing_result [definition, in MetaRocq.SafeChecker.PCUICSafeRetyping]
map_InP_length [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_InP_spec [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_InP [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
map_erase_length [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
map_erase_irrel [lemma, in MetaRocq.Erasure.ErasureFunctionProperties]
map_decl_body [definition, in MetaRocq.Template.EtaExpand]
map_trans_minductive_body [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_one_ind_body [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_trans_constructor_body [definition, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_expand_lets_to_extended_list_k_above [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_expand_lets_lift_cancel [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_cofix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_option_out_check_one_fix [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_context_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_map2 [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map_vass_map_def [lemma, in MetaRocq.Template.LiftSubst]
map_non_nil [lemma, in MetaRocq.Template.LiftSubst]
map_branches_k_map_branches_k [lemma, in MetaRocq.Template.LiftSubst]
map_map_subst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
map_branches_k_map_branches_k [lemma, in MetaRocq.PCUIC.PCUICConversion]
map_subst_instance_to_extended_list_k [lemma, in MetaRocq.PCUIC.Syntax.PCUICUnivSubst]
map_onPrim [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim.ont [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim.P' [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim.P [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_onPrim [section, in MetaRocq.PCUIC.PCUICEtaExpand]
map_All [definition, in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.ont [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.P' [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_All.P [variable, in MetaRocq.PCUIC.PCUICEtaExpand]
map_All [section, in MetaRocq.PCUIC.PCUICEtaExpand]
map_subterms [definition, in MetaRocq.Erasure.Typed.Utils]
map_with_bigprod [definition, in MetaRocq.Erasure.Typed.Utils]
map_In [definition, in MetaRocq.Erasure.Typed.Utils]
map_snd [definition, in MetaRocq.Erasure.Typed.Utils]
map_fst [definition, in MetaRocq.Erasure.Typed.Utils]
map_vass_map_def [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
map_decl_anon [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
map_def_anon [definition, in MetaRocq.PCUIC.Syntax.PCUICNamelessDef]
map_option_out_impl [lemma, in MetaRocq.Utils.MROption]
map_option_out_length [lemma, in MetaRocq.Utils.MROption]
map_option_out_map_option_map [lemma, in MetaRocq.Utils.MROption]
map_option_out [definition, in MetaRocq.Utils.MROption]
map_reln_ext [lemma, in MetaRocq.PCUIC.PCUICContexts]
map_subst_app_decomp [lemma, in MetaRocq.PCUIC.PCUICContexts]
map_subst_app_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICContexts]
map_subst_instance_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICContexts]
map_subst_expand_lets_k [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_subst_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_expand_lets_subst_comm [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_subst_inst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_idsn_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_inst_idsn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_map_branch_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_map_predicate_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_gen [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_map_predicate_shift [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_proper [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_proper [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_id_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_id_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift_eq_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift_eq_spec [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branches_shift [abbreviation, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_bcontext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_bbody [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.f [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.shift [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.fn [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift.T [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_branch_shift [section, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_puinst [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_pcontext [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_preturn [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_shift_pparams [lemma, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [definition, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.f [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.finst [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.shift [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.fn [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift.T [variable, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_predicate_shift [section, in MetaRocq.PCUIC.PCUICSigmaCalculus]
map_error [definition, in MetaRocq.Erasure.Typed.ResultMonad]
map_decl_name_fold_context_k [lemma, in MetaRocq.Common.BasicAst]
map_context_id [lemma, in MetaRocq.Common.BasicAst]
map_mapi_context [lemma, in MetaRocq.Common.BasicAst]
map_map_context [lemma, in MetaRocq.Common.BasicAst]
map_context_map [lemma, in MetaRocq.Common.BasicAst]
map_context_mapi_context [lemma, in MetaRocq.Common.BasicAst]
map_fold_context_k [lemma, in MetaRocq.Common.BasicAst]
map_decl_id [lemma, in MetaRocq.Common.BasicAst]
map_decl_body [lemma, in MetaRocq.Common.BasicAst]
map_decl_type [lemma, in MetaRocq.Common.BasicAst]
map_context_length [lemma, in MetaRocq.Common.BasicAst]
map_context_proper [instance, in MetaRocq.Common.BasicAst]
map_context [definition, in MetaRocq.Common.BasicAst]
map_decl_pointwise [instance, in MetaRocq.Common.BasicAst]
map_decl_proper [instance, in MetaRocq.Common.BasicAst]
map_decl_ext [lemma, in MetaRocq.Common.BasicAst]
map_decl [definition, in MetaRocq.Common.BasicAst]
map_def_id_spec [lemma, in MetaRocq.Common.BasicAst]
map_def_eq_spec [lemma, in MetaRocq.Common.BasicAst]
map_def_spec [lemma, in MetaRocq.Common.BasicAst]
map_def_id [lemma, in MetaRocq.Common.BasicAst]
map_def_map_def [lemma, in MetaRocq.Common.BasicAst]
map_dbody [lemma, in MetaRocq.Common.BasicAst]
map_dtype [lemma, in MetaRocq.Common.BasicAst]
map_def [definition, in MetaRocq.Common.BasicAst]
map_binder_annot [definition, in MetaRocq.Common.BasicAst]
map_subterms [definition, in MetaRocq.Erasure.EBeta]
map_context_eqP_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_decl_eqP_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branches_k_map_branches_k [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branches_map_branches [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_k_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_proper [instance, in MetaRocq.PCUIC.PCUICAst]
map_branch_k_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_context_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_decl_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_id [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_map_branch_k [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch_k_id [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_k_map_branch_k [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_map_branch [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_map_predicate [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_map_predicate_k [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_map_predicate_k [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_proper' [instance, in MetaRocq.PCUIC.PCUICAst]
map_predicate_proper [instance, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_context_id_spec_cond [lemma, in MetaRocq.PCUIC.PCUICAst]
map_context_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_decl_id_spec_cond [lemma, in MetaRocq.PCUIC.PCUICAst]
map_decl_id_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_eq_spec [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_id [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_map_predicate [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branches_k [abbreviation, in MetaRocq.PCUIC.PCUICAst]
map_k_bcontext [lemma, in MetaRocq.PCUIC.PCUICAst]
map_k_bbody [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch_k [definition, in MetaRocq.PCUIC.PCUICAst]
map_branch_k.g [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch_k.f [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch_k.term' [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch_k.term [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch_k [section, in MetaRocq.PCUIC.PCUICAst]
map_branches [definition, in MetaRocq.PCUIC.PCUICAst]
map_bcontext [lemma, in MetaRocq.PCUIC.PCUICAst]
map_bbody [lemma, in MetaRocq.PCUIC.PCUICAst]
map_branch [definition, in MetaRocq.PCUIC.PCUICAst]
map_branch.g [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch.f [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch.term' [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch.term [variable, in MetaRocq.PCUIC.PCUICAst]
map_branch [section, in MetaRocq.PCUIC.PCUICAst]
map_k_puinst [lemma, in MetaRocq.PCUIC.PCUICAst]
map_k_pcontext [lemma, in MetaRocq.PCUIC.PCUICAst]
map_k_preturn [lemma, in MetaRocq.PCUIC.PCUICAst]
map_k_pparams [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k [definition, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.f [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.uf [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k.term [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate_k [section, in MetaRocq.PCUIC.PCUICAst]
map_puinst [lemma, in MetaRocq.PCUIC.PCUICAst]
map_pcontext [lemma, in MetaRocq.PCUIC.PCUICAst]
map_preturn [lemma, in MetaRocq.PCUIC.PCUICAst]
map_pparams [lemma, in MetaRocq.PCUIC.PCUICAst]
map_predicate [definition, in MetaRocq.PCUIC.PCUICAst]
map_predicate.pcontextf [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate.preturnf [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate.paramf [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate.uf [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate.term' [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate.term [variable, in MetaRocq.PCUIC.PCUICAst]
map_predicate [section, in MetaRocq.PCUIC.PCUICAst]
map_remove_match_on_box_repeat_box [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
map_repeat [lemma, in MetaRocq.Erasure.EOptimizePropDiscr]
map_opt_length [lemma, in MetaRocq.Erasure.EReorderCstrs]
map_optimize_repeat_box [lemma, in MetaRocq.Erasure.EReorderCstrs]
map_depth_hom [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
map_All2 [definition, in MetaRocq.Utils.All_Forall]
map_All2.f [variable, in MetaRocq.Utils.All_Forall]
map_All2.Q [variable, in MetaRocq.Utils.All_Forall]
map_All2.P [variable, in MetaRocq.Utils.All_Forall]
map_All2.B [variable, in MetaRocq.Utils.All_Forall]
map_All2.A [variable, in MetaRocq.Utils.All_Forall]
map_All2 [section, in MetaRocq.Utils.All_Forall]
map_All_length [lemma, in MetaRocq.Utils.All_Forall]
map_All [definition, in MetaRocq.Utils.All_Forall]
map_All.fn [variable, in MetaRocq.Utils.All_Forall]
map_All.P [variable, in MetaRocq.Utils.All_Forall]
map_All.Q [variable, in MetaRocq.Utils.All_Forall]
map_All.C [variable, in MetaRocq.Utils.All_Forall]
map_All.B [variable, in MetaRocq.Utils.All_Forall]
map_All.A [variable, in MetaRocq.Utils.All_Forall]
map_All [section, in MetaRocq.Utils.All_Forall]
map_option_out_All [lemma, in MetaRocq.Utils.All_Forall]
map_option_Some [lemma, in MetaRocq.Utils.All_Forall]
map_eq_inj [lemma, in MetaRocq.Utils.All_Forall]
map_fix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
map_cofix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReduction]
map_trans_env [lemma, in MetaRocq.ErasurePlugin.ETransform]
map_of_typed_global_env [definition, in MetaRocq.ErasurePlugin.ETransform]
map_eval_primitive [definition, in MetaRocq.Erasure.EWcbvEval]
map_In_length [lemma, in MetaRocq.ErasurePlugin.Erasure]
map_constr_with_binders [definition, in MetaRocq.Template.Checker]
map_case_branch_with_binders [definition, in MetaRocq.Template.Checker]
map_predicate_with_binders [definition, in MetaRocq.Template.Checker]
map_context_with_binders [definition, in MetaRocq.Template.Checker]
map_global_env_decls [definition, in MetaRocq.Erasure.Typed.Certifying]
map_constants_global_env [definition, in MetaRocq.Erasure.Typed.Certifying]
map_constants_global_decls [definition, in MetaRocq.Erasure.Typed.Certifying]
map_subst_let_expand_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_to_extended_list [lemma, in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_k_to_extended_list_lift [lemma, in MetaRocq.PCUIC.PCUICInductives]
map_subst_let_expand_k [lemma, in MetaRocq.PCUIC.PCUICInductives]
map_expand_lets_to_extended_list_k [lemma, in MetaRocq.PCUIC.PCUICInductives]
map_context [definition, in MetaRocq.Erasure.EAst]
map_decl [definition, in MetaRocq.Erasure.EAst]
map_def [definition, in MetaRocq.Erasure.EAst]
map_bcontext_redl [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_inj [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_decomp_recomp' [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_decomp_recomp [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_recomp_decomp' [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_recomp_decomp [lemma, in MetaRocq.PCUIC.PCUICReduction]
map_subst_instance_to_extended_list_k [lemma, in MetaRocq.Template.UnivSubst]
map_fix_rho_rename [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst' [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_cofix_subst [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho_map [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_prim_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_terms_map [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_brs_map [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_brs_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_map [lemma, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_gen [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_br_wf [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_terms [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_fix_rho [definition, in MetaRocq.PCUIC.PCUICParallelReductionConfluence]
map_pair [definition, in MetaRocq.Utils.MRProd]
map_fst_add_multiple [lemma, in MetaRocq.Erasure.EWcbvEvalNamed]
map_def_name [definition, in MetaRocq.Erasure.EWcbvEvalNamed]
map_optimize_repeat_box [lemma, in MetaRocq.Erasure.EInlineProjections]
map_map2 [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_fold_context_k [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_mutual_inductive_body' [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_one_inductive_body' [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_constructor_body' [definition, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map_option_out_check_one_cofix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_option_out_check_one_fix [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_context_trans [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_map2 [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map_array_model_set_type [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_array_model_set_default [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_array_model_set_value [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_def_ext [instance, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_vass_map_def_inst [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_inst_idsn [lemma, in MetaRocq.PCUIC.Conversion.PCUICInstConv]
map_strip_repeat_box [lemma, in MetaRocq.Erasure.ERemoveParams]
map_repeat [lemma, in MetaRocq.Erasure.ERemoveParams]
map_option_out_check_one_cofix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_option_out_check_one_fix [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_map_comm [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_decl_subst_instance_set_binder_name [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_map2 [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map_branches_k_map_branches_k [lemma, in MetaRocq.Template.Ast]
map_branches_k [abbreviation, in MetaRocq.Template.Ast]
map_branches [definition, in MetaRocq.Template.Ast]
map_branches_map_branches [lemma, in MetaRocq.Template.Ast]
map_branch_id_spec [lemma, in MetaRocq.Template.Ast]
map_branch_proper [instance, in MetaRocq.Template.Ast]
map_branch_eq_spec [lemma, in MetaRocq.Template.Ast]
map_branch_id [lemma, in MetaRocq.Template.Ast]
map_branch_map_branch [lemma, in MetaRocq.Template.Ast]
map_bbody [lemma, in MetaRocq.Template.Ast]
map_branch [definition, in MetaRocq.Template.Ast]
map_branch.bbodyf [variable, in MetaRocq.Template.Ast]
map_branch.term' [variable, in MetaRocq.Template.Ast]
map_branch.term [variable, in MetaRocq.Template.Ast]
map_branch [section, in MetaRocq.Template.Ast]
map_k_puinst [lemma, in MetaRocq.Template.Ast]
map_k_pcontext [lemma, in MetaRocq.Template.Ast]
map_k_preturn [lemma, in MetaRocq.Template.Ast]
map_k_pparams [lemma, in MetaRocq.Template.Ast]
map_predicate_k [definition, in MetaRocq.Template.Ast]
map_predicate_k.f [variable, in MetaRocq.Template.Ast]
map_predicate_k.uf [variable, in MetaRocq.Template.Ast]
map_predicate_k.term [variable, in MetaRocq.Template.Ast]
map_predicate_k [section, in MetaRocq.Template.Ast]
map_predicate_proper' [instance, in MetaRocq.Template.Ast]
map_predicate_proper [instance, in MetaRocq.Template.Ast]
map_predicate_id_spec [lemma, in MetaRocq.Template.Ast]
map_predicate_eq_spec [lemma, in MetaRocq.Template.Ast]
map_predicate_id [lemma, in MetaRocq.Template.Ast]
map_predicate_map_predicate [lemma, in MetaRocq.Template.Ast]
map_puints [lemma, in MetaRocq.Template.Ast]
map_preturn [lemma, in MetaRocq.Template.Ast]
map_pparams [lemma, in MetaRocq.Template.Ast]
map_predicate [definition, in MetaRocq.Template.Ast]
map_predicate.preturnf [variable, in MetaRocq.Template.Ast]
map_predicate.paramf [variable, in MetaRocq.Template.Ast]
map_predicate.uf [variable, in MetaRocq.Template.Ast]
map_predicate.term' [variable, in MetaRocq.Template.Ast]
map_predicate.term [variable, in MetaRocq.Template.Ast]
map_predicate [section, in MetaRocq.Template.Ast]
map_onPrims [definition, in MetaRocq.Erasure.EPrimitive]
map_All2_dep [definition, in MetaRocq.Erasure.EPrimitive]
map_All2_dep.F [variable, in MetaRocq.Erasure.EPrimitive]
map_All2_dep.hP [variable, in MetaRocq.Erasure.EPrimitive]
map_All2_dep.P [variable, in MetaRocq.Erasure.EPrimitive]
map_All2_dep.B [variable, in MetaRocq.Erasure.EPrimitive]
map_All2_dep.A [variable, in MetaRocq.Erasure.EPrimitive]
map_All2_dep [section, in MetaRocq.Erasure.EPrimitive]
map_primIn_spec [lemma, in MetaRocq.Erasure.EPrimitive]
map_primIn [definition, in MetaRocq.Erasure.EPrimitive]
map_prim_eq_prop [lemma, in MetaRocq.Erasure.EPrimitive]
map_prim_eq [lemma, in MetaRocq.Erasure.EPrimitive]
map_prim_id_prop [lemma, in MetaRocq.Erasure.EPrimitive]
map_prim_id [lemma, in MetaRocq.Erasure.EPrimitive]
map_prim_compose [lemma, in MetaRocq.Erasure.EPrimitive]
map_prim [definition, in MetaRocq.Erasure.EPrimitive]
map_array_model [definition, in MetaRocq.Erasure.EPrimitive]
map_lift_map_lift [lemma, in MetaRocq.PCUIC.PCUICCasesHelper]
map_non_nil [lemma, in MetaRocq.Erasure.ELiftSubst]
map_def_id_spec [lemma, in MetaRocq.Erasure.ELiftSubst]
map_def_eq_spec [lemma, in MetaRocq.Erasure.ELiftSubst]
map_prim [abbreviation, in MetaRocq.PCUIC.utils.PCUICPrimitive]
map_array_model [abbreviation, in MetaRocq.PCUIC.utils.PCUICPrimitive]
map_trans_repeat_box [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
map_repeat [lemma, in MetaRocq.Erasure.ECoInductiveToInductive]
map2 [definition, in MetaRocq.Utils.MRList]
map2 [section, in MetaRocq.Utils.MRList]
Map2Bias [section, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.A [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.B [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.C [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.default [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
Map2Bias.f [variable, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2i [definition, in MetaRocq.Utils.MRList]
map2i_ext [lemma, in MetaRocq.Utils.MRList]
map2i_rec [definition, in MetaRocq.Utils.MRList]
map2_set_binder_name_expand_lets [lemma, in MetaRocq.PCUIC.PCUICSR]
map2_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_map_left [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_map [lemma, in MetaRocq.PCUIC.Conversion.PCUICNamelessConv]
map2_snd [lemma, in MetaRocq.Utils.MRList]
map2_diag [lemma, in MetaRocq.Utils.MRList]
map2_map_l [lemma, in MetaRocq.Utils.MRList]
map2_length [lemma, in MetaRocq.Utils.MRList]
map2_mapi [lemma, in MetaRocq.Utils.MRList]
map2_ext [lemma, in MetaRocq.Utils.MRList]
map2_map2_bias_left [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2_bias_left_length [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2_bias_left [definition, in MetaRocq.TemplatePCUIC.TemplateToPCUIC]
map2_trans [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_eq [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_Proper [instance, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_map_map [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
map2_set_binder_name_fold [lemma, in MetaRocq.PCUIC.Conversion.PCUICRenameConv]
map2_set_binder_name_alpha_eq [lemma, in MetaRocq.PCUIC.PCUICContexts]
map2_set_binder_name_alpha [lemma, in MetaRocq.PCUIC.PCUICContexts]
map2_set_binder_name_alpha_eq [lemma, in MetaRocq.PCUIC.PCUICCasesContexts]
map2_app [lemma, in MetaRocq.Utils.All_Forall]
map2_set_binder_name_map [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_map_r [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
map2_set_binder_name_context_assumptions [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
map2_length [lemma, in MetaRocq.PCUIC.Syntax.PCUICCases]
map2_trans [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_Proper [instance, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_map_map [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha_eq [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_set_binder_name_alpha [lemma, in MetaRocq.TemplatePCUIC.PCUICToTemplateCorrectness]
map2_cst [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_set_binder_name_context_assumptions [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_trans [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2_map_map [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
map2.A [variable, in MetaRocq.Utils.MRList]
map2.B [variable, in MetaRocq.Utils.MRList]
map2.C [variable, in MetaRocq.Utils.MRList]
map2.f [variable, in MetaRocq.Utils.MRList]
masked [definition, in MetaRocq.Erasure.Typed.Optimize]
masked_weakening [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_all_zeros [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_map [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_app [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_length [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_len [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_count_zeros [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
masked_nil [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mask_rev [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mask_last [lemma, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
maybe_string_of_list [definition, in MetaRocq.Erasure.EAstUtils]
Measure [section, in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.cf [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.flags [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.no [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
Measure.Σ [variable, in MetaRocq.SafeChecker.PCUICSafeReduce]
metarocq_tour [library]
metarocq_tour_prelude [library]
meta_conv_all [lemma, in MetaRocq.PCUIC.PCUICTyping]
meta_conv_term [lemma, in MetaRocq.PCUIC.PCUICTyping]
meta_conv [lemma, in MetaRocq.PCUIC.PCUICTyping]
mFix [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
mFixMfixMismatch [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
mfixpoint [definition, in MetaRocq.Common.BasicAst]
mfixpoint [definition, in MetaRocq.Erasure.EAst]
mfixpoint_size [definition, in MetaRocq.Examples.tauto]
mfixpoint_size [definition, in MetaRocq.PCUIC.utils.PCUICSize]
mfixpoint_depth_nth_error [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth_In [lemma, in MetaRocq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth [abbreviation, in MetaRocq.PCUIC.Syntax.PCUICDepth]
mfixpoint_depth_gen [definition, in MetaRocq.PCUIC.Syntax.PCUICDepth]
mFixRargMismatch [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
mfix_hole_context [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
mfix_hole [definition, in MetaRocq.PCUIC.Syntax.PCUICPosition]
mFix_mfix [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
mib_masks [record, in MetaRocq.Erasure.Typed.Optimize]
mind_body_to_entry [definition, in MetaRocq.Template.AstUtils]
mind_body_to_entry [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mind_entry_private [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_universes [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_inds [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_params [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_finite [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_record [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_lc [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_consnames [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_template [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_arity [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_typename [projection, in MetaRocq.PCUIC.PCUICAst]
mind_entry_private [projection, in MetaRocq.Erasure.EAst]
mind_entry_inds [projection, in MetaRocq.Erasure.EAst]
mind_entry_params [projection, in MetaRocq.Erasure.EAst]
mind_entry_finite [projection, in MetaRocq.Erasure.EAst]
mind_entry_record [projection, in MetaRocq.Erasure.EAst]
mind_entry_lc [projection, in MetaRocq.Erasure.EAst]
mind_entry_consnames [projection, in MetaRocq.Erasure.EAst]
mind_entry_template [projection, in MetaRocq.Erasure.EAst]
mind_entry_arity [projection, in MetaRocq.Erasure.EAst]
mind_entry_typename [projection, in MetaRocq.Erasure.EAst]
mind_entry_private [projection, in MetaRocq.Template.Ast]
mind_entry_variance [projection, in MetaRocq.Template.Ast]
mind_entry_template [projection, in MetaRocq.Template.Ast]
mind_entry_universes [projection, in MetaRocq.Template.Ast]
mind_entry_inds [projection, in MetaRocq.Template.Ast]
mind_entry_params [projection, in MetaRocq.Template.Ast]
mind_entry_finite [projection, in MetaRocq.Template.Ast]
mind_entry_record [projection, in MetaRocq.Template.Ast]
mind_entry_lc [projection, in MetaRocq.Template.Ast]
mind_entry_consnames [projection, in MetaRocq.Template.Ast]
mind_entry_arity [projection, in MetaRocq.Template.Ast]
mind_entry_typename [projection, in MetaRocq.Template.Ast]
MiniHoTT [library]
MiniHoTT_paths [library]
mkApp [definition, in MetaRocq.Erasure.EAst]
mkApp [definition, in MetaRocq.Template.Ast]
mkAppBox [definition, in MetaRocq.Erasure.Extract]
mkAppBox_repeat [lemma, in MetaRocq.Erasure.Prelim]
mkAppMkApps [lemma, in MetaRocq.Template.AstUtils]
mkApps [definition, in MetaRocq.PCUIC.PCUICAst]
mkApps [definition, in MetaRocq.Erasure.EAst]
mkApps [definition, in MetaRocq.Template.Ast]
MkAppsInd [module, in MetaRocq.Erasure.EInduction]
MkAppsInd.case [definition, in MetaRocq.Erasure.EInduction]
MkAppsInd.inspect [definition, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pforce [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plazy [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pprim [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pcofix [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pfix [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pproj [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pcase [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pconstruct [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pconst [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.papp [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plet [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.plam [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pevar [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pvar [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.prel [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.pbox [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case.P [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_case [section, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pforce [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plazy [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pprim [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pcofix [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pfix [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pproj [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pcase [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pconstruct [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pconst [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.papp [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plet [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.plam [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pevar [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pvar [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.prel [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.pbox [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec.P [variable, in MetaRocq.Erasure.EInduction]
MkAppsInd.MkApps_rec [section, in MetaRocq.Erasure.EInduction]
MkAppsInd.rec [definition, in MetaRocq.Erasure.EInduction]
mkApps_snoc [lemma, in MetaRocq.PCUIC.PCUICNormal]
mkApps_snoc [lemma, in MetaRocq.Erasure.Prelim]
mkApps_tsize [lemma, in MetaRocq.Examples.tauto]
mkApps_tApp [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
mkApps_Prim_nil [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
mkApps_Prod_nil [lemma, in MetaRocq.PCUIC.PCUICSafeLemmata]
mkApps_app [lemma, in MetaRocq.Template.AstUtils]
mkApps_nisApp [lemma, in MetaRocq.Template.AstUtils]
mkApps_tApp [lemma, in MetaRocq.Template.AstUtils]
mkApps_spec_sind [definition, in MetaRocq.Template.AstUtils]
mkApps_spec_rec [definition, in MetaRocq.Template.AstUtils]
mkApps_spec_ind [definition, in MetaRocq.Template.AstUtils]
mkApps_spec_rect [definition, in MetaRocq.Template.AstUtils]
mkApps_intro [constructor, in MetaRocq.Template.AstUtils]
mkApps_spec [inductive, in MetaRocq.Template.AstUtils]
mkApps_eq_inj [lemma, in MetaRocq.Template.AstUtils]
mkApps_mkApp [lemma, in MetaRocq.Template.AstUtils]
mkApps_nonempty [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_nisApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_elim [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_elim_rec [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_sind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_ind [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec_rect [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_intro [constructor, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_spec [inductive, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_decompose_app [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_right [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_left [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_inv [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_eq_head [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_Fix_spec [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_notApp_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_nApp_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_discr [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp_inj [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_app [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_decompose_app_rec [definition, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tApp [lemma, in MetaRocq.PCUIC.utils.PCUICAstUtils]
mkApps_tRel [lemma, in MetaRocq.Template.EtaExpand]
mkApps_trans_inv [lemma, in MetaRocq.PCUIC.PCUICExpandLetsCorrectness]
mkApps_ex [lemma, in MetaRocq.Template.LiftSubst]
mkApps_tRel [lemma, in MetaRocq.Template.LiftSubst]
mkApps_tApp [lemma, in MetaRocq.Template.LiftSubst]
mkApps_ind_typing_spine [lemma, in MetaRocq.PCUIC.PCUICInductiveInversion]
mkApps_decompose_app [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
mkApps_decompose_app_rec [definition, in MetaRocq.PCUIC.Syntax.PCUICInduction]
mkApps_context_hole [lemma, in MetaRocq.PCUIC.PCUICReduction]
mkApps_context [definition, in MetaRocq.PCUIC.PCUICReduction]
mkApps_tApp [lemma, in MetaRocq.Template.TypingWf]
mkApps_tApp' [lemma, in MetaRocq.Template.TypingWf]
mkApps_trans_wf [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_app [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_morphism [lemma, in MetaRocq.TemplatePCUIC.TemplateToPCUICCorrectness]
mkApps_eq [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_elim [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_elim_rec [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_spec_sind [definition, in MetaRocq.Erasure.EAstUtils]
mkApps_spec_rec [definition, in MetaRocq.Erasure.EAstUtils]
mkApps_spec_ind [definition, in MetaRocq.Erasure.EAstUtils]
mkApps_spec_rect [definition, in MetaRocq.Erasure.EAstUtils]
mkApps_intro [constructor, in MetaRocq.Erasure.EAstUtils]
mkApps_spec [inductive, in MetaRocq.Erasure.EAstUtils]
mkApps_eq_right [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_head_inj [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_eq_inj [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_eq_decompose_app_rec [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_head_spine_decompose [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_head_spine [lemma, in MetaRocq.Erasure.EAstUtils]
mkApps_app [lemma, in MetaRocq.Erasure.EAstUtils]
mkApp_tsize [lemma, in MetaRocq.Examples.tauto]
mkApp_tApp [lemma, in MetaRocq.Template.AstUtils]
mkApp_mkApps [lemma, in MetaRocq.Template.AstUtils]
mkApp_mkApps [lemma, in MetaRocq.Template.TypingWf]
mkApp_ex [lemma, in MetaRocq.Template.TypingWf]
mkApp_ex_wf [lemma, in MetaRocq.Template.TypingWf]
mkAssumArity [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
mkAssumArity_it_mkProd_or_LetIn [lemma, in MetaRocq.SafeChecker.PCUICSafeReduce]
mkCase_old [definition, in MetaRocq.Template.AstUtils]
mkImpl [definition, in MetaRocq.Examples.demo]
mkLambda_or_LetIn [definition, in MetaRocq.Erasure.Typed.OptimizeCorrectness]
mkNormalArity [definition, in MetaRocq.Erasure.Typed.Erasure]
mkTApps [definition, in MetaRocq.Erasure.Typed.ExAst]
mk_ctx_subst_length [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
mk_ctx_subst_spec [lemma, in MetaRocq.PCUIC.PCUICContextSubst]
mk_ctx_subst [definition, in MetaRocq.PCUIC.PCUICContextSubst]
mk_ctx_subst_spec' [lemma, in MetaRocq.PCUIC.PCUICSpine]
mk_is_eta_application [constructor, in MetaRocq.ErasurePlugin.ErasureCorrectness]
mk_is_eta_fix_application [constructor, in MetaRocq.ErasurePlugin.ErasureCorrectness]
mk_env_flags [definition, in MetaRocq.Erasure.EWcbvEval]
modpath [inductive, in MetaRocq.Common.Kernames]
ModPathComp [module, in MetaRocq.Common.Kernames]
ModPathComp.compare [definition, in MetaRocq.Common.Kernames]
ModPathComp.compare_trans [lemma, in MetaRocq.Common.Kernames]
ModPathComp.compare_sym [lemma, in MetaRocq.Common.Kernames]
ModPathComp.compare_eq [lemma, in MetaRocq.Common.Kernames]
ModPathComp.eq [definition, in MetaRocq.Common.Kernames]
ModPathComp.eq_univ [definition, in MetaRocq.Common.Kernames]
ModPathComp.mpbound_compare [definition, in MetaRocq.Common.Kernames]
ModPathComp.nat_compare_trans [lemma, in MetaRocq.Common.Kernames]
ModPathComp.nat_compare_sym [lemma, in MetaRocq.Common.Kernames]
ModPathComp.t [definition, in MetaRocq.Common.Kernames]
_ ?= _ [notation, in MetaRocq.Common.Kernames]
ModPathMap [module, in MetaRocq.Common.Kernames]
ModPathMapDecide [module, in MetaRocq.Common.Kernames]
ModPathMapExtraFact [module, in MetaRocq.Common.Kernames]
ModPathMapFact [module, in MetaRocq.Common.Kernames]
ModPathOT [module, in MetaRocq.Common.Kernames]
ModPathOTNew [module, in MetaRocq.Common.Kernames]
ModPathSet [module, in MetaRocq.Common.Kernames]
ModPathSetDecide [module, in MetaRocq.Common.Kernames]
ModPathSetExtraDecide [module, in MetaRocq.Common.Kernames]
ModPathSetExtraOrdProp [module, in MetaRocq.Common.Kernames]
ModPathSetFact [module, in MetaRocq.Common.Kernames]
ModPathSetOrdProp [module, in MetaRocq.Common.Kernames]
ModPathSetProp [module, in MetaRocq.Common.Kernames]
modpath_is_okay [definition, in MetaRocq.Quotation.CommonUtils]
modpath_is_absolute [definition, in MetaRocq.Quotation.CommonUtils]
modpath_EqDec [instance, in MetaRocq.Common.Kernames]
modpath_eq_dec [definition, in MetaRocq.Common.Kernames]
modpath_sind [definition, in MetaRocq.Common.Kernames]
modpath_rec [definition, in MetaRocq.Common.Kernames]
modpath_ind [definition, in MetaRocq.Common.Kernames]
modpath_rect [definition, in MetaRocq.Common.Kernames]
Monad [record, in MetaRocq.Utils.monad_utils]
MonadAllAll [section, in MetaRocq.Utils.monad_utils]
MonadAllAll.A [variable, in MetaRocq.Utils.monad_utils]
MonadAllAll.f [variable, in MetaRocq.Utils.monad_utils]
MonadAllAll.M [variable, in MetaRocq.Utils.monad_utils]
MonadAllAll.P [variable, in MetaRocq.Utils.monad_utils]
MonadAllAll.Q [variable, in MetaRocq.Utils.monad_utils]
MonadAllAll.T [variable, in MetaRocq.Utils.monad_utils]
MonadAst [library]
MonadBasicAst [library]
MonadExc [record, in MetaRocq.Utils.monad_utils]
MonadOperations [section, in MetaRocq.Utils.monad_utils]
MonadOperations [section, in MetaRocq.Utils.monad_utils]
MonadOperations.A [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.A [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.B [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.B [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.C [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.e [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.E [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.f [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.f [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.g [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.h [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.M [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.M [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.ME [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.T [variable, in MetaRocq.Utils.monad_utils]
MonadOperations.T [variable, in MetaRocq.Utils.monad_utils]
monad_map_branches_k [definition, in MetaRocq.Template.MonadAst]
monad_map_branches [definition, in MetaRocq.Template.MonadAst]
monad_map_branch [definition, in MetaRocq.Template.MonadAst]
monad_map_predicate_k [definition, in MetaRocq.Template.MonadAst]
monad_map_predicate [definition, in MetaRocq.Template.MonadAst]
monad_map_branches_k [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branch_k [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branches [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_branch [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_predicate_k [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_map_predicate [definition, in MetaRocq.PCUIC.PCUICMonadAst]
monad_trans_global_decl [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_minductive_body [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constant_body [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_one_ind_body [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_projection_body [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constructor_body [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_local [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_decl [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_global_decl' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_minductive_body' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constant_body' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_one_ind_body' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_projection_body' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_constructor_body' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_local' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_trans_decl' [definition, in MetaRocq.TemplatePCUIC.TemplateMonadToPCUIC]
monad_map_app_invs [lemma, in MetaRocq.SafeChecker.PCUICErrors]
monad_map_app [lemma, in MetaRocq.SafeChecker.PCUICErrors]
monad_length_map [lemma, in MetaRocq.SafeChecker.PCUICErrors]
monad_map_Forall2 [lemma, in MetaRocq.SafeChecker.PCUICErrors]
monad_map_All2 [lemma, in MetaRocq.SafeChecker.PCUICErrors]
monad_exc [instance, in MetaRocq.SafeChecker.PCUICErrors]
monad_map_In [definition, in MetaRocq.Erasure.Typed.Utils]
Monad_EnvCheck_wf_env_ext [instance, in MetaRocq.SafeCheckerPlugin.SafeTemplateChecker]
Monad_result [instance, in MetaRocq.Erasure.Typed.ResultMonad]
monad_All_All [definition, in MetaRocq.Utils.monad_utils]
monad_Alli_nth [definition, in MetaRocq.Utils.monad_utils]
monad_Alli_nth_gen [definition, in MetaRocq.Utils.monad_utils]
monad_Alli_nth.P [variable, in MetaRocq.Utils.monad_utils]
monad_Alli_nth.A [variable, in MetaRocq.Utils.monad_utils]
monad_Alli_nth.M [variable, in MetaRocq.Utils.monad_utils]
monad_Alli_nth.T [variable, in MetaRocq.Utils.monad_utils]
monad_Alli_nth [section, in MetaRocq.Utils.monad_utils]
monad_Alli_All [definition, in MetaRocq.Utils.monad_utils]
monad_Alli [definition, in MetaRocq.Utils.monad_utils]
monad_prod [definition, in MetaRocq.Utils.monad_utils]
monad_All2 [definition, in MetaRocq.Utils.monad_utils]
monad_All [definition, in MetaRocq.Utils.monad_utils]
monad_iter [definition, in MetaRocq.Utils.monad_utils]
monad_map2 [definition, in MetaRocq.Utils.monad_utils]
monad_map_i [definition, in MetaRocq.Utils.monad_utils]
monad_map_i_aux [definition, in MetaRocq.Utils.monad_utils]
monad_fold_right [definition, in MetaRocq.Utils.monad_utils]
monad_fold_left [definition, in MetaRocq.Utils.monad_utils]
monad_option_map [definition, in MetaRocq.Utils.monad_utils]
monad_map [definition, in MetaRocq.Utils.monad_utils]
Monad_EnvCheck_X_env_ext_type [instance, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_forall [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_Alli_nth_gen_forall [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_lift_ext [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_All_All [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_mapi [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_mapi_rec [definition, in MetaRocq.SafeChecker.PCUICSafeChecker]
monad_exc [instance, in MetaRocq.Template.Checker]
monad_fold_context [definition, in MetaRocq.Common.MonadBasicAst]
monad_fold_context_In [definition, in MetaRocq.Common.MonadBasicAst]
monad_mapi_context_In [definition, in MetaRocq.Common.MonadBasicAst]
monad_fold_context_k [definition, in MetaRocq.Common.MonadBasicAst]
monad_mapi_context [definition, in MetaRocq.Common.MonadBasicAst]
monad_map_context [definition, in MetaRocq.Common.MonadBasicAst]
monad_map_decl [definition, in MetaRocq.Common.MonadBasicAst]
monad_typ_or_sort_map [definition, in MetaRocq.Common.MonadBasicAst]
monad_map_def [definition, in MetaRocq.Common.MonadBasicAst]
monad_map_binder_annot [definition, in MetaRocq.Common.MonadBasicAst]
monad_utils [library]
Monomorphic_entry [constructor, in MetaRocq.Common.Universes]
Monomorphic_ctx [constructor, in MetaRocq.Common.Universes]
monomorphic_level_in_global_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_levels_of_udecl [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint_ext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_global_constraint [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
monomorphic_level_notin_AUContext [lemma, in MetaRocq.PCUIC.Conversion.PCUICUnivSubstitutionConv]
MoreCongruenceLemmas [section, in MetaRocq.PCUIC.PCUICConversion]
MoreCongruenceLemmas.cf [variable, in MetaRocq.PCUIC.PCUICConversion]
MoreCongruenceLemmas.wfΣ [variable, in MetaRocq.PCUIC.PCUICConversion]
MoreCongruenceLemmas.Σ [variable, in MetaRocq.PCUIC.PCUICConversion]
move_ws_term [definition, in MetaRocq.PCUIC.PCUICConfluence]
MPbound [constructor, in MetaRocq.Common.Kernames]
MPdot [constructor, in MetaRocq.Common.Kernames]
MPfile [constructor, in MetaRocq.Common.Kernames]
MRArith [library]
MRCompare [library]
MREquality [library]
MRFSets [library]
MRList [library]
MRListable [library]
MRMonadNotation [module, in MetaRocq.Utils.monad_utils]
_ ;; _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
' _ <- _ ;; _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
_ <- _ ;; _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
mlet ' _ <- _ ;; _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
mlet _ <- _ ;; _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
_ =<< _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
_ >>= _ (monad_scope) [notation, in MetaRocq.Utils.monad_utils]
MRMSets [library]
MROption [library]
MRPred [library]
MRPrelude [library]
MRProd [library]
MRReflect [library]
MRRelations [library]
MRSquash [library]
MRString [library]
MRUtils [library]
MR_ExtrOCamlZPosInt [library]
MR_ExtrOCamlInt63 [library]
MR_ExtrOCamlNatInt [library]
Msem [definition, in MetaRocq.Examples.tauto]
MSetAVL [module, in MetaRocq.Utils.MRMSets]
MSetAVL.Decide [module, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideSig [module, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz [module, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibnizSig [module, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.Raw [module, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.Raw.tree_EqDec [instance, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.Raw.tree_dec [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.Raw.t_EqDec [instance, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.t_EqDec [instance, in MetaRocq.Utils.MRMSets]
MSetAVL.DecideWithLeibniz.t_dec [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw [module, in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.bst_dec [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.gt_tree_dec [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.Decide.Raw.lt_tree_dec [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel [module, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrelSig [module, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw [module, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.bst_irrel [lemma, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.gt_tree_irrel [lemma, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.invert_bst [definition, in MetaRocq.Utils.MRMSets]
MSetAVL.LtIrrel.Raw.lt_tree_irrel [lemma, in MetaRocq.Utils.MRMSets]
MSetAVL.MakeSig [module, in MetaRocq.Utils.MRMSets]
MSetList [module, in MetaRocq.Utils.MRMSets]
MSetList.MakeSig [module, in MetaRocq.Utils.MRMSets]
MSetList.MakeWithLeibnizSig [module, in MetaRocq.Utils.MRMSets]
MSets [module, in MetaRocq.Utils.MRMSets]
MSets.DecideSig [module, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties [module, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdPropertiesSig [module, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.above [definition, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.above_spec [lemma, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.below [definition, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.below_spec [lemma, in MetaRocq.Utils.MRMSets]
MSets.ExtraOrdProperties.P [module, in MetaRocq.Utils.MRMSets]
MSets.FactsSig [module, in MetaRocq.Utils.MRMSets]
MSets.OrdPropertiesSig [module, in MetaRocq.Utils.MRMSets]
MSets.PropertiesSig [module, in MetaRocq.Utils.MRMSets]
MSets.UsualSets [module, in MetaRocq.Utils.MRMSets]
MSets.UsualSets.E [module, in MetaRocq.Utils.MRMSets]
MSets.WDecideOnSig [module, in MetaRocq.Utils.MRMSets]
MSets.WDecideSig [module, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn [module, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOnSig [module, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_dec [definition, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_alt_iff [lemma, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.Exists_alt [definition, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_forall2_iff [lemma, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_forall_iff [lemma, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_alt_iff [lemma, in MetaRocq.Utils.MRMSets]
MSets.WExtraPropertiesOn.For_all_alt [definition, in MetaRocq.Utils.MRMSets]
MSets.WFactsOnSig [module, in MetaRocq.Utils.MRMSets]
MSets.WFactsSig [module, in MetaRocq.Utils.MRMSets]
MSets.WPropertiesOnSig [module, in MetaRocq.Utils.MRMSets]
MSets.WPropertiesSig [module, in MetaRocq.Utils.MRMSets]
Msg [constructor, in MetaRocq.SafeChecker.PCUICErrors]
mutual_inductive_body [record, in MetaRocq.Erasure.Typed.ExAst]
mutual_inductive_entry [record, in MetaRocq.PCUIC.PCUICAst]
mutual_inductive_body [record, in MetaRocq.Erasure.EAst]
mutual_inductive_entry [record, in MetaRocq.Erasure.EAst]
mutual_inductive_entry [record, in MetaRocq.Template.Ast]
mut_pt_i [definition, in MetaRocq.Examples.demo]
mut_list_i [definition, in MetaRocq.Examples.demo]
mut_i [definition, in MetaRocq.Examples.demo]
my_None [constructor, in MetaRocq.Template.TemplateMonad.Common]
my_Some [constructor, in MetaRocq.Template.TemplateMonad.Common]
my_projT2 [projection, in MetaRocq.Template.TemplateMonad.Common]
my_projT1 [projection, in MetaRocq.Template.TemplateMonad.Common]

---

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)

Generated by coqdoc and improved with CoqdocJS