| 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 | (387 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 | (45 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 | (2 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 | (11 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 | (27 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 | (5 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 | (2 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 | (14 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 | (53 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 | (5 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 | (62 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 | (3 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 | (136 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 | (22 entries) |
Global Index
A
ap [definition, in HoTT]ap [projection, in Equiv]
apD [definition, in HoTT]
apD10 [definition, in HoTT]
append [definition, in Vector]
ap_compose [definition, in HoTT]
ap_transport [lemma, in HoTT]
ap_compose [definition, in Equiv]
B
bad_pop [definition, in DIPop]BASES [section, in Vector]
_ ++ _ [notation, in Vector]
bot [projection, in PreOrder]
bot_is_least [projection, in PreOrder]
BuildContr [constructor, in HoTT]
BuildEquiv [constructor, in Equiv]
BuildIsEquiv [constructor, in Equiv]
Build_Mon [constructor, in PreOrder]
Build_erasure [constructor, in CastMonad]
b_to_c [definition, in DepEquiv]
C
CanonicalPartialEquiv [record, in Equiv]caseS [definition, in Vector]
caseS' [definition, in Vector]
case0 [definition, in Vector]
Cast [abbreviation, in CastMonad]
CastMonad [library]
cast_fail [definition, in CastMonad]
Cast_info_wrap [definition, in CastMonad]
cast_some [definition, in CastMonad]
cast_erasure [record, in CastMonad]
Cast_info [abbreviation, in CastMonad]
cbind [definition, in CastMonad]
cbind_assoc [lemma, in CastMonad]
cbind_right_id [lemma, in CastMonad]
cbind_Some' [definition, in CastMonad]
cbind_Some [definition, in CastMonad]
center [projection, in HoTT]
check [projection, in Decidable]
Checkable [record, in Decidable]
CheckableProp [record, in Decidable]
checkable_decidable [instance, in Decidable]
Checkable_PartialEquivK [definition, in Equiv]
checkP [projection, in Decidable]
checkP_dec [projection, in Decidable]
clift [definition, in CastMonad]
compose [definition, in Equiv]
compV [definition, in Equiv]
concat [definition, in HoTT]
concat_p1 [definition, in Equiv]
concat_1p [definition, in Equiv]
cons [constructor, in Vector]
const [definition, in Vector]
contr [projection, in HoTT]
Contr [record, in HoTT]
convert [projection, in Decidable]
creturn [definition, in CastMonad]
c_to_b [definition, in DepEquiv]
c_to_a [projection, in DepEquiv]
D
dec [projection, in Decidable]dec [constructor, in Decidable]
Decidable [record, in Decidable]
Decidable [inductive, in Decidable]
Decidable [library]
DecidablePaths [record, in Decidable]
DecidablePaths_fun [instance, in Decidable]
DecidablePaths_prod [instance, in Decidable]
DecidablePaths_unit [instance, in Decidable]
DecidablePaths_option [instance, in Decidable]
DecidablePaths_list [instance, in Decidable]
DecidablePaths_nat [instance, in Decidable]
DecidablePaths_bool [instance, in Decidable]
DecidablePaths_DecidableProp [instance, in Decidable]
DecidablePaths_cast [instance, in CastMonad]
DecidablePaths_instr [instance, in DIStack]
DecidableProp [record, in Decidable]
DecidableProp_Decidable_HProp [instance, in Decidable]
decidablep_is_checkableprop [instance, in Decidable]
Decidable_proven [instance, in Decidable]
Decidable_False [instance, in Decidable]
Decidable_True [instance, in Decidable]
Decidable_implies [instance, in Decidable]
Decidable_not [instance, in Decidable]
Decidable_or [instance, in Decidable]
Decidable_and [instance, in Decidable]
Decidable_eq_option [instance, in Decidable]
Decidable_le_nat [instance, in Decidable]
Decidable_eq_list [instance, in Decidable]
Decidable_eq_nat [instance, in Decidable]
Decidable_eq_bool [instance, in Decidable]
Decidable_bool [instance, in Decidable]
decidable_is_checkable [instance, in Decidable]
Decidable_eq_cast [instance, in CastMonad]
dec_paths [projection, in Decidable]
dec_p [projection, in Decidable]
DepEquiv [record, in DepEquiv]
DepEquiv [library]
DepEquiv_eq [definition, in DepEquiv]
DepEquiv_rel [definition, in DepEquiv]
DepEquiv_PartialEquivK [definition, in DepEquiv]
DepEquiv_vector_list_simpl [instance, in DIPop]
DepEquiv_instr [instance, in DIStack]
DepEquiv_instr_retr [definition, in DIStack]
DepEquiv_dstack [instance, in DIStack]
DepEquiv_with_pe [instance, in HODepEquiv]
dinstr [inductive, in DIStack]
dinstr_to_instr [definition, in DIStack]
DIPop [library]
DIStack [library]
dstack [definition, in DIStack]
dstack_to_list [definition, in DIStack]
E
empty [inductive, in HoTT]Equiv [record, in Equiv]
Equiv [library]
EquivToPartialEquivK [definition, in Equiv]
eta_path_sigma_uncurried [definition, in HoTT]
exec [definition, in DIStack]
Exists [inductive, in Vector]
Exists_cons_tl [constructor, in Vector]
Exists_cons_hd [constructor, in Vector]
Exists2 [inductive, in Vector]
Exists2_cons_tl [constructor, in Vector]
Exists2_cons_hd [constructor, in Vector]
existT [constructor, in HoTT]
e_isequiv [projection, in Equiv]
e_fun [projection, in Equiv]
e_adj [projection, in Equiv]
e_retr [projection, in Equiv]
e_sect [projection, in Equiv]
e_inv [projection, in Equiv]
F
Fail [constructor, in CastMonad]Fail_is_not_Some [definition, in DIStack]
fold_left2 [definition, in Vector]
fold_right2 [definition, in Vector]
fold_right [definition, in Vector]
fold_left [definition, in Vector]
Forall [inductive, in Vector]
Forall_cons [constructor, in Vector]
Forall_nil [constructor, in Vector]
Forall2 [inductive, in Vector]
Forall2_cons [constructor, in Vector]
Forall2_nil [constructor, in Vector]
Functor [record, in Equiv]
FunctorOnEq [instance, in Equiv]
FunctorOnPreorder [instance, in Equiv]
Funext [definition, in HoTT]
FunExt [axiom, in HODepEquiv]
f_ord [projection, in PreOrder]
f_dep_eq [definition, in HoTT]
f_ord [projection, in CastMonad]
H
hd [definition, in Vector]Hedberg [instance, in Decidable]
HODepEquiv [instance, in HODepEquiv]
HODepEquiv [library]
HODepEquiv_easy [instance, in HODepEquiv]
HODepEquiv2 [instance, in HODepEquiv]
HODepEquiv2_sym [instance, in HODepEquiv]
HoTT [library]
HProp [record, in HoTT]
HProp_isHProp [instance, in HoTT]
Hprop_False [instance, in HoTT]
Hprop_True [instance, in HoTT]
HProp_and [instance, in HoTT]
HProp_bool [instance, in HoTT]
HSet_HProp [instance, in HoTT]
HSet_HProp [instance, in Equiv]
I
IConst [constructor, in DIStack]idL [definition, in Equiv]
idR [definition, in Equiv]
In [inductive, in Vector]
Injective_comp [instance, in Equiv]
instr [inductive, in DIStack]
instr_to_dinstr [definition, in DIStack]
instr_index [definition, in DIStack]
inst_show_vector [instance, in Showable]
inst_show_list [instance, in Showable]
inverse [definition, in HoTT]
inverse_left_inverse [lemma, in HoTT]
In_cons_tl [constructor, in Vector]
In_cons_hd [constructor, in Vector]
IPlus [constructor, in DIStack]
IsDepEquiv [definition, in DepEquiv]
IsEquiv [record, in Equiv]
IsHProp [record, in HoTT]
IsHProp [inductive, in HoTT]
IsHProp_contr [instance, in HoTT]
IsHProp_contr_ [definition, in HoTT]
IsHProp_implies [instance, in HoTT]
IsHProp_not [instance, in HoTT]
IsHProp_sum [instance, in HoTT]
isHSet [projection, in HoTT]
IsHSet [record, in HoTT]
IsInjective [record, in Equiv]
IsInjective_S [instance, in Equiv]
IsInjective_id [definition, in Equiv]
IsPartialEquiv [record, in Equiv]
IsPartialEquivK [record, in Equiv]
is_hprop_c [projection, in Decidable]
is_hprop_p [projection, in Decidable]
Is_true [definition, in HoTT]
is_hprop [projection, in HoTT]
is_hprop [constructor, in HoTT]
ITERATORS [section, in Vector]
i_retr [projection, in Equiv]
i_sect [projection, in Equiv]
i_inv [projection, in Equiv]
K
kleisli_comp [definition, in CastMonad]L
last [definition, in Vector]lift [definition, in HODepEquiv]
lift2 [definition, in HODepEquiv]
list_to_vector [definition, in DIPop]
list_to_dstack [definition, in DIStack]
M
map [definition, in Vector]map_list [definition, in DIPop]
map2 [definition, in Vector]
mon [projection, in PreOrder]
monotone_function [record, in PreOrder]
N
NConst [constructor, in DIStack]nil [constructor, in Vector]
not [definition, in HoTT]
not_implemented [definition, in Showable]
NPlus [constructor, in DIStack]
nth [definition, in Vector]
nth_order [definition, in Vector]
O
of_list [definition, in Vector]P
P [projection, in DepEquiv]PartialEquivK [record, in Equiv]
partial_equiv [projection, in DepEquiv]
path_sum [definition, in HoTT]
path_conj_uncurried [definition, in HoTT]
path_prod_uncurried [definition, in HoTT]
path_sigma_uncurried [definition, in HoTT]
path_sigma [definition, in HoTT]
path_Cast_inv [definition, in CastMonad]
path_Cast [definition, in CastMonad]
pek_isequiv [projection, in Equiv]
pek_fun [projection, in Equiv]
pek_adj [projection, in Equiv]
pek_retr [projection, in Equiv]
pek_sect [projection, in Equiv]
pek_inv [projection, in Equiv]
pe_isequiv [projection, in Equiv]
pe_fun [projection, in Equiv]
pe_adj [projection, in Equiv]
pe_retr [projection, in Equiv]
pe_sect [projection, in Equiv]
pe_inv [projection, in Equiv]
pop [definition, in DIPop]
pop' [definition, in DIPop]
PreOrder [library]
PreOrderCast [instance, in CastMonad]
PreOrderCast_HProp [instance, in CastMonad]
PreOrder_forall [instance, in PreOrder]
PreOrder_p [record, in PreOrder]
projT1 [definition, in HoTT]
projT2 [definition, in HoTT]
proj1 [definition, in HoTT]
proj2 [definition, in HoTT]
prop_c_to_a [projection, in DepEquiv]
pr1_path [definition, in HoTT]
pr2_path [definition, in HoTT]
p_mon [projection, in PreOrder]
R
rectS [definition, in Vector]rect2 [definition, in Vector]
rel [projection, in PreOrder]
rel_trans [projection, in PreOrder]
rel_refl [projection, in PreOrder]
replace [definition, in Vector]
replace_order [definition, in Vector]
rev [definition, in Vector]
rev_append [definition, in Vector]
rev_append_tail [definition, in Vector]
S
SCANNING [section, in Vector]SCHEMES [section, in Vector]
shiftin [definition, in Vector]
shiftout [definition, in Vector]
shiftrepeat [definition, in Vector]
show [projection, in Showable]
Show [record, in Showable]
Showable [library]
showC [projection, in DepEquiv]
show_nat [instance, in Showable]
show_default [instance, in Showable]
show_not_implemented_for [axiom, in Showable]
show_instr [instance, in DIStack]
sigT [inductive, in HoTT]
simple_exec [definition, in DIStack]
Some [constructor, in CastMonad]
Some_inj_eq [definition, in CastMonad]
Some_inj_retr [definition, in CastMonad]
Some_inj_sect [definition, in CastMonad]
Some_inj [definition, in CastMonad]
sub_eq_implies_complex [definition, in DepEquiv]
sub_eq_implies_simpl [definition, in DepEquiv]
sub_eq_implies [definition, in DepEquiv]
S_length [definition, in DIPop]
S_inv [definition, in Equiv]
T
t [inductive, in Vector]tl [definition, in Vector]
TotalEquiv [definition, in DepEquiv]
total_equiv [projection, in DepEquiv]
to_list [definition, in Vector]
to_simpl_dom [definition, in DepEquiv]
to_dep_dom2 [definition, in DepEquiv]
to_dep_dom [definition, in DepEquiv]
to_simpl [definition, in DepEquiv]
to_dep [definition, in DepEquiv]
to_rich [definition, in DepEquiv]
to_dep_dom2 [definition, in HODepEquiv]
to_simpl_dom2 [definition, in HODepEquiv]
to_subset [definition, in Equiv]
transport [definition, in HoTT]
transport_cst_sigma [definition, in HoTT]
transport_Cast_Fail [definition, in CastMonad]
transport_Cast [definition, in CastMonad]
transport_vector [definition, in DIPop]
transport_instr_Plus [definition, in DIStack]
transport_instr_Const [definition, in DIStack]
transport_bind [definition, in Equiv]
trunc [lemma, in Vector]
Trunc [module, in HoTT]
trunc_sigma [instance, in HoTT]
Trunc.istrunc_horio [instance, in HoTT]
Trunc.tr [constructor, in HoTT]
Trunc.Trunc [inductive, in HoTT]
Trunc.Trunc_ind [definition, in HoTT]
U
unlift [definition, in HODepEquiv]use_fail [definition, in CastMonad]
use_some [definition, in CastMonad]
use_bool [definition, in CastMonad]
V
valid_instr [definition, in DIStack]vcons [definition, in DIPop]
vector [definition, in DIPop]
Vector [library]
VECTORLIST [section, in Vector]
VectorNotations [module, in Vector]
_ [@ _ ] (vector_scope) [notation, in Vector]
[ _ ; .. ; _ ] (vector_scope) [notation, in Vector]
[ _ ] (vector_scope) [notation, in Vector]
_ :: _ (vector_scope) [notation, in Vector]
[] (vector_scope) [notation, in Vector]
vector_to_list [definition, in DIPop]
vnil [definition, in DIPop]
_
_show_vector [definition, in Showable]_show_list [definition, in Showable]
_HProp_isHProp [projection, in HoTT]
_typeP [projection, in HoTT]
_Cast [inductive, in CastMonad]
other
{ _ : _ & _ } (type_scope) [notation, in HoTT]{ _ : _ & _ } (type_scope) [notation, in DIPop]
{ _ : _ & _ } (type_scope) [notation, in DIStack]
_ [@ _ ] [notation, in Vector]
_ :: _ [notation, in Vector]
_ ≈ _ [notation, in DepEquiv]
_ .2 [notation, in DepEquiv]
_ .1 [notation, in DepEquiv]
_ --> _ [notation, in PreOrder]
_ ≼ _ [notation, in PreOrder]
_ ..2 [notation, in HoTT]
_ ..1 [notation, in HoTT]
_ ^ [notation, in HoTT]
_ @ _ [notation, in HoTT]
_ # _ [notation, in HoTT]
_ == _ [notation, in HoTT]
_ .2 [notation, in HoTT]
_ .1 [notation, in HoTT]
_ °° _ [notation, in CastMonad]
_ <- _ ; _ [notation, in CastMonad]
_ >>= _ [notation, in CastMonad]
_ ⇀ _ [notation, in CastMonad]
_ .2 [notation, in DIPop]
_ .1 [notation, in DIPop]
_ .2 [notation, in DIStack]
_ .1 [notation, in DIStack]
_ ^?-1 [notation, in Equiv]
_ ≃?K _ [notation, in Equiv]
_ °H _ [notation, in Equiv]
_ °V _ [notation, in Equiv]
_ ≃? _ [notation, in Equiv]
_ ≃ _ [notation, in Equiv]
_ ° _ [notation, in Equiv]
idK _ [notation, in Equiv]
( _ ; _ ) [notation, in DepEquiv]
( _ ; _ ) [notation, in HoTT]
( _ ; _ ) [notation, in DIPop]
( _ ; _ ) [notation, in DIStack]
[] [notation, in Vector]
α [definition, in Equiv]
π1 [abbreviation, in Equiv]
Notation Index
B
_ ++ _ [in Vector]V
_ [@ _ ] (vector_scope) [in Vector][ _ ; .. ; _ ] (vector_scope) [in Vector]
[ _ ] (vector_scope) [in Vector]
_ :: _ (vector_scope) [in Vector]
[] (vector_scope) [in Vector]
other
{ _ : _ & _ } (type_scope) [in HoTT]{ _ : _ & _ } (type_scope) [in DIPop]
{ _ : _ & _ } (type_scope) [in DIStack]
_ [@ _ ] [in Vector]
_ :: _ [in Vector]
_ ≈ _ [in DepEquiv]
_ .2 [in DepEquiv]
_ .1 [in DepEquiv]
_ --> _ [in PreOrder]
_ ≼ _ [in PreOrder]
_ ..2 [in HoTT]
_ ..1 [in HoTT]
_ ^ [in HoTT]
_ @ _ [in HoTT]
_ # _ [in HoTT]
_ == _ [in HoTT]
_ .2 [in HoTT]
_ .1 [in HoTT]
_ °° _ [in CastMonad]
_ <- _ ; _ [in CastMonad]
_ >>= _ [in CastMonad]
_ ⇀ _ [in CastMonad]
_ .2 [in DIPop]
_ .1 [in DIPop]
_ .2 [in DIStack]
_ .1 [in DIStack]
_ ^?-1 [in Equiv]
_ ≃?K _ [in Equiv]
_ °H _ [in Equiv]
_ °V _ [in Equiv]
_ ≃? _ [in Equiv]
_ ≃ _ [in Equiv]
_ ° _ [in Equiv]
idK _ [in Equiv]
( _ ; _ ) [in DepEquiv]
( _ ; _ ) [in HoTT]
( _ ; _ ) [in DIPop]
( _ ; _ ) [in DIStack]
[] [in Vector]
Module Index
T
Trunc [in HoTT]V
VectorNotations [in Vector]Library Index
C
CastMonadD
DecidableDepEquiv
DIPop
DIStack
E
EquivH
HODepEquivHoTT
P
PreOrderS
ShowableV
VectorConstructor Index
B
BuildContr [in HoTT]BuildEquiv [in Equiv]
BuildIsEquiv [in Equiv]
Build_Mon [in PreOrder]
Build_erasure [in CastMonad]
C
cons [in Vector]D
dec [in Decidable]E
Exists_cons_tl [in Vector]Exists_cons_hd [in Vector]
Exists2_cons_tl [in Vector]
Exists2_cons_hd [in Vector]
existT [in HoTT]
F
Fail [in CastMonad]Forall_cons [in Vector]
Forall_nil [in Vector]
Forall2_cons [in Vector]
Forall2_nil [in Vector]
I
IConst [in DIStack]In_cons_tl [in Vector]
In_cons_hd [in Vector]
IPlus [in DIStack]
is_hprop [in HoTT]
N
NConst [in DIStack]nil [in Vector]
NPlus [in DIStack]
S
Some [in CastMonad]T
Trunc.tr [in HoTT]Lemma Index
A
ap_transport [in HoTT]C
cbind_assoc [in CastMonad]cbind_right_id [in CastMonad]
I
inverse_left_inverse [in HoTT]T
trunc [in Vector]Axiom Index
F
FunExt [in HODepEquiv]S
show_not_implemented_for [in Showable]Inductive Index
D
Decidable [in Decidable]dinstr [in DIStack]
E
empty [in HoTT]Exists [in Vector]
Exists2 [in Vector]
F
Forall [in Vector]Forall2 [in Vector]
I
In [in Vector]instr [in DIStack]
IsHProp [in HoTT]
S
sigT [in HoTT]T
t [in Vector]Trunc.Trunc [in HoTT]
_
_Cast [in CastMonad]Projection Index
A
ap [in Equiv]B
bot [in PreOrder]bot_is_least [in PreOrder]
C
center [in HoTT]check [in Decidable]
checkP [in Decidable]
checkP_dec [in Decidable]
contr [in HoTT]
convert [in Decidable]
c_to_a [in DepEquiv]
D
dec [in Decidable]dec_paths [in Decidable]
dec_p [in Decidable]
E
e_isequiv [in Equiv]e_fun [in Equiv]
e_adj [in Equiv]
e_retr [in Equiv]
e_sect [in Equiv]
e_inv [in Equiv]
F
f_ord [in PreOrder]f_ord [in CastMonad]
I
isHSet [in HoTT]is_hprop_c [in Decidable]
is_hprop_p [in Decidable]
is_hprop [in HoTT]
i_retr [in Equiv]
i_sect [in Equiv]
i_inv [in Equiv]
M
mon [in PreOrder]P
P [in DepEquiv]partial_equiv [in DepEquiv]
pek_isequiv [in Equiv]
pek_fun [in Equiv]
pek_adj [in Equiv]
pek_retr [in Equiv]
pek_sect [in Equiv]
pek_inv [in Equiv]
pe_isequiv [in Equiv]
pe_fun [in Equiv]
pe_adj [in Equiv]
pe_retr [in Equiv]
pe_sect [in Equiv]
pe_inv [in Equiv]
prop_c_to_a [in DepEquiv]
p_mon [in PreOrder]
R
rel [in PreOrder]rel_trans [in PreOrder]
rel_refl [in PreOrder]
S
show [in Showable]showC [in DepEquiv]
T
total_equiv [in DepEquiv]_
_HProp_isHProp [in HoTT]_typeP [in HoTT]
Section Index
B
BASES [in Vector]I
ITERATORS [in Vector]S
SCANNING [in Vector]SCHEMES [in Vector]
V
VECTORLIST [in Vector]Instance Index
C
checkable_decidable [in Decidable]D
DecidablePaths_fun [in Decidable]DecidablePaths_prod [in Decidable]
DecidablePaths_unit [in Decidable]
DecidablePaths_option [in Decidable]
DecidablePaths_list [in Decidable]
DecidablePaths_nat [in Decidable]
DecidablePaths_bool [in Decidable]
DecidablePaths_DecidableProp [in Decidable]
DecidablePaths_cast [in CastMonad]
DecidablePaths_instr [in DIStack]
DecidableProp_Decidable_HProp [in Decidable]
decidablep_is_checkableprop [in Decidable]
Decidable_proven [in Decidable]
Decidable_False [in Decidable]
Decidable_True [in Decidable]
Decidable_implies [in Decidable]
Decidable_not [in Decidable]
Decidable_or [in Decidable]
Decidable_and [in Decidable]
Decidable_eq_option [in Decidable]
Decidable_le_nat [in Decidable]
Decidable_eq_list [in Decidable]
Decidable_eq_nat [in Decidable]
Decidable_eq_bool [in Decidable]
Decidable_bool [in Decidable]
decidable_is_checkable [in Decidable]
Decidable_eq_cast [in CastMonad]
DepEquiv_vector_list_simpl [in DIPop]
DepEquiv_instr [in DIStack]
DepEquiv_dstack [in DIStack]
DepEquiv_with_pe [in HODepEquiv]
F
FunctorOnEq [in Equiv]FunctorOnPreorder [in Equiv]
H
Hedberg [in Decidable]HODepEquiv [in HODepEquiv]
HODepEquiv_easy [in HODepEquiv]
HODepEquiv2 [in HODepEquiv]
HODepEquiv2_sym [in HODepEquiv]
HProp_isHProp [in HoTT]
Hprop_False [in HoTT]
Hprop_True [in HoTT]
HProp_and [in HoTT]
HProp_bool [in HoTT]
HSet_HProp [in HoTT]
HSet_HProp [in Equiv]
I
Injective_comp [in Equiv]inst_show_vector [in Showable]
inst_show_list [in Showable]
IsHProp_contr [in HoTT]
IsHProp_implies [in HoTT]
IsHProp_not [in HoTT]
IsHProp_sum [in HoTT]
IsInjective_S [in Equiv]
P
PreOrderCast [in CastMonad]PreOrderCast_HProp [in CastMonad]
PreOrder_forall [in PreOrder]
S
show_nat [in Showable]show_default [in Showable]
show_instr [in DIStack]
T
trunc_sigma [in HoTT]Trunc.istrunc_horio [in HoTT]
Abbreviation Index
C
Cast [in CastMonad]Cast_info [in CastMonad]
other
π1 [in Equiv]Definition Index
A
ap [in HoTT]apD [in HoTT]
apD10 [in HoTT]
append [in Vector]
ap_compose [in HoTT]
ap_compose [in Equiv]
B
bad_pop [in DIPop]b_to_c [in DepEquiv]
C
caseS [in Vector]caseS' [in Vector]
case0 [in Vector]
cast_fail [in CastMonad]
Cast_info_wrap [in CastMonad]
cast_some [in CastMonad]
cbind [in CastMonad]
cbind_Some' [in CastMonad]
cbind_Some [in CastMonad]
Checkable_PartialEquivK [in Equiv]
clift [in CastMonad]
compose [in Equiv]
compV [in Equiv]
concat [in HoTT]
concat_p1 [in Equiv]
concat_1p [in Equiv]
const [in Vector]
creturn [in CastMonad]
c_to_b [in DepEquiv]
D
DepEquiv_eq [in DepEquiv]DepEquiv_rel [in DepEquiv]
DepEquiv_PartialEquivK [in DepEquiv]
DepEquiv_instr_retr [in DIStack]
dinstr_to_instr [in DIStack]
dstack [in DIStack]
dstack_to_list [in DIStack]
E
EquivToPartialEquivK [in Equiv]eta_path_sigma_uncurried [in HoTT]
exec [in DIStack]
F
Fail_is_not_Some [in DIStack]fold_left2 [in Vector]
fold_right2 [in Vector]
fold_right [in Vector]
fold_left [in Vector]
Funext [in HoTT]
f_dep_eq [in HoTT]
H
hd [in Vector]I
idL [in Equiv]idR [in Equiv]
instr_to_dinstr [in DIStack]
instr_index [in DIStack]
inverse [in HoTT]
IsDepEquiv [in DepEquiv]
IsHProp_contr_ [in HoTT]
IsInjective_id [in Equiv]
Is_true [in HoTT]
K
kleisli_comp [in CastMonad]L
last [in Vector]lift [in HODepEquiv]
lift2 [in HODepEquiv]
list_to_vector [in DIPop]
list_to_dstack [in DIStack]
M
map [in Vector]map_list [in DIPop]
map2 [in Vector]
N
not [in HoTT]not_implemented [in Showable]
nth [in Vector]
nth_order [in Vector]
O
of_list [in Vector]P
path_sum [in HoTT]path_conj_uncurried [in HoTT]
path_prod_uncurried [in HoTT]
path_sigma_uncurried [in HoTT]
path_sigma [in HoTT]
path_Cast_inv [in CastMonad]
path_Cast [in CastMonad]
pop [in DIPop]
pop' [in DIPop]
projT1 [in HoTT]
projT2 [in HoTT]
proj1 [in HoTT]
proj2 [in HoTT]
pr1_path [in HoTT]
pr2_path [in HoTT]
R
rectS [in Vector]rect2 [in Vector]
replace [in Vector]
replace_order [in Vector]
rev [in Vector]
rev_append [in Vector]
rev_append_tail [in Vector]
S
shiftin [in Vector]shiftout [in Vector]
shiftrepeat [in Vector]
simple_exec [in DIStack]
Some_inj_eq [in CastMonad]
Some_inj_retr [in CastMonad]
Some_inj_sect [in CastMonad]
Some_inj [in CastMonad]
sub_eq_implies_complex [in DepEquiv]
sub_eq_implies_simpl [in DepEquiv]
sub_eq_implies [in DepEquiv]
S_length [in DIPop]
S_inv [in Equiv]
T
tl [in Vector]TotalEquiv [in DepEquiv]
to_list [in Vector]
to_simpl_dom [in DepEquiv]
to_dep_dom2 [in DepEquiv]
to_dep_dom [in DepEquiv]
to_simpl [in DepEquiv]
to_dep [in DepEquiv]
to_rich [in DepEquiv]
to_dep_dom2 [in HODepEquiv]
to_simpl_dom2 [in HODepEquiv]
to_subset [in Equiv]
transport [in HoTT]
transport_cst_sigma [in HoTT]
transport_Cast_Fail [in CastMonad]
transport_Cast [in CastMonad]
transport_vector [in DIPop]
transport_instr_Plus [in DIStack]
transport_instr_Const [in DIStack]
transport_bind [in Equiv]
Trunc.Trunc_ind [in HoTT]
U
unlift [in HODepEquiv]use_fail [in CastMonad]
use_some [in CastMonad]
use_bool [in CastMonad]
V
valid_instr [in DIStack]vcons [in DIPop]
vector [in DIPop]
vector_to_list [in DIPop]
vnil [in DIPop]
_
_show_vector [in Showable]_show_list [in Showable]
other
α [in Equiv]Record Index
C
CanonicalPartialEquiv [in Equiv]cast_erasure [in CastMonad]
Checkable [in Decidable]
CheckableProp [in Decidable]
Contr [in HoTT]
D
Decidable [in Decidable]DecidablePaths [in Decidable]
DecidableProp [in Decidable]
DepEquiv [in DepEquiv]
E
Equiv [in Equiv]F
Functor [in Equiv]H
HProp [in HoTT]I
IsEquiv [in Equiv]IsHProp [in HoTT]
IsHSet [in HoTT]
IsInjective [in Equiv]
IsPartialEquiv [in Equiv]
IsPartialEquivK [in Equiv]
M
monotone_function [in PreOrder]P
PartialEquivK [in Equiv]PreOrder_p [in PreOrder]
S
Show [in Showable]| 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 | (387 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 | (45 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 | (2 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 | (11 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 | (27 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 | (5 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 | (2 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 | (14 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 | (53 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 | (5 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 | (62 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 | (3 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 | (136 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 | (22 entries) |
This page has been generated by coqdoc