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 (18986 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 (297 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 (8135 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 (1490 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 (343 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 (524 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 (720 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 (401 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 (331 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 (4701 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 (178 entries)

_

_reduce_stack [definition, in MetaRocq.SafeChecker.PCUICSafeReduce]
_isconv [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
_isconv_fallback [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
_isconv_args [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
_isconv_args' [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
_isconv_prog [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]
_isconv_red [definition, in MetaRocq.SafeChecker.PCUICSafeConversion]