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) |