| 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 | _ | (795 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 | _ | (4 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 | _ | (1 entry) |
| 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 | _ | (348 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 | _ | (26 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 | _ | (75 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 | _ | (27 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 | _ | (47 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 | _ | (199 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 | _ | (8 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 | _ | (6 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 | _ | (47 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 | _ | (7 entries) |
Global Index
A
ALL [constructor, in sysf]APP [constructor, in sysf]
app [definition, in tutorial]
appH [definition, in tutorial]
appmatcol [definition, in tutorial]
appmatcolH [definition, in tutorial]
appmatcol_assoc [lemma, in tutorial]
appmatcol_assocH [lemma, in tutorial]
appmatrow [definition, in tutorial]
appmatrowH [definition, in tutorial]
appmatrow_assoc [lemma, in tutorial]
appmatrow_assocH [lemma, in tutorial]
app_ass [lemma, in tutorial]
app_assH [lemma, in tutorial]
app_nil [lemma, in tutorial]
app_nilH [lemma, in tutorial]
ARR [constructor, in sysf]
B
Bool [section, in Vector]Bool.A [variable, in Vector]
Bool.f [variable, in Vector]
C
cast_compose [lemma, in Heq.Heq]cast_elim [lemma, in Heq.Heq]
cast_elim_r [lemma, in Heq.Heq]
cast_intro [lemma, in Heq.Heq]
cast_intro_r [lemma, in Heq.Heq]
CompMR [section, in sysf]
CompMR.ops [variable, in sysf]
CompMR.P [variable, in sysf]
cons [constructor, in tutorial]
conscol [definition, in tutorial]
conscolH [definition, in tutorial]
consH [constructor, in tutorial]
conshdtlcol [lemma, in tutorial]
conshdtlcolH [lemma, in tutorial]
consMap [definition, in sysf]
consmap [definition, in sysf]
consMapInv [lemma, in sysf]
consmap_shsub [lemma, in sysf]
consMap_shSub [lemma, in sysf]
consMap_SubL [lemma, in sysf]
consmap_subL [lemma, in sysf]
consMap_succ [lemma, in sysf]
consPredExp [definition, in strnorm]
consPredExp_hd [lemma, in strnorm]
consPredExp_is_CR [lemma, in strnorm]
consPredExp_tl [lemma, in strnorm]
cons_leA [abbreviation, in MergesortList]
cons_leA [abbreviation, in MergesortVector]
cons_sort [abbreviation, in MergesortList]
cons_sort [abbreviation, in MergesortVector]
convert [inductive, in strnorm]
convertC [definition, in strnorm]
convert_sub [lemma, in strnorm]
convert_subst [lemma, in strnorm]
count_occ_cons_eq [lemma, in Vector]
count_occ_cons_neq [lemma, in Vector]
CR [definition, in strnorm]
CR1 [definition, in strnorm]
CR2 [definition, in strnorm]
CR3 [definition, in strnorm]
CR4 [lemma, in strnorm]
Cutting [section, in Vector]
Cutting.A [variable, in Vector]
c_app [constructor, in strnorm]
c_cong_app_1 [constructor, in strnorm]
c_cong_app_2 [constructor, in strnorm]
c_cong_lam [constructor, in strnorm]
c_cong_tabs [constructor, in strnorm]
c_cong_tapp [constructor, in strnorm]
c_tapp [constructor, in strnorm]
D
defs [section, in MergesortVector]defs [section, in MergesortList]
defs.A [variable, in MergesortVector]
defs.A [variable, in MergesortList]
defs.R [variable, in MergesortVector]
defs.R [variable, in MergesortList]
destruct_vector [lemma, in Vector]
distr_rev [lemma, in tutorial]
distr_revH [lemma, in tutorial]
dropMap [definition, in sysf]
dropRen [definition, in sysf]
dropSub [definition, in sysf]
E
Elts [section, in Vector]Elts.A [variable, in Vector]
Elts.eqA_dec [variable, in Vector]
Elts.Remove [section, in Vector]
Elts.Remove.eq_dec [variable, in Vector]
Env [definition, in sysf]
eq_Heq [lemma, in Heq.Heq]
eq_HeqI [lemma, in Heq.Heq]
eq_implies_iff [lemma, in strnorm]
Exp [inductive, in sysf]
F
Facts [section, in Vector]Facts.A [variable, in Vector]
finish_tag [definition, in Heq.Heq]
Fold_Left_Recursor [section, in Vector]
Fold_Left_Recursor.A [variable, in Vector]
Fold_Left_Recursor.B [variable, in Vector]
Fold_Left_Recursor.f [variable, in Vector]
Fold_Right_Recursor [section, in Vector]
Fold_Right_Recursor.A [variable, in Vector]
Fold_Right_Recursor.a0 [variable, in Vector]
Fold_Right_Recursor.B [variable, in Vector]
Fold_Right_Recursor.f [variable, in Vector]
Forall [inductive, in MergesortList]
Forall [inductive, in MergesortVector]
Forall_cons [constructor, in MergesortVector]
Forall_cons [constructor, in MergesortList]
Forall_impl [lemma, in MergesortList]
Forall_impl [lemma, in MergesortVector]
Forall_nil [constructor, in MergesortVector]
Forall_nil [constructor, in MergesortList]
Fundamental [lemma, in strnorm]
H
Happ [lemma, in Heq.Heq]Happdep [lemma, in Heq.Heq]
hcast [definition, in Heq.Heq]
hd [definition, in tutorial]
hdcol [definition, in tutorial]
hdcolH [definition, in tutorial]
hdconscol [lemma, in tutorial]
hdconscolH [lemma, in tutorial]
hdConsMap [lemma, in sysf]
hdEnv [definition, in sysf]
hdH [definition, in tutorial]
hdMap [definition, in sysf]
hdMap_substMap [lemma, in sysf]
hdMap_subSub [lemma, in sysf]
HdRel [inductive, in MergesortVector]
HdRel [inductive, in MergesortList]
HdRel_cons [constructor, in MergesortList]
HdRel_cons [constructor, in MergesortVector]
HdRel_inv [lemma, in MergesortList]
HdRel_inv [lemma, in MergesortVector]
HdRel_nil [constructor, in MergesortList]
HdRel_nil [constructor, in MergesortVector]
hdtail [lemma, in tutorial]
hdtailH [lemma, in tutorial]
Heq [definition, in Heq.Heq]
Heq [library]
HeqEvar [definition, in Heq.Heq]
HeqHint [definition, in Heq.Heq]
HeqLockHyp1 [definition, in Heq.Heq]
HeqLockHyp2 [definition, in Heq.Heq]
Heq_eq [lemma, in Heq.Heq]
Heq_eqI [lemma, in Heq.Heq]
Heq_eq_dep [lemma, in Heq.Heq]
Heq_extensionality [lemma, in Heq.Heq]
Heq_fold [lemma, in Heq.Heq]
Heq_ind_gen [lemma, in Heq.Heq]
Heq_JMeq [lemma, in Heq.Heq]
Heq_proj1 [lemma, in Heq.Heq]
Heq_proj1_conj [lemma, in Heq.Heq]
Heq_proj2 [lemma, in Heq.Heq]
Heq_sigT [lemma, in Heq.Heq]
Heq_split [lemma, in Heq.Heq]
Hfun [lemma, in Heq.Heq]
Hfundep [lemma, in Heq.Heq]
HHideConcl [definition, in Heq.Heq]
HId [definition, in Heq.Heq]
hide_evars_example [lemma, in tutorial]
hresolve_arg [definition, in Heq.Heq]
Hrf [lemma, in Heq.Heq]
Hrfgen [lemma, in Heq.Heq]
HrfI [lemma, in Heq.Heq]
Hrw [lemma, in Heq.Heq]
HSetConcl [definition, in Heq.Heq]
HSetConcl0 [definition, in Heq.Heq]
Hty [definition, in Heq.Heq]
htyeq [definition, in Heq.Heq]
HType [definition, in Heq.Heq]
I
idMap [definition, in sysf]idren [definition, in sysf]
idRen [definition, in sysf]
idSub [definition, in sysf]
idsub [definition, in sysf]
idSub_SS [lemma, in sysf]
idsub_ss [lemma, in sysf]
idtemp [definition, in Heq.Heq]
iff_implies_eq [lemma, in strnorm]
In [definition, in tutorial]
inv_convert_tapp [lemma, in strnorm]
in_app_or [lemma, in tutorial]
in_or_app [lemma, in tutorial]
L
LAM [constructor, in sysf]lelistA [abbreviation, in MergesortList]
lelistA [abbreviation, in MergesortVector]
lelistA_inv [abbreviation, in MergesortVector]
lelistA_inv [abbreviation, in MergesortList]
liftMap [definition, in sysf]
liftMap_MR [lemma, in sysf]
liftMap_succ [lemma, in sysf]
LocallySorted [inductive, in MergesortList]
LocallySorted [inductive, in MergesortVector]
LSorted_consn [constructor, in MergesortList]
LSorted_consn [constructor, in MergesortVector]
LSorted_cons1 [constructor, in MergesortList]
LSorted_cons1 [constructor, in MergesortVector]
LSorted_nil [constructor, in MergesortList]
LSorted_nil [constructor, in MergesortVector]
M
map [definition, in tutorial]Map [section, in Vector]
Map [section, in tutorial]
mapExp [definition, in sysf]
mapExp_MR [lemma, in sysf]
mapH [definition, in tutorial]
MapH [section, in tutorial]
MapH.F [variable, in tutorial]
MapH.f [variable, in tutorial]
MapH.P [variable, in tutorial]
MapH.Q [variable, in tutorial]
MapH.U [variable, in tutorial]
MapH.V [variable, in tutorial]
MapOps [record, in sysf]
mapT [definition, in sysf]
MapT [definition, in sysf]
Map.A [variable, in tutorial]
Map.A [variable, in Vector]
Map.B [variable, in tutorial]
Map.B [variable, in Vector]
Map.f [variable, in Vector]
Map.f [variable, in tutorial]
Map_extensional [lemma, in sysf]
map_extensional [lemma, in sysf]
matchbug [definition, in Heq.Heq]
matchbug_elmt [definition, in Heq.Heq]
matchbug_fix [definition, in Heq.Heq]
matchbug_sig [definition, in Heq.Heq]
Matrix [section, in tutorial]
matrix [definition, in tutorial]
MatrixH [section, in tutorial]
matrixH [definition, in tutorial]
MatrixH.P [variable, in tutorial]
MatrixH.U [variable, in tutorial]
Matrix.A [variable, in tutorial]
matU [abbreviation, in tutorial]
mcr [definition, in sysf]
MCR [definition, in sysf]
MergesortList [library]
MergesortVector [library]
minus_n_O [lemma, in Vector]
N
NatOrder [module, in MergesortList]NatOrder [module, in MergesortVector]
NatOrder.A [definition, in MergesortVector]
NatOrder.A [definition, in MergesortList]
NatOrder.le_bool [definition, in MergesortVector]
NatOrder.le_bool [definition, in MergesortList]
NatOrder.le_bool_total [lemma, in MergesortVector]
NatOrder.le_bool_total [lemma, in MergesortList]
NatSeq [section, in Vector]
NatSort [module, in MergesortList]
NatSort [module, in MergesortVector]
neutral [definition, in strnorm]
nil [constructor, in tutorial]
nilH [constructor, in tutorial]
nilMap [definition, in sysf]
nilMap_eq [lemma, in sysf]
nil_leA [abbreviation, in MergesortVector]
nil_leA [abbreviation, in MergesortList]
nil_sort [abbreviation, in MergesortList]
nil_sort [abbreviation, in MergesortVector]
NoDup [inductive, in tutorial]
NoDup_cons [constructor, in tutorial]
NoDup_cons [constructor, in Vector]
NoDup_nil [constructor, in tutorial]
NoDup_nil [constructor, in Vector]
NoDup_remove_1 [lemma, in tutorial]
normal [definition, in strnorm]
n1n2_Sn [definition, in tutorial]
n1n2_SnHN [definition, in tutorial]
n_Spred [definition, in tutorial]
P
permHN_nil [constructor, in tutorial]permHN_skip [constructor, in tutorial]
permHN_swap [constructor, in tutorial]
permHN_trans [constructor, in tutorial]
permH_nil [constructor, in tutorial]
permH_skip [constructor, in tutorial]
permH_swap [constructor, in tutorial]
permH_trans [constructor, in tutorial]
permN_nil [constructor, in tutorial]
permN_skip [constructor, in tutorial]
permN_swap [constructor, in tutorial]
permN_trans [constructor, in tutorial]
Permutation [inductive, in tutorial]
PermutationH [inductive, in tutorial]
PermutationHN [inductive, in tutorial]
PermutationHN_app_swap [lemma, in tutorial]
PermutationHN_cons_app [lemma, in tutorial]
PermutationHN_refl [lemma, in tutorial]
PermutationHN_sym [lemma, in tutorial]
PermutationH_app_swap [lemma, in tutorial]
PermutationH_cons_app [lemma, in tutorial]
PermutationH_refl [lemma, in tutorial]
PermutationH_sym [lemma, in tutorial]
PermutationN [inductive, in tutorial]
PermutationN_app_swap [lemma, in tutorial]
PermutationN_cons_app [lemma, in tutorial]
PermutationN_refl [lemma, in tutorial]
PermutationN_sym [lemma, in tutorial]
Permutation_app_swap [lemma, in tutorial]
Permutation_cons_app [lemma, in tutorial]
Permutation_refl [lemma, in tutorial]
Permutation_sym [lemma, in tutorial]
perm_nil [constructor, in tutorial]
perm_nil [constructor, in Vector]
perm_skip [constructor, in tutorial]
perm_skip [constructor, in Vector]
perm_swap [constructor, in Vector]
perm_swap [constructor, in tutorial]
perm_trans [constructor, in Vector]
perm_trans [constructor, in tutorial]
PExp [abbreviation, in sysf]
plus_assoc [definition, in Vector]
plus_comm [definition, in tutorial]
plus_comm [definition, in Vector]
plus_commHN [definition, in tutorial]
plus_n_O [definition, in tutorial]
plus_n_O [definition, in Vector]
plus_Snm_nSm [definition, in Vector]
plus_Snm_nSm [definition, in tutorial]
PMap [abbreviation, in sysf]
Pmat [abbreviation, in tutorial]
Pmat [abbreviation, in tutorial]
PmatH [abbreviation, in tutorial]
PmatH [abbreviation, in tutorial]
power [definition, in Vector]
PPredExpList [abbreviation, in strnorm]
Pred [definition, in strnorm]
PredExp [definition, in strnorm]
PredExpList [definition, in strnorm]
PRen [abbreviation, in sysf]
proj2m [definition, in strnorm]
proj3 [definition, in strnorm]
proj3m [definition, in strnorm]
proj4 [definition, in strnorm]
proj4m [definition, in strnorm]
proj5 [definition, in strnorm]
PSub [abbreviation, in sysf]
PVar [abbreviation, in sysf]
PvecH [abbreviation, in tutorial]
PvecH [abbreviation, in tutorial]
R
RCS [definition, in sysf]rcs [definition, in sysf]
RC_arrow [definition, in strnorm]
RC_arrow_is_CR [lemma, in strnorm]
RED [definition, in strnorm]
REDC [lemma, in strnorm]
REDC2 [lemma, in strnorm]
REDC3 [lemma, in strnorm]
ReDun [section, in Vector]
ReDun.A [variable, in Vector]
RED_Hcong [lemma, in strnorm]
RED_is_CR [lemma, in strnorm]
RED_LAM [lemma, in strnorm]
RED_renaming [lemma, in strnorm]
RED_substitution [lemma, in strnorm]
RED_TABS [lemma, in strnorm]
RED_TAPP [lemma, in strnorm]
refl_Heq [lemma, in Heq.Heq]
Rel [definition, in strnorm]
RenExp [definition, in sysf]
RenExp_def [lemma, in sysf]
renL [definition, in sysf]
RenL [definition, in sysf]
renL_rr [lemma, in sysf]
RenL_succ [lemma, in sysf]
RenMap [definition, in sysf]
RenT [definition, in sysf]
renT [definition, in sysf]
renTy [definition, in sysf]
renTy_def [lemma, in sysf]
renTy_rr [lemma, in sysf]
rev [definition, in tutorial]
revappC [lemma, in tutorial]
revH [definition, in tutorial]
rev_append [definition, in tutorial]
rev_appendH [definition, in tutorial]
rev_append_rev [lemma, in tutorial]
rev_append_revH [lemma, in tutorial]
RTS [definition, in sysf]
rts [definition, in sysf]
RTS_idRen [lemma, in sysf]
RTS_RenL [lemma, in sysf]
rts_renL [lemma, in sysf]
RTS_SS [lemma, in sysf]
RTS_subRen [lemma, in sysf]
S
sb [projection, in sysf]SCS [definition, in sysf]
scs [definition, in sysf]
SetIncl [section, in Vector]
SetIncl.A [variable, in Vector]
set_concl_example [lemma, in tutorial]
SExp [definition, in sysf]
shren [definition, in sysf]
shsub [definition, in sysf]
shSub [definition, in sysf]
shSub_simpl [lemma, in sysf]
sigT_eta [lemma, in Heq.Heq]
SimpleMergeExample [definition, in MergesortVector]
SimpleMergeExample [definition, in MergesortList]
simpl_hyps_example [lemma, in tutorial]
simulation [definition, in strnorm]
SMap [definition, in sysf]
Smat [definition, in tutorial]
SmatH [definition, in tutorial]
SN [inductive, in strnorm]
SNRC [definition, in strnorm]
SNRC_is_CR [lemma, in strnorm]
SN_APP_1 [lemma, in strnorm]
SN_by_simulation [lemma, in strnorm]
SN_convert [lemma, in strnorm]
sn_next [constructor, in strnorm]
SN_sub [lemma, in strnorm]
SN_subst [lemma, in strnorm]
SN_TAPP [lemma, in strnorm]
Sort [module, in MergesortList]
Sort [module, in MergesortVector]
sort [abbreviation, in MergesortVector]
sort [abbreviation, in MergesortList]
Sorted [inductive, in MergesortVector]
Sorted [inductive, in MergesortList]
Sorted_cons [constructor, in MergesortList]
Sorted_cons [constructor, in MergesortVector]
Sorted_extends [lemma, in MergesortList]
Sorted_extends [lemma, in MergesortVector]
Sorted_inv [lemma, in MergesortVector]
Sorted_inv [lemma, in MergesortList]
Sorted_LocallySorted_iff [lemma, in MergesortList]
Sorted_LocallySorted_iff [lemma, in MergesortVector]
Sorted_nil [constructor, in MergesortVector]
Sorted_nil [constructor, in MergesortList]
Sorted_rect [lemma, in MergesortList]
Sorted_rect [lemma, in MergesortVector]
Sorted_StronglySorted [lemma, in MergesortVector]
Sorted_StronglySorted [lemma, in MergesortList]
Sort.flatten_stack [definition, in MergesortList]
Sort.flatten_stack [definition, in MergesortVector]
Sort.iter_merge [definition, in MergesortList]
Sort.iter_merge [definition, in MergesortVector]
Sort.LocallySorted_sort [lemma, in MergesortList]
Sort.LocallySorted_sort [lemma, in MergesortVector]
Sort.merge [definition, in MergesortList]
Sort.merge [definition, in MergesortVector]
Sort.merge_list_to_stack [definition, in MergesortVector]
Sort.merge_list_to_stack [definition, in MergesortList]
Sort.merge_stack [definition, in MergesortVector]
Sort.merge_stack [definition, in MergesortList]
Sort.Permuted_iter_merge [lemma, in MergesortList]
Sort.Permuted_iter_merge [lemma, in MergesortVector]
Sort.Permuted_merge [lemma, in MergesortList]
Sort.Permuted_merge [lemma, in MergesortVector]
Sort.Permuted_merge_list_to_stack [lemma, in MergesortList]
Sort.Permuted_merge_list_to_stack [lemma, in MergesortVector]
Sort.Permuted_merge_stack [lemma, in MergesortVector]
Sort.Permuted_merge_stack [lemma, in MergesortList]
Sort.Permuted_sort [lemma, in MergesortVector]
Sort.Permuted_sort [lemma, in MergesortList]
Sort.Pstk [abbreviation, in MergesortVector]
Sort.SconsNone [constructor, in MergesortVector]
Sort.SconsSome [constructor, in MergesortVector]
Sort.Snil [constructor, in MergesortVector]
Sort.sort [definition, in MergesortVector]
Sort.sort [definition, in MergesortList]
Sort.SortedB [abbreviation, in MergesortList]
Sort.SortedB [abbreviation, in MergesortVector]
Sort.SortedStack [definition, in MergesortList]
Sort.SortedStack [definition, in MergesortVector]
Sort.Sorted_iter_merge [lemma, in MergesortList]
Sort.Sorted_iter_merge [lemma, in MergesortVector]
Sort.Sorted_merge [lemma, in MergesortVector]
Sort.Sorted_merge [lemma, in MergesortList]
Sort.Sorted_merge_list_to_stack [lemma, in MergesortList]
Sort.Sorted_merge_list_to_stack [lemma, in MergesortVector]
Sort.Sorted_merge_stack [lemma, in MergesortList]
Sort.Sorted_merge_stack [lemma, in MergesortVector]
Sort.Sorted_sort [lemma, in MergesortList]
Sort.Sorted_sort [lemma, in MergesortVector]
Sort.Sstk [definition, in MergesortVector]
Sort.Stack [inductive, in MergesortVector]
Sort.StronglySorted_sort [lemma, in MergesortVector]
Sort.StronglySorted_sort [lemma, in MergesortList]
sort_inv [abbreviation, in MergesortList]
sort_inv [abbreviation, in MergesortVector]
sort_rect [abbreviation, in MergesortVector]
sort_rect [abbreviation, in MergesortList]
SPredExpList [definition, in strnorm]
SRen [definition, in sysf]
SSorted_cons [constructor, in MergesortVector]
SSorted_cons [constructor, in MergesortList]
SSorted_nil [constructor, in MergesortList]
SSorted_nil [constructor, in MergesortVector]
sss_assoc [lemma, in sysf]
SSS_assoc [lemma, in sysf]
SSub [definition, in sysf]
SS_idSub [lemma, in sysf]
ss_idsub [lemma, in sysf]
strnorm [library]
StronglySorted [inductive, in MergesortVector]
StronglySorted [inductive, in MergesortList]
StronglySorted_inv [lemma, in MergesortVector]
StronglySorted_inv [lemma, in MergesortList]
StronglySorted_rec [lemma, in MergesortList]
StronglySorted_rec [lemma, in MergesortVector]
StronglySorted_rect [lemma, in MergesortVector]
StronglySorted_rect [lemma, in MergesortList]
StronglySorted_Sorted [lemma, in MergesortList]
StronglySorted_Sorted [lemma, in MergesortVector]
StrongNormalization [lemma, in strnorm]
subE [definition, in sysf]
SubExp [definition, in sysf]
subExp [definition, in sysf]
subExpC1 [definition, in sysf]
subExpC2 [definition, in sysf]
SubExp_idSub [lemma, in sysf]
subExp_idsub [lemma, in sysf]
subExp_RenExp [lemma, in sysf]
SubExp_RS [lemma, in sysf]
subExp_ss [lemma, in sysf]
SubExp_SS [lemma, in sysf]
subExp_SubExp [lemma, in sysf]
SubExp_subExp_TAPP [lemma, in sysf]
subE_idsub [lemma, in sysf]
subE_length [lemma, in sysf]
subE_ss [lemma, in sysf]
subL [definition, in sysf]
SubL [definition, in sysf]
SubL_idSub [lemma, in sysf]
subL_idsub [lemma, in sysf]
subL_rs [lemma, in sysf]
SubL_RS [lemma, in sysf]
subL_shsub [lemma, in sysf]
SubL_shSub [lemma, in sysf]
subL_sr [lemma, in sysf]
subL_ss [lemma, in sysf]
SubL_SS [lemma, in sysf]
SubL_succ [lemma, in sysf]
subL_succ [lemma, in sysf]
SubMap [definition, in sysf]
subRen [definition, in sysf]
subRen_RenL [lemma, in sysf]
subRen_ss [lemma, in sysf]
subRen_subVar [lemma, in sysf]
substMap [definition, in sysf]
substMap_MR [lemma, in sysf]
substMap_subVar [lemma, in sysf]
subSub [definition, in sysf]
subSub_consMap [lemma, in sysf]
subSub_dropSub [lemma, in sysf]
subSub_idSub [lemma, in sysf]
subSub_idsub [lemma, in sysf]
subSub_RS [lemma, in sysf]
subSub_shSub [lemma, in sysf]
subSub_SS [lemma, in sysf]
subSub_ss [lemma, in sysf]
subSub_SubL [lemma, in sysf]
subSub_subVar [lemma, in sysf]
subT [definition, in sysf]
SubT [definition, in sysf]
subTy [definition, in sysf]
subTy_idsub [lemma, in sysf]
subTy_rs [lemma, in sysf]
subTy_sr [lemma, in sysf]
subTy_ss [lemma, in sysf]
subVar [definition, in sysf]
subVar_idsub [lemma, in sysf]
subVar_ss [lemma, in sysf]
subVar_succ [lemma, in sysf]
Sub_singSub [lemma, in sysf]
sub_singsub [lemma, in sysf]
SVAR [constructor, in sysf]
sVAR [constructor, in sysf]
SVar [definition, in sysf]
Svec [definition, in Vector]
Svec [definition, in tutorial]
SvecH [definition, in tutorial]
sym_Heq [lemma, in Heq.Heq]
sysf [library]
T
TABS [constructor, in sysf]tail [definition, in tutorial]
tailH [definition, in tutorial]
TAPP [constructor, in sysf]
tlcol [definition, in tutorial]
tlcolH [definition, in tutorial]
tlconscol [lemma, in tutorial]
tlconscolH [lemma, in tutorial]
tlConsMap [lemma, in sysf]
tlMap [definition, in sysf]
tlMap_substMap [lemma, in sysf]
tlMap_subSub [lemma, in sysf]
TotalOrder [module, in MergesortList]
TotalOrder [module, in MergesortVector]
TotalOrder.A [axiom, in MergesortVector]
TotalOrder.A [axiom, in MergesortList]
TotalOrder.le_bool [axiom, in MergesortList]
TotalOrder.le_bool [axiom, in MergesortVector]
TotalOrder.le_bool_total [axiom, in MergesortVector]
TotalOrder.le_bool_total [axiom, in MergesortList]
trans_Heq [lemma, in Heq.Heq]
tuple_split [lemma, in Heq.Heq]
tutorial [library]
Ty [inductive, in sysf]
TYVAR [constructor, in sysf]
U
UnivVar [definition, in strnorm]V
vapp [definition, in Vector]vapp_ass [lemma, in Vector]
vapp_comm_cons [lemma, in Vector]
vapp_cons_not_nil [lemma, in Vector]
vapp_eq_nil [lemma, in Vector]
vapp_eq_unit [lemma, in Vector]
vapp_inj_head [lemma, in Vector]
vapp_inj_tail [lemma, in Vector]
vapp_inv_head [lemma, in Vector]
vapp_inv_tail [lemma, in Vector]
vapp_nil_end [lemma, in Vector]
vapp_nth1 [lemma, in Vector]
vapp_nth2 [lemma, in Vector]
vapp_removelast_last [lemma, in Vector]
VAR [constructor, in sysf]
VariableDomainMap [section, in sysf]
VariableDomainMap.ops [variable, in sysf]
VariableDomainMap.P [variable, in sysf]
varsp [definition, in strnorm]
varT [inductive, in sysf]
VarT [inductive, in sysf]
Var_inv [lemma, in sysf]
vass_app [lemma, in Vector]
vcombine [definition, in Vector]
vcombine_nth [lemma, in Vector]
vcombine_split [lemma, in Vector]
vcons [constructor, in Vector]
vcount_occ [definition, in Vector]
vcount_occ_In [lemma, in Vector]
vcount_occ_inv_nil [lemma, in Vector]
vcount_occ_nil [lemma, in Vector]
vdistr_rev [lemma, in Vector]
VDMap [definition, in sysf]
vec [abbreviation, in Vector]
vec [abbreviation, in Vector]
vec [abbreviation, in Vector]
vec [abbreviation, in Vector]
vec [abbreviation, in Vector]
vec [abbreviation, in tutorial]
vec [abbreviation, in Vector]
vec [abbreviation, in Vector]
vecH [abbreviation, in tutorial]
Vector [section, in tutorial]
vector [inductive, in Vector]
vector [inductive, in tutorial]
Vector [library]
vectorH [inductive, in tutorial]
VectorH [section, in tutorial]
VectorH.P [variable, in tutorial]
VectorH.U [variable, in tutorial]
VectorOps [section, in Vector]
VectorOps.A [variable, in Vector]
VectorOps.eqA_dec [variable, in Vector]
VectorOps.Permutation [section, in Vector]
VectorOps.Reverse_Induction [section, in Vector]
VectorPairs [section, in Vector]
VectorPairs.A [variable, in Vector]
VectorPairs.B [variable, in Vector]
Vectors [section, in Vector]
Vectors.A [variable, in Vector]
Vector.A [variable, in tutorial]
vector_eq_dec [lemma, in Vector]
vector_power [definition, in Vector]
vector_prod [definition, in Vector]
vecU [abbreviation, in tutorial]
vecU [abbreviation, in tutorial]
vexistsb [definition, in Vector]
vexistsb_exists [lemma, in Vector]
vexistsb_nth [lemma, in Vector]
vexists_last [lemma, in Vector]
vfilter [definition, in Vector]
vfilter_In [lemma, in Vector]
vfind [definition, in Vector]
vfirstn [definition, in Vector]
vfirstn_removelast [lemma, in Vector]
vfirstn_skipn [lemma, in Vector]
vflat_map [definition, in Vector]
vfold_left [definition, in Vector]
vfold_left_app [lemma, in Vector]
vfold_left_length [lemma, in Vector]
vfold_left_rev_right [lemma, in Vector]
vfold_right [definition, in Vector]
vfold_right_app [lemma, in Vector]
vfold_symmetric [lemma, in Vector]
vforallb [definition, in Vector]
vforallb_forall [lemma, in Vector]
vhd [definition, in Vector]
vhdtail [lemma, in Vector]
vhead [definition, in Vector]
vhead_cons [lemma, in Vector]
vhead_nil [lemma, in Vector]
VIn [definition, in Vector]
vincl [definition, in Vector]
vincl_app [lemma, in Vector]
vincl_appl [lemma, in Vector]
vincl_appr [lemma, in Vector]
vincl_cons [lemma, in Vector]
vincl_refl [lemma, in Vector]
vincl_tl [lemma, in Vector]
vincl_tran [lemma, in Vector]
vin_app_or [lemma, in Vector]
vin_combine_l [lemma, in Vector]
vin_combine_r [lemma, in Vector]
vin_cons [lemma, in Vector]
VIn_dec [lemma, in Vector]
vin_eq [lemma, in Vector]
vin_flat_map [lemma, in Vector]
vin_inv [lemma, in Vector]
vin_map [lemma, in Vector]
vin_map_iff [lemma, in Vector]
vin_nil [lemma, in Vector]
vin_or_app [lemma, in Vector]
vin_prod [lemma, in Vector]
vin_prod_aux [lemma, in Vector]
vin_prod_iff [lemma, in Vector]
VIn_rev [lemma, in Vector]
VIn_split [lemma, in Vector]
vin_split_l [lemma, in Vector]
vin_split_r [lemma, in Vector]
vl [projection, in sysf]
vlast [definition, in Vector]
vmap [definition, in Vector]
vmap_app [lemma, in Vector]
vmap_ext [lemma, in Vector]
vmap_map [lemma, in Vector]
vmap_nth [lemma, in Vector]
vmap_rev [lemma, in Vector]
vnil [constructor, in Vector]
vnil_cons [lemma, in Vector]
VNoDup [inductive, in Vector]
VNoDup_Permutation [lemma, in Vector]
VNoDup_remove_1 [lemma, in Vector]
VNoDup_remove_2 [lemma, in Vector]
vnth [definition, in Vector]
vnth_default [definition, in Vector]
vnth_error [definition, in Vector]
vnth_In [lemma, in Vector]
vnth_indep [lemma, in Vector]
vnth_in_or_default [lemma, in Vector]
vnth_ok [definition, in Vector]
vnth_overflow [lemma, in Vector]
vnth_S_cons [lemma, in Vector]
vpartition [definition, in Vector]
VPermutation [inductive, in Vector]
VPermutation_app [lemma, in Vector]
VPermutation_app_head [lemma, in Vector]
VPermutation_app_inv [lemma, in Vector]
VPermutation_app_inv_l [lemma, in Vector]
VPermutation_app_inv_r [lemma, in Vector]
VPermutation_app_swap [lemma, in Vector]
VPermutation_app_tail [lemma, in Vector]
VPermutation_cons_app [lemma, in Vector]
VPermutation_cons_app_inv [lemma, in Vector]
VPermutation_cons_inv [lemma, in Vector]
VPermutation_in [lemma, in Vector]
VPermutation_ind_bis [lemma, in Vector]
VPermutation_length [lemma, in Vector]
VPermutation_map [lemma, in Vector]
VPermutation_nil [lemma, in Vector]
VPermutation_nil_cons [lemma, in Vector]
VPermutation_refl [lemma, in Vector]
VPermutation_rev [lemma, in Vector]
VPermutation_sym [lemma, in Vector]
VPermutation_trans [lemma, in Vector]
vr [projection, in sysf]
vremove [definition, in Vector]
vremovelast [definition, in Vector]
vremovelast_app [lemma, in Vector]
vremovelast_firstn [lemma, in Vector]
vremove_In [lemma, in Vector]
vrev [definition, in Vector]
vrev' [definition, in Vector]
vrev_acc [abbreviation, in Vector]
vrev_acc_rev [abbreviation, in Vector]
vrev_alt [lemma, in Vector]
vrev_append [definition, in Vector]
vrev_append_rev [lemma, in Vector]
vrev_ind [lemma, in Vector]
vrev_involutive [lemma, in Vector]
vrev_nth [lemma, in Vector]
vrev_unit [lemma, in Vector]
vrev_vector_ind [lemma, in Vector]
vseq [definition, in Vector]
vseq_nth [lemma, in Vector]
vseq_shift [lemma, in Vector]
vskipn [definition, in Vector]
vsplit [definition, in Vector]
vsplit_combine [lemma, in Vector]
vsplit_nth [lemma, in Vector]
vtail [definition, in Vector]
W
wk [projection, in sysf]Z
ZVAR [constructor, in sysf]zVAR [constructor, in sysf]
Projection Index
S
sb [in sysf]V
vl [in sysf]vr [in sysf]
W
wk [in sysf]Record Index
M
MapOps [in sysf]Lemma Index
A
appmatcol_assoc [in tutorial]appmatcol_assocH [in tutorial]
appmatrow_assoc [in tutorial]
appmatrow_assocH [in tutorial]
app_ass [in tutorial]
app_assH [in tutorial]
app_nil [in tutorial]
app_nilH [in tutorial]
C
cast_compose [in Heq.Heq]cast_elim [in Heq.Heq]
cast_elim_r [in Heq.Heq]
cast_intro [in Heq.Heq]
cast_intro_r [in Heq.Heq]
conshdtlcol [in tutorial]
conshdtlcolH [in tutorial]
consMapInv [in sysf]
consmap_shsub [in sysf]
consMap_shSub [in sysf]
consMap_SubL [in sysf]
consmap_subL [in sysf]
consMap_succ [in sysf]
consPredExp_hd [in strnorm]
consPredExp_is_CR [in strnorm]
consPredExp_tl [in strnorm]
convert_sub [in strnorm]
convert_subst [in strnorm]
count_occ_cons_eq [in Vector]
count_occ_cons_neq [in Vector]
CR4 [in strnorm]
D
destruct_vector [in Vector]distr_rev [in tutorial]
distr_revH [in tutorial]
E
eq_Heq [in Heq.Heq]eq_HeqI [in Heq.Heq]
eq_implies_iff [in strnorm]
F
Forall_impl [in MergesortList]Forall_impl [in MergesortVector]
Fundamental [in strnorm]
H
Happ [in Heq.Heq]Happdep [in Heq.Heq]
hdconscol [in tutorial]
hdconscolH [in tutorial]
hdConsMap [in sysf]
hdMap_substMap [in sysf]
hdMap_subSub [in sysf]
HdRel_inv [in MergesortList]
HdRel_inv [in MergesortVector]
hdtail [in tutorial]
hdtailH [in tutorial]
Heq_eq [in Heq.Heq]
Heq_eqI [in Heq.Heq]
Heq_eq_dep [in Heq.Heq]
Heq_extensionality [in Heq.Heq]
Heq_fold [in Heq.Heq]
Heq_ind_gen [in Heq.Heq]
Heq_JMeq [in Heq.Heq]
Heq_proj1 [in Heq.Heq]
Heq_proj1_conj [in Heq.Heq]
Heq_proj2 [in Heq.Heq]
Heq_sigT [in Heq.Heq]
Heq_split [in Heq.Heq]
Hfun [in Heq.Heq]
Hfundep [in Heq.Heq]
hide_evars_example [in tutorial]
Hrf [in Heq.Heq]
Hrfgen [in Heq.Heq]
HrfI [in Heq.Heq]
Hrw [in Heq.Heq]
I
idSub_SS [in sysf]idsub_ss [in sysf]
iff_implies_eq [in strnorm]
inv_convert_tapp [in strnorm]
in_app_or [in tutorial]
in_or_app [in tutorial]
L
liftMap_MR [in sysf]liftMap_succ [in sysf]
M
mapExp_MR [in sysf]Map_extensional [in sysf]
map_extensional [in sysf]
minus_n_O [in Vector]
N
NatOrder.le_bool_total [in MergesortVector]NatOrder.le_bool_total [in MergesortList]
nilMap_eq [in sysf]
NoDup_remove_1 [in tutorial]
P
PermutationHN_app_swap [in tutorial]PermutationHN_cons_app [in tutorial]
PermutationHN_refl [in tutorial]
PermutationHN_sym [in tutorial]
PermutationH_app_swap [in tutorial]
PermutationH_cons_app [in tutorial]
PermutationH_refl [in tutorial]
PermutationH_sym [in tutorial]
PermutationN_app_swap [in tutorial]
PermutationN_cons_app [in tutorial]
PermutationN_refl [in tutorial]
PermutationN_sym [in tutorial]
Permutation_app_swap [in tutorial]
Permutation_cons_app [in tutorial]
Permutation_refl [in tutorial]
Permutation_sym [in tutorial]
R
RC_arrow_is_CR [in strnorm]REDC [in strnorm]
REDC2 [in strnorm]
REDC3 [in strnorm]
RED_Hcong [in strnorm]
RED_is_CR [in strnorm]
RED_LAM [in strnorm]
RED_renaming [in strnorm]
RED_substitution [in strnorm]
RED_TABS [in strnorm]
RED_TAPP [in strnorm]
refl_Heq [in Heq.Heq]
RenExp_def [in sysf]
renL_rr [in sysf]
RenL_succ [in sysf]
renTy_def [in sysf]
renTy_rr [in sysf]
revappC [in tutorial]
rev_append_rev [in tutorial]
rev_append_revH [in tutorial]
RTS_idRen [in sysf]
RTS_RenL [in sysf]
rts_renL [in sysf]
RTS_SS [in sysf]
RTS_subRen [in sysf]
S
set_concl_example [in tutorial]shSub_simpl [in sysf]
sigT_eta [in Heq.Heq]
simpl_hyps_example [in tutorial]
SNRC_is_CR [in strnorm]
SN_APP_1 [in strnorm]
SN_by_simulation [in strnorm]
SN_convert [in strnorm]
SN_sub [in strnorm]
SN_subst [in strnorm]
SN_TAPP [in strnorm]
Sorted_extends [in MergesortList]
Sorted_extends [in MergesortVector]
Sorted_inv [in MergesortVector]
Sorted_inv [in MergesortList]
Sorted_LocallySorted_iff [in MergesortList]
Sorted_LocallySorted_iff [in MergesortVector]
Sorted_rect [in MergesortList]
Sorted_rect [in MergesortVector]
Sorted_StronglySorted [in MergesortVector]
Sorted_StronglySorted [in MergesortList]
Sort.LocallySorted_sort [in MergesortList]
Sort.LocallySorted_sort [in MergesortVector]
Sort.Permuted_iter_merge [in MergesortList]
Sort.Permuted_iter_merge [in MergesortVector]
Sort.Permuted_merge [in MergesortList]
Sort.Permuted_merge [in MergesortVector]
Sort.Permuted_merge_list_to_stack [in MergesortList]
Sort.Permuted_merge_list_to_stack [in MergesortVector]
Sort.Permuted_merge_stack [in MergesortVector]
Sort.Permuted_merge_stack [in MergesortList]
Sort.Permuted_sort [in MergesortVector]
Sort.Permuted_sort [in MergesortList]
Sort.Sorted_iter_merge [in MergesortList]
Sort.Sorted_iter_merge [in MergesortVector]
Sort.Sorted_merge [in MergesortVector]
Sort.Sorted_merge [in MergesortList]
Sort.Sorted_merge_list_to_stack [in MergesortList]
Sort.Sorted_merge_list_to_stack [in MergesortVector]
Sort.Sorted_merge_stack [in MergesortList]
Sort.Sorted_merge_stack [in MergesortVector]
Sort.Sorted_sort [in MergesortList]
Sort.Sorted_sort [in MergesortVector]
Sort.StronglySorted_sort [in MergesortVector]
Sort.StronglySorted_sort [in MergesortList]
sss_assoc [in sysf]
SSS_assoc [in sysf]
SS_idSub [in sysf]
ss_idsub [in sysf]
StronglySorted_inv [in MergesortVector]
StronglySorted_inv [in MergesortList]
StronglySorted_rec [in MergesortList]
StronglySorted_rec [in MergesortVector]
StronglySorted_rect [in MergesortVector]
StronglySorted_rect [in MergesortList]
StronglySorted_Sorted [in MergesortList]
StronglySorted_Sorted [in MergesortVector]
StrongNormalization [in strnorm]
SubExp_idSub [in sysf]
subExp_idsub [in sysf]
subExp_RenExp [in sysf]
SubExp_RS [in sysf]
subExp_ss [in sysf]
SubExp_SS [in sysf]
subExp_SubExp [in sysf]
SubExp_subExp_TAPP [in sysf]
subE_idsub [in sysf]
subE_length [in sysf]
subE_ss [in sysf]
SubL_idSub [in sysf]
subL_idsub [in sysf]
subL_rs [in sysf]
SubL_RS [in sysf]
subL_shsub [in sysf]
SubL_shSub [in sysf]
subL_sr [in sysf]
subL_ss [in sysf]
SubL_SS [in sysf]
SubL_succ [in sysf]
subL_succ [in sysf]
subRen_RenL [in sysf]
subRen_ss [in sysf]
subRen_subVar [in sysf]
substMap_MR [in sysf]
substMap_subVar [in sysf]
subSub_consMap [in sysf]
subSub_dropSub [in sysf]
subSub_idSub [in sysf]
subSub_idsub [in sysf]
subSub_RS [in sysf]
subSub_shSub [in sysf]
subSub_SS [in sysf]
subSub_ss [in sysf]
subSub_SubL [in sysf]
subSub_subVar [in sysf]
subTy_idsub [in sysf]
subTy_rs [in sysf]
subTy_sr [in sysf]
subTy_ss [in sysf]
subVar_idsub [in sysf]
subVar_ss [in sysf]
subVar_succ [in sysf]
Sub_singSub [in sysf]
sub_singsub [in sysf]
sym_Heq [in Heq.Heq]
T
tlconscol [in tutorial]tlconscolH [in tutorial]
tlConsMap [in sysf]
tlMap_substMap [in sysf]
tlMap_subSub [in sysf]
trans_Heq [in Heq.Heq]
tuple_split [in Heq.Heq]
V
vapp_ass [in Vector]vapp_comm_cons [in Vector]
vapp_cons_not_nil [in Vector]
vapp_eq_nil [in Vector]
vapp_eq_unit [in Vector]
vapp_inj_head [in Vector]
vapp_inj_tail [in Vector]
vapp_inv_head [in Vector]
vapp_inv_tail [in Vector]
vapp_nil_end [in Vector]
vapp_nth1 [in Vector]
vapp_nth2 [in Vector]
vapp_removelast_last [in Vector]
Var_inv [in sysf]
vass_app [in Vector]
vcombine_nth [in Vector]
vcombine_split [in Vector]
vcount_occ_In [in Vector]
vcount_occ_inv_nil [in Vector]
vcount_occ_nil [in Vector]
vdistr_rev [in Vector]
vector_eq_dec [in Vector]
vexistsb_exists [in Vector]
vexistsb_nth [in Vector]
vexists_last [in Vector]
vfilter_In [in Vector]
vfirstn_removelast [in Vector]
vfirstn_skipn [in Vector]
vfold_left_app [in Vector]
vfold_left_length [in Vector]
vfold_left_rev_right [in Vector]
vfold_right_app [in Vector]
vfold_symmetric [in Vector]
vforallb_forall [in Vector]
vhdtail [in Vector]
vhead_cons [in Vector]
vhead_nil [in Vector]
vincl_app [in Vector]
vincl_appl [in Vector]
vincl_appr [in Vector]
vincl_cons [in Vector]
vincl_refl [in Vector]
vincl_tl [in Vector]
vincl_tran [in Vector]
vin_app_or [in Vector]
vin_combine_l [in Vector]
vin_combine_r [in Vector]
vin_cons [in Vector]
VIn_dec [in Vector]
vin_eq [in Vector]
vin_flat_map [in Vector]
vin_inv [in Vector]
vin_map [in Vector]
vin_map_iff [in Vector]
vin_nil [in Vector]
vin_or_app [in Vector]
vin_prod [in Vector]
vin_prod_aux [in Vector]
vin_prod_iff [in Vector]
VIn_rev [in Vector]
VIn_split [in Vector]
vin_split_l [in Vector]
vin_split_r [in Vector]
vmap_app [in Vector]
vmap_ext [in Vector]
vmap_map [in Vector]
vmap_nth [in Vector]
vmap_rev [in Vector]
vnil_cons [in Vector]
VNoDup_Permutation [in Vector]
VNoDup_remove_1 [in Vector]
VNoDup_remove_2 [in Vector]
vnth_In [in Vector]
vnth_indep [in Vector]
vnth_in_or_default [in Vector]
vnth_overflow [in Vector]
vnth_S_cons [in Vector]
VPermutation_app [in Vector]
VPermutation_app_head [in Vector]
VPermutation_app_inv [in Vector]
VPermutation_app_inv_l [in Vector]
VPermutation_app_inv_r [in Vector]
VPermutation_app_swap [in Vector]
VPermutation_app_tail [in Vector]
VPermutation_cons_app [in Vector]
VPermutation_cons_app_inv [in Vector]
VPermutation_cons_inv [in Vector]
VPermutation_in [in Vector]
VPermutation_ind_bis [in Vector]
VPermutation_length [in Vector]
VPermutation_map [in Vector]
VPermutation_nil [in Vector]
VPermutation_nil_cons [in Vector]
VPermutation_refl [in Vector]
VPermutation_rev [in Vector]
VPermutation_sym [in Vector]
VPermutation_trans [in Vector]
vremovelast_app [in Vector]
vremovelast_firstn [in Vector]
vremove_In [in Vector]
vrev_alt [in Vector]
vrev_append_rev [in Vector]
vrev_ind [in Vector]
vrev_involutive [in Vector]
vrev_nth [in Vector]
vrev_unit [in Vector]
vrev_vector_ind [in Vector]
vseq_nth [in Vector]
vseq_shift [in Vector]
vsplit_combine [in Vector]
vsplit_nth [in Vector]
Section Index
B
Bool [in Vector]C
CompMR [in sysf]Cutting [in Vector]
D
defs [in MergesortVector]defs [in MergesortList]
E
Elts [in Vector]Elts.Remove [in Vector]
F
Facts [in Vector]Fold_Left_Recursor [in Vector]
Fold_Right_Recursor [in Vector]
M
Map [in Vector]Map [in tutorial]
MapH [in tutorial]
Matrix [in tutorial]
MatrixH [in tutorial]
N
NatSeq [in Vector]R
ReDun [in Vector]S
SetIncl [in Vector]V
VariableDomainMap [in sysf]Vector [in tutorial]
VectorH [in tutorial]
VectorOps [in Vector]
VectorOps.Permutation [in Vector]
VectorOps.Reverse_Induction [in Vector]
VectorPairs [in Vector]
Vectors [in Vector]
Constructor Index
A
ALL [in sysf]APP [in sysf]
ARR [in sysf]
C
cons [in tutorial]consH [in tutorial]
c_app [in strnorm]
c_cong_app_1 [in strnorm]
c_cong_app_2 [in strnorm]
c_cong_lam [in strnorm]
c_cong_tabs [in strnorm]
c_cong_tapp [in strnorm]
c_tapp [in strnorm]
F
Forall_cons [in MergesortVector]Forall_cons [in MergesortList]
Forall_nil [in MergesortVector]
Forall_nil [in MergesortList]
H
HdRel_cons [in MergesortList]HdRel_cons [in MergesortVector]
HdRel_nil [in MergesortList]
HdRel_nil [in MergesortVector]
L
LAM [in sysf]LSorted_consn [in MergesortList]
LSorted_consn [in MergesortVector]
LSorted_cons1 [in MergesortList]
LSorted_cons1 [in MergesortVector]
LSorted_nil [in MergesortList]
LSorted_nil [in MergesortVector]
N
nil [in tutorial]nilH [in tutorial]
NoDup_cons [in tutorial]
NoDup_cons [in Vector]
NoDup_nil [in tutorial]
NoDup_nil [in Vector]
P
permHN_nil [in tutorial]permHN_skip [in tutorial]
permHN_swap [in tutorial]
permHN_trans [in tutorial]
permH_nil [in tutorial]
permH_skip [in tutorial]
permH_swap [in tutorial]
permH_trans [in tutorial]
permN_nil [in tutorial]
permN_skip [in tutorial]
permN_swap [in tutorial]
permN_trans [in tutorial]
perm_nil [in tutorial]
perm_nil [in Vector]
perm_skip [in tutorial]
perm_skip [in Vector]
perm_swap [in Vector]
perm_swap [in tutorial]
perm_trans [in Vector]
perm_trans [in tutorial]
S
sn_next [in strnorm]Sorted_cons [in MergesortList]
Sorted_cons [in MergesortVector]
Sorted_nil [in MergesortVector]
Sorted_nil [in MergesortList]
Sort.SconsNone [in MergesortVector]
Sort.SconsSome [in MergesortVector]
Sort.Snil [in MergesortVector]
SSorted_cons [in MergesortVector]
SSorted_cons [in MergesortList]
SSorted_nil [in MergesortList]
SSorted_nil [in MergesortVector]
SVAR [in sysf]
sVAR [in sysf]
T
TABS [in sysf]TAPP [in sysf]
TYVAR [in sysf]
V
VAR [in sysf]vcons [in Vector]
vnil [in Vector]
Z
ZVAR [in sysf]zVAR [in sysf]
Inductive Index
C
convert [in strnorm]E
Exp [in sysf]F
Forall [in MergesortList]Forall [in MergesortVector]
H
HdRel [in MergesortVector]HdRel [in MergesortList]
L
LocallySorted [in MergesortList]LocallySorted [in MergesortVector]
N
NoDup [in tutorial]P
Permutation [in tutorial]PermutationH [in tutorial]
PermutationHN [in tutorial]
PermutationN [in tutorial]
S
SN [in strnorm]Sorted [in MergesortVector]
Sorted [in MergesortList]
Sort.Stack [in MergesortVector]
StronglySorted [in MergesortVector]
StronglySorted [in MergesortList]
T
Ty [in sysf]V
varT [in sysf]VarT [in sysf]
vector [in Vector]
vector [in tutorial]
vectorH [in tutorial]
VNoDup [in Vector]
VPermutation [in Vector]
Abbreviation Index
C
cons_leA [in MergesortList]cons_leA [in MergesortVector]
cons_sort [in MergesortList]
cons_sort [in MergesortVector]
L
lelistA [in MergesortList]lelistA [in MergesortVector]
lelistA_inv [in MergesortVector]
lelistA_inv [in MergesortList]
M
matU [in tutorial]N
nil_leA [in MergesortVector]nil_leA [in MergesortList]
nil_sort [in MergesortList]
nil_sort [in MergesortVector]
P
PExp [in sysf]PMap [in sysf]
Pmat [in tutorial]
Pmat [in tutorial]
PmatH [in tutorial]
PmatH [in tutorial]
PPredExpList [in strnorm]
PRen [in sysf]
PSub [in sysf]
PVar [in sysf]
PvecH [in tutorial]
PvecH [in tutorial]
S
sort [in MergesortVector]sort [in MergesortList]
Sort.Pstk [in MergesortVector]
Sort.SortedB [in MergesortList]
Sort.SortedB [in MergesortVector]
sort_inv [in MergesortList]
sort_inv [in MergesortVector]
sort_rect [in MergesortVector]
sort_rect [in MergesortList]
V
vec [in Vector]vec [in Vector]
vec [in Vector]
vec [in Vector]
vec [in Vector]
vec [in tutorial]
vec [in Vector]
vec [in Vector]
vecH [in tutorial]
vecU [in tutorial]
vecU [in tutorial]
vrev_acc [in Vector]
vrev_acc_rev [in Vector]
Definition Index
A
app [in tutorial]appH [in tutorial]
appmatcol [in tutorial]
appmatcolH [in tutorial]
appmatrow [in tutorial]
appmatrowH [in tutorial]
C
conscol [in tutorial]conscolH [in tutorial]
consMap [in sysf]
consmap [in sysf]
consPredExp [in strnorm]
convertC [in strnorm]
CR [in strnorm]
CR1 [in strnorm]
CR2 [in strnorm]
CR3 [in strnorm]
D
dropMap [in sysf]dropRen [in sysf]
dropSub [in sysf]
E
Env [in sysf]F
finish_tag [in Heq.Heq]H
hcast [in Heq.Heq]hd [in tutorial]
hdcol [in tutorial]
hdcolH [in tutorial]
hdEnv [in sysf]
hdH [in tutorial]
hdMap [in sysf]
Heq [in Heq.Heq]
HeqEvar [in Heq.Heq]
HeqHint [in Heq.Heq]
HeqLockHyp1 [in Heq.Heq]
HeqLockHyp2 [in Heq.Heq]
HHideConcl [in Heq.Heq]
HId [in Heq.Heq]
hresolve_arg [in Heq.Heq]
HSetConcl [in Heq.Heq]
HSetConcl0 [in Heq.Heq]
Hty [in Heq.Heq]
htyeq [in Heq.Heq]
HType [in Heq.Heq]
I
idMap [in sysf]idren [in sysf]
idRen [in sysf]
idSub [in sysf]
idsub [in sysf]
idtemp [in Heq.Heq]
In [in tutorial]
L
liftMap [in sysf]M
map [in tutorial]mapExp [in sysf]
mapH [in tutorial]
mapT [in sysf]
MapT [in sysf]
matchbug [in Heq.Heq]
matchbug_elmt [in Heq.Heq]
matchbug_fix [in Heq.Heq]
matchbug_sig [in Heq.Heq]
matrix [in tutorial]
matrixH [in tutorial]
mcr [in sysf]
MCR [in sysf]
N
NatOrder.A [in MergesortVector]NatOrder.A [in MergesortList]
NatOrder.le_bool [in MergesortVector]
NatOrder.le_bool [in MergesortList]
neutral [in strnorm]
nilMap [in sysf]
normal [in strnorm]
n1n2_Sn [in tutorial]
n1n2_SnHN [in tutorial]
n_Spred [in tutorial]
P
plus_assoc [in Vector]plus_comm [in tutorial]
plus_comm [in Vector]
plus_commHN [in tutorial]
plus_n_O [in tutorial]
plus_n_O [in Vector]
plus_Snm_nSm [in Vector]
plus_Snm_nSm [in tutorial]
power [in Vector]
Pred [in strnorm]
PredExp [in strnorm]
PredExpList [in strnorm]
proj2m [in strnorm]
proj3 [in strnorm]
proj3m [in strnorm]
proj4 [in strnorm]
proj4m [in strnorm]
proj5 [in strnorm]
R
RCS [in sysf]rcs [in sysf]
RC_arrow [in strnorm]
RED [in strnorm]
Rel [in strnorm]
RenExp [in sysf]
renL [in sysf]
RenL [in sysf]
RenMap [in sysf]
RenT [in sysf]
renT [in sysf]
renTy [in sysf]
rev [in tutorial]
revH [in tutorial]
rev_append [in tutorial]
rev_appendH [in tutorial]
RTS [in sysf]
rts [in sysf]
S
SCS [in sysf]scs [in sysf]
SExp [in sysf]
shren [in sysf]
shsub [in sysf]
shSub [in sysf]
SimpleMergeExample [in MergesortVector]
SimpleMergeExample [in MergesortList]
simulation [in strnorm]
SMap [in sysf]
Smat [in tutorial]
SmatH [in tutorial]
SNRC [in strnorm]
Sort.flatten_stack [in MergesortList]
Sort.flatten_stack [in MergesortVector]
Sort.iter_merge [in MergesortList]
Sort.iter_merge [in MergesortVector]
Sort.merge [in MergesortList]
Sort.merge [in MergesortVector]
Sort.merge_list_to_stack [in MergesortVector]
Sort.merge_list_to_stack [in MergesortList]
Sort.merge_stack [in MergesortVector]
Sort.merge_stack [in MergesortList]
Sort.sort [in MergesortVector]
Sort.sort [in MergesortList]
Sort.SortedStack [in MergesortList]
Sort.SortedStack [in MergesortVector]
Sort.Sstk [in MergesortVector]
SPredExpList [in strnorm]
SRen [in sysf]
SSub [in sysf]
subE [in sysf]
SubExp [in sysf]
subExp [in sysf]
subExpC1 [in sysf]
subExpC2 [in sysf]
subL [in sysf]
SubL [in sysf]
SubMap [in sysf]
subRen [in sysf]
substMap [in sysf]
subSub [in sysf]
subT [in sysf]
SubT [in sysf]
subTy [in sysf]
subVar [in sysf]
SVar [in sysf]
Svec [in Vector]
Svec [in tutorial]
SvecH [in tutorial]
T
tail [in tutorial]tailH [in tutorial]
tlcol [in tutorial]
tlcolH [in tutorial]
tlMap [in sysf]
U
UnivVar [in strnorm]V
vapp [in Vector]varsp [in strnorm]
vcombine [in Vector]
vcount_occ [in Vector]
VDMap [in sysf]
vector_power [in Vector]
vector_prod [in Vector]
vexistsb [in Vector]
vfilter [in Vector]
vfind [in Vector]
vfirstn [in Vector]
vflat_map [in Vector]
vfold_left [in Vector]
vfold_right [in Vector]
vforallb [in Vector]
vhd [in Vector]
vhead [in Vector]
VIn [in Vector]
vincl [in Vector]
vlast [in Vector]
vmap [in Vector]
vnth [in Vector]
vnth_default [in Vector]
vnth_error [in Vector]
vnth_ok [in Vector]
vpartition [in Vector]
vremove [in Vector]
vremovelast [in Vector]
vrev [in Vector]
vrev' [in Vector]
vrev_append [in Vector]
vseq [in Vector]
vskipn [in Vector]
vsplit [in Vector]
vtail [in Vector]
Module Index
N
NatOrder [in MergesortList]NatOrder [in MergesortVector]
NatSort [in MergesortList]
NatSort [in MergesortVector]
S
Sort [in MergesortList]Sort [in MergesortVector]
T
TotalOrder [in MergesortList]TotalOrder [in MergesortVector]
Axiom Index
T
TotalOrder.A [in MergesortVector]TotalOrder.A [in MergesortList]
TotalOrder.le_bool [in MergesortList]
TotalOrder.le_bool [in MergesortVector]
TotalOrder.le_bool_total [in MergesortVector]
TotalOrder.le_bool_total [in MergesortList]
Variable Index
B
Bool.A [in Vector]Bool.f [in Vector]
C
CompMR.ops [in sysf]CompMR.P [in sysf]
Cutting.A [in Vector]
D
defs.A [in MergesortVector]defs.A [in MergesortList]
defs.R [in MergesortVector]
defs.R [in MergesortList]
E
Elts.A [in Vector]Elts.eqA_dec [in Vector]
Elts.Remove.eq_dec [in Vector]
F
Facts.A [in Vector]Fold_Left_Recursor.A [in Vector]
Fold_Left_Recursor.B [in Vector]
Fold_Left_Recursor.f [in Vector]
Fold_Right_Recursor.A [in Vector]
Fold_Right_Recursor.a0 [in Vector]
Fold_Right_Recursor.B [in Vector]
Fold_Right_Recursor.f [in Vector]
M
MapH.F [in tutorial]MapH.f [in tutorial]
MapH.P [in tutorial]
MapH.Q [in tutorial]
MapH.U [in tutorial]
MapH.V [in tutorial]
Map.A [in tutorial]
Map.A [in Vector]
Map.B [in tutorial]
Map.B [in Vector]
Map.f [in Vector]
Map.f [in tutorial]
MatrixH.P [in tutorial]
MatrixH.U [in tutorial]
Matrix.A [in tutorial]
R
ReDun.A [in Vector]S
SetIncl.A [in Vector]V
VariableDomainMap.ops [in sysf]VariableDomainMap.P [in sysf]
VectorH.P [in tutorial]
VectorH.U [in tutorial]
VectorOps.A [in Vector]
VectorOps.eqA_dec [in Vector]
VectorPairs.A [in Vector]
VectorPairs.B [in Vector]
Vectors.A [in Vector]
Vector.A [in tutorial]
Library Index
H
HeqM
MergesortListMergesortVector
S
strnormsysf
T
tutorialV
Vector| 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 | _ | (795 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 | _ | (4 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 | _ | (1 entry) |
| 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 | _ | (348 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 | _ | (26 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 | _ | (75 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 | _ | (27 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 | _ | (47 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 | _ | (199 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 | _ | (8 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 | _ | (6 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 | _ | (47 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 | _ | (7 entries) |
This page has been generated by coqdoc