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 | (75519 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 | (245 entries) |
Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |
P (constructor)
ParameterEntry [in MetaCoq.Template.Ast]ParameterEntry [in MetaCoq.PCUIC.PCUICAst]
ParameterEntry [in MetaCoq.Erasure.EAst]
Polymorphic_entry [in MetaCoq.Template.Universes]
Polymorphic_ctx [in MetaCoq.Template.Universes]
positionR_root [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_deep [in MetaCoq.PCUIC.Syntax.PCUICPosition]
positionR_app_lr [in MetaCoq.PCUIC.Syntax.PCUICPosition]
pred_atom_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_prod [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_fix_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_proj_congr [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_case [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_letin [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_app [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_abs [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_proj [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_const [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_delta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_proj [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_cofix_case [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_fix [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_iota [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_rel_refl [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_rel_def_unfold [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_zeta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_beta [in MetaCoq.PCUIC.PCUICParallelReduction]
pred_hole_return [in MetaCoq.PCUIC.Syntax.PCUICPosition]
pred_hole_params [in MetaCoq.PCUIC.Syntax.PCUICPosition]
primFloat [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primFloatModel [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primInt [in MetaCoq.PCUIC.utils.PCUICPrimitive]
primIntModel [in MetaCoq.PCUIC.utils.PCUICPrimitive]
ProdNotConvertibleAnn [in MetaCoq.SafeChecker.PCUICErrors]
ProdNotConvertibleDomains [in MetaCoq.SafeChecker.PCUICErrors]
prod_cons [in MetaCoq.PCUIC.Bidirectional.BDTyping]
prod_red_r [in MetaCoq.Template.Typing]
prod_red_l [in MetaCoq.Template.Typing]
Prod_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
Prod_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_r [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_l [in MetaCoq.PCUIC.Syntax.PCUICPosition]
prod_letin_other [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_letin_tLetIn [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_letin_tProd [in MetaCoq.SafeChecker.PCUICSafeChecker]
prod_red_r [in MetaCoq.PCUIC.PCUICReduction]
prod_red_l [in MetaCoq.PCUIC.PCUICReduction]
prog_view_other [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_CoFix [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Fix [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Proj [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Case [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Prod [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Lambda [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_Const [in MetaCoq.SafeChecker.PCUICSafeConversion]
prog_view_App [in MetaCoq.SafeChecker.PCUICSafeConversion]
Proj [in MetaCoq.PCUIC.Syntax.PCUICPosition]
proj_red [in MetaCoq.Template.Typing]
proj_c [in MetaCoq.PCUIC.Syntax.PCUICPosition]
proj_red [in MetaCoq.PCUIC.PCUICReduction]
PropLevel.lProp [in MetaCoq.Template.Universes]
PropLevel.lSProp [in MetaCoq.Template.Universes]
PropLevel.ltSPropProp [in MetaCoq.Template.Universes]
psubst_vdef [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_vass [in MetaCoq.PCUIC.PCUICParallelReduction]
psubst_empty [in MetaCoq.PCUIC.PCUICParallelReduction]
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 | (75519 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 | (245 entries) |
Binder 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 | (61331 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 | (144 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 | (89 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 | (236 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 | (6913 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 | (1141 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 | (34 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 | (269 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 | (443 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 | (296 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 | (604 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 | (248 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 | (3386 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 | (140 entries) |