Global Index

other

(837 entries)

Notation Index

other

(28 entries)

Module Index

other

(1 entry)

Variable Index

other

(38 entries)

Library Index

other

(41 entries)

Lemma Index

other

(352 entries)

Constructor Index

other

(59 entries)

Inductive Index

other

(20 entries)

Projection Index

other

(6 entries)

Section Index

other

(21 entries)

Instance Index

other

(126 entries)

Definition Index

other

(142 entries)

Record Index

other

(3 entries)

Global Index

A

Acceptability [library]
acc_conj_correct [lemma, in Acceptability]
acc_conj [definition, in Acceptability]
AD [lemma, in AD]
AD [library]
and_dec [instance, in Base]
app [constructor, in Lvw]
App [definition, in Encoding]
app_converges [lemma, in Seval]
app_closed [lemma, in Lvw]
app_equi_proper [instance, in Base]
app_eq_proper [lemma, in crush_no_refl_ideas]
ARS [library]

B

bapp [constructor, in Lvw]
Base [library]
BaseLists [library]
benchTerm [definition, in Reflection]
bijection [library]
bijections [section, in bijection]
bijections.A [variable, in bijection]
bijections.B [variable, in bijection]
bijective [inductive, in bijection]
blam [constructor, in Lvw]
bool_enc_correct [lemma, in LBool]
bool_enc_inj [instance, in LBool]
bool_enc [definition, in LBool]
bool_enc_inv_correct [lemma, in Computability]
bool_enc_inv [definition, in Computability]
bool_eq_dec [instance, in Base]
bter [constructor, in Lvw]
bterm [inductive, in Lvw]
bvar [constructor, in Lvw]

C

card [definition, in Base]
Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_cons [lemma, in Base]
card_ex [lemma, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
cChoice [definition, in Computability]
church_rosser [definition, in ARS]
church_rosser [lemma, in Lvw]
closed [definition, in Lvw]
closed_star [lemma, in Lvw]
closed_step [lemma, in Lvw]
closed_subst [lemma, in Lvw]
closed_dec [instance, in Lvw]
closed_app [lemma, in Lvw]
closed_dcl [lemma, in Lvw]
closed_k_dclosed [lemma, in Lvw]
closed_dcl_x [lemma, in LTactics]
clR [lemma, in crush_no_refl_ideas]
clR' [lemma, in crush_no_refl_ideas]
comb_proc_red [lemma, in Lvw]
Comp [inductive, in LvwClos]
CompApp [constructor, in LvwClos]
CompBeta [definition, in LvwClos_Eval]
CompBeta_sound [lemma, in LvwClos_Eval]
CompBeta_validComp [lemma, in LvwClos_Eval]
CompClos [constructor, in LvwClos]
complement [definition, in Decidability]
complete_induction [lemma, in Base]
CompSeval [definition, in LvwClos_Eval]
CompSeval_sound [lemma, in LvwClos_Eval]
CompSeval_validComp [lemma, in LvwClos_Eval]
CompStep_correct2 [lemma, in LvwClos]
CompStep_correct2' [lemma, in LvwClos]
Computability [library]
CompVar [constructor, in LvwClos]
Comp_ind_deep [definition, in LvwClos]
Comp_ind_deep' [definition, in LvwClos]
confluence [lemma, in Lvw]
confluent [definition, in ARS]
confluent_CR [lemma, in ARS]
conj [definition, in Decidability]
cons_equi_proper [instance, in Base]
converges [definition, in Lvw]
converges_proper [instance, in Lvw]
converges_equiv [lemma, in Lvw]
convert [definition, in Lvw]
convert' [definition, in Lvw]
convI [definition, in LTactics]
correct [definition, in internalize_def]
correct_t [projection, in internalize_def]
crush_no_refl_ideas [library]
CStep [inductive, in LvwClos]
CStepApp [constructor, in LvwClos]
CStepAppL [constructor, in LvwClos]
CStepAppR [constructor, in LvwClos]
CStepVal [constructor, in LvwClos]
CStepVar [constructor, in LvwClos]
CStep_equivC [lemma, in LvwClos]
CStep_reduceC [lemma, in LvwClos]
CStep_star_subrelation [instance, in LvwClos]
C27 [lemma, in Scott]
C27_proc [lemma, in Scott]

D

database_dummy [lemma, in Tactics_old]
dclApp [constructor, in Lvw]
dcllam [constructor, in Lvw]
dclosed [inductive, in Lvw]
dclosedb [definition, in Proc]
dclosedb_spec [lemma, in Proc]
dclosed_dec [instance, in Lvw]
dclosed_closed [lemma, in Lvw]
dclosed_gt [lemma, in Lvw]
dclosed_ge [lemma, in Lvw]
dclosed_closed_k [lemma, in Lvw]
dclvar [constructor, in Lvw]
dec [definition, in Base]
Decidability [library]
decides [definition, in Decidability]
decision [definition, in Base]
deClos [definition, in LvwClos]
deClos_lam [lemma, in LvwClos]
deClos_correct_star [lemma, in LvwClos]
deClos_correct' [lemma, in LvwClos]
deClos_correct'' [lemma, in LvwClos]
deClos_validEnv [lemma, in LvwClos]
deClos_valComp [lemma, in LvwClos]
dec_acc [lemma, in Acceptability]
dec_lacc [lemma, in Acceptability]
dec_P [lemma, in MuRec]
dec_pdec [lemma, in Computability]
dec_ldec [lemma, in Decidability]
dec_enc [lemma, in LNat]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
denoteComp [definition, in Reflection]
denoteTerm [definition, in Reflection]
denoteTerm_correct [lemma, in Reflection]
diamond [definition, in ARS]
diamond_to_confluent [lemma, in ARS]
diamond_to_semi_confluent [lemma, in ARS]
disj [definition, in Decidability]
disjoint [definition, in Base]
disjoint_cons [lemma, in Base]
disjoint_forall [lemma, in Base]
doesHaltIn [definition, in Eval]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
DupfreeLength [section, in Base]
DupfreeLength.X [variable, in Base]
dupfreeN [constructor, in Base]
dupfree_elAt [lemma, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_equi [lemma, in Base]
dupfree_ex [lemma, in Base]
dupfree_lt [lemma, in Base]
dupfree_eq [lemma, in Base]
dupfree_le [lemma, in Base]
dupfree_reorder [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_inv [lemma, in Base]
Dupfree.X [variable, in Base]

E

ecl [inductive, in ARS]
eclC [constructor, in ARS]
eclR [constructor, in ARS]
eclS [constructor, in ARS]
ecl_sym [lemma, in ARS]
ecl_trans [lemma, in ARS]
elAt [definition, in Base]
elAt_el [lemma, in Base]
elAt_app [lemma, in Base]
elAt' [definition, in internalize_tac]
el_elAt [lemma, in Base]
el_pos [lemma, in Base]
enc [definition, in internalize_def]
Encoding [library]
enc_extinj [lemma, in Computability]
enc_f [projection, in internalize_def]
eproc_equiv [lemma, in Seval]
eqApp [lemma, in Lvw]
eqC [constructor, in LvwClos]
eqRef [constructor, in Lvw]
eqStarT [lemma, in Lvw]
eqStep [constructor, in Lvw]
eqSym [constructor, in Lvw]
eqTrans [constructor, in Lvw]
Equality [library]
Equi [section, in Base]
equi [definition, in Base]
equiv [inductive, in Lvw]
equivC [inductive, in LvwClos]
equivC_deClos [lemma, in LvwClos]
equivC_App_proper [instance, in LvwClos]
equivC_Equivalence [instance, in LvwClos]
equivC_if [lemma, in LvwClos]
equiv_eva [lemma, in Seval]
equiv_app_proper [instance, in Lvw]
equiv_lambda [lemma, in Lvw]
equiv_ecl [lemma, in Lvw]
equiv_Equivalence [instance, in Lvw]
equiv_trans_r [lemma, in Tactics_old]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]
eq_term_dec [lemma, in Computability]
eq_ref [lemma, in ARS]
eq_dec_string [instance, in Lvw]
Eq_ldec [lemma, in Scott]
Eta [lemma, in Lvw]
eva [definition, in Seval]
eval [definition, in Seval]
Eval [definition, in Eval]
Eval [library]
eval_seval [lemma, in Seval]
eval_step [lemma, in Seval]
eval_converges [lemma, in Seval]
Eval_converges [lemma, in Eval]
eval_converges [lemma, in Eval]
Eval_eval [lemma, in Eval]
eval_Eval [lemma, in Eval]
Eval_correct [lemma, in Eval]
eva_Sn_n [lemma, in Seval]
eva_n_Sn [lemma, in Seval]
eva_equiv [lemma, in Seval]
eva_seval [lemma, in Seval]
eva_lam [lemma, in Seval]
expandDenote [lemma, in Reflection]

F

False_dec [instance, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_app [lemma, in Base]
filter_fst [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
FirstFixedPoint [lemma, in Fixpoints]
Fixpoints [library]
FixX [section, in ARS]
FixX.X [variable, in ARS]
Fix_X.intX [variable, in Lists]
Fix_X.X [variable, in Lists]
Fix_X [section, in Lists]
Fix_X.intX [variable, in LOptions]
Fix_X.X [variable, in LOptions]
Fix_X [section, in LOptions]
Fix_X.eq_dec_X [variable, in BaseLists]
Fix_X.X [variable, in BaseLists]
Fix_X [section, in BaseLists]
Fix_XY.intY [variable, in LProd]
Fix_XY.Y [variable, in LProd]
Fix_XY.intX [variable, in LProd]
Fix_XY.X [variable, in LProd]
Fix_XY [section, in LProd]
FP [definition, in Base]
from_sumbool_elim [lemma, in SumBool]
from_sumbool [definition, in SumBool]
functional [definition, in ARS]

H

helper [definition, in intermediate]

I

I [definition, in Lvw]
iApp [constructor, in intermediate]
iConst [constructor, in intermediate]
iff_dec [instance, in Base]
iFix [constructor, in intermediate]
iLam [constructor, in intermediate]
iMatch [constructor, in intermediate]
impl_dec [instance, in Base]
inb [definition, in Lists]
inb_spec [lemma, in Lists]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_preorder [instance, in Base]
incl_equi_proper [instance, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
injective [definition, in bijection]
inj_enc [projection, in internalize_def]
inj_reg [record, in internalize_def]
int [definition, in internalize_def]
intApp [lemma, in LTactics]
intAppTest [lemma, in LTactics]
intApp' [instance, in LTactics]
intermediate [library]
internalizedClass [record, in internalize_def]
internalizer [projection, in internalize_def]
internalizesF [definition, in internalize_def]
internalize_tac [library]
internalize_demo [library]
internalize_def [library]
intFApp [lemma, in LTactics]
intFEquiv [lemma, in LTactics]
inverse [definition, in bijection]
inv2bij [lemma, in bijection]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
is_bijective [constructor, in bijection]
it [definition, in Base]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
iTerm [inductive, in intermediate]
iType [constructor, in intermediate]
it_fp [lemma, in Base]
it_ind [lemma, in Base]
iVar [constructor, in intermediate]
I_neq_Omega [lemma, in Scott]
I_proc [lemma, in LTactics]

J

joinable [definition, in ARS]

K

K [definition, in Lvw]
K_proc [lemma, in LTactics]

L

lacc [definition, in Acceptability]
lacc_disj [lemma, in Acceptability]
lacc_conj [lemma, in Acceptability]
lam [constructor, in Lvw]
Lam [definition, in Encoding]
lambda [definition, in Lvw]
lambdaComp [constructor, in LvwClos]
lambda_dec [instance, in Lvw]
lambda_lam [lemma, in Lvw]
lamComp [inductive, in LvwClos]
lamComp_star [lemma, in LvwClos]
lamComp_noStep [lemma, in LvwClos]
lamOmega [lemma, in Rice]
lam_app_proper [lemma, in crush_no_refl_ideas]
LBool [library]
lcomp_comp [lemma, in Computability]
ldec [definition, in Decidability]
ldec_dec [lemma, in Computability]
ldec_disj [lemma, in Decidability]
ldec_conj [lemma, in Decidability]
ldec_complement [lemma, in Decidability]
ldec_proc [lemma, in Proc]
ldec_closed [lemma, in Proc]
ldec_lambda [lemma, in Proc]
left_inv_inj [lemma, in bijection]
left_inverse [definition, in bijection]
liftPhi [definition, in Reflection]
liftPhi_correct [lemma, in Reflection]
Lists [library]
lists_cons [definition, in Lists]
list_enc_correct [lemma, in Lists]
list_enc_inj [instance, in Lists]
list_enc [definition, in Lists]
list_cc [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
LNat [library]
LOptions [library]
LProd [library]
LProp [library]
lStep [lemma, in crush_no_refl_ideas]
LTactics [library]
Lvw [library]
LvwClos [library]
LvwClos_Eval [library]

M

map_ext' [lemma, in Reflection]
mk_inj_reg [constructor, in internalize_def]
mk_registered [constructor, in internalize_def]
MoreAcc [library]
mu [definition, in MuRec]
MuRec [library]
MuRecursor [section, in MuRec]
MuRecursor.dec'_P [variable, in MuRec]
MuRecursor.P [variable, in MuRec]
MuRecursor.P_proc [variable, in MuRec]
mu_complete [lemma, in MuRec]
mu_sound [lemma, in MuRec]
mu_proc [lemma, in MuRec]
mu' [definition, in MuRec]
mu'_complete [lemma, in MuRec]
mu'_sound [lemma, in MuRec]
mu'_n_true [lemma, in MuRec]
mu'_0_false [lemma, in MuRec]
mu'_n_false [lemma, in MuRec]
mu'_proc [lemma, in MuRec]

N

O

oenc_correct_some [lemma, in LOptions]
Omega [definition, in Lvw]
omega [definition, in Lvw]
Omega_diverges [lemma, in Seval]
Omega_closed [lemma, in LTactics]
omega_proc [lemma, in LTactics]
on0 [definition, in internalize_demo]
option_enc_correct [lemma, in LOptions]
option_enc_inj [instance, in LOptions]
option_some [definition, in LOptions]
option_none [definition, in LOptions]
option_enc [definition, in LOptions]
option_enc_inj [instance, in LProd]
or_dec [instance, in Base]

P

parametrized_confluence [lemma, in ARS]
parametrized_semi_confluence [lemma, in ARS]
pi [definition, in Acceptability]
Por [definition, in Por]
Por [library]
Por_correct' [lemma, in Por]
Por_correct_2 [lemma, in Por]
Por_correct_1 [lemma, in Por]
Por_correct_1b [lemma, in Por]
Por_correct_1a [lemma, in Por]
Por_proc [lemma, in Por]
pos [definition, in Base]
pos [section, in Base]
pos_length [lemma, in BaseLists]
pos_second_S [lemma, in BaseLists]
pos_first_S [lemma, in BaseLists]
pos_None [lemma, in BaseLists]
pos_elAt [lemma, in Base]
pos.X [variable, in Base]
_ .[ _ ] [notation, in Base]
pow [definition, in ARS]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
powSk [lemma, in Lvw]
pow_add [lemma, in ARS]
pow_star [lemma, in ARS]
pow_trans_lam [lemma, in Lvw]
pow_trans_lam' [lemma, in Lvw]
Proc [definition, in Reflection]
proc [definition, in Lvw]
Proc [library]
proc_t [projection, in internalize_def]
proc_enc [projection, in internalize_def]
proc_dec [lemma, in Lvw]
proc_lambda [lemma, in Tactics_old]
proc_closed [lemma, in Tactics_old]
prod_eq_dec [instance, in Base]
prod_enc_correct [lemma, in LProd]
prod_enc [definition, in LProd]
prop_term [instance, in LProp]
prop_enc [definition, in LProp]

R

S

T

Tactics_old [library]
tcompl [definition, in Decidability]
tconj [definition, in Decidability]
tdisj [definition, in Decidability]
term [inductive, in Lvw]
term_term_eq_dec [instance, in Equality]
term_term_eqb [instance, in Equality]
term_eqb [definition, in Equality]
term_nat_eq_dec [instance, in Equality]
term_nat_eqb [instance, in Equality]
term_elAt [instance, in Lists]
term_nth_error [instance, in Lists]
term_map [instance, in Lists]
term_pos [instance, in Lists]
term_list_in_dec [instance, in Lists]
term_inb [instance, in Lists]
term_nth [instance, in Lists]
term_filter [instance, in Lists]
term_append [instance, in Lists]
term_cons [instance, in Lists]
term_nil [instance, in Lists]
term_size [instance, in Size]
term_subst [instance, in Subst]
term_orb [instance, in LBool]
term_andb [instance, in LBool]
term_negb [instance, in LBool]
term_false [instance, in LBool]
term_true [instance, in LBool]
term_option_map [instance, in LOptions]
term_Some [instance, in LOptions]
term_None [instance, in LOptions]
term_nat_le_dec [instance, in LNat]
term_leb [instance, in LNat]
term_mult [instance, in LNat]
term_plus [instance, in LNat]
term_pred [instance, in LNat]
term_S [instance, in LNat]
term_O [instance, in LNat]
term_not_dec [instance, in SumBool]
term_impl_dec [instance, in SumBool]
term_from_sumbool [instance, in SumBool]
term_to_sumbool [instance, in SumBool]
term_right [instance, in SumBool]
term_left [instance, in SumBool]
term_False_dec [instance, in SumBool]
term_True_dec [instance, in SumBool]
term_eq_dec_proc [definition, in Lvw]
term_eq_dec [instance, in Lvw]
term_nat_eqb [instance, in internalize_demo]
term_option_map [instance, in internalize_demo]
term_on0 [instance, in internalize_demo]
term_prod_eq_dec [instance, in LProd]
term_snd [instance, in LProd]
term_fst [instance, in LProd]
term_pair [instance, in LProd]
term_doesHaltIn [instance, in Eval]
term_eva [instance, in Eval]
term_term_enc [instance, in Encoding]
term_nat_enc [instance, in Encoding]
term_lam [instance, in Encoding]
term_app [instance, in Encoding]
term_var [instance, in Encoding]
term_enc_correct [lemma, in Encoding]
term_enc_inj [instance, in Encoding]
term_enc [definition, in Encoding]
term_lambda_dec [instance, in Proc]
term_closed_dec [instance, in Proc]
term_dclosed_dec [instance, in Proc]
term_dclosedb [instance, in Proc]
term_unenc [instance, in Unenc]
test [instance, in internalize_demo]
testT [definition, in internalize_demo]
test_Some_nat [lemma, in internalize_demo]
totality [lemma, in MoreAcc]
totality_compl [lemma, in MoreAcc]
totality_proc [lemma, in MoreAcc]
to_list [definition, in StringBase]
to_string [definition, in StringBase]
to_sumbool [definition, in SumBool]
transform [definition, in internalize_tac]
transitive [definition, in ARS]
True_dec [instance, in Base]
TT [inductive, in internalize_def]
TyAll [constructor, in internalize_def]
TyB [constructor, in internalize_def]
TyElim [constructor, in internalize_def]

U

undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_eq [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_fp_equi [lemma, in Base]
Undup.X [variable, in Base]
unenc [definition, in LNat]
Unenc [library]
unenc_correct2 [lemma, in LNat]
unenc_correct [lemma, in LNat]
uniform_confluent [definition, in ARS]
uniform_confluence [lemma, in Lvw]
unique_normal_forms [lemma, in Lvw]
unit_enc [definition, in internalize_demo]

V

validComp [inductive, in LvwClos]
validCompApp [constructor, in LvwClos]
validCompClos [constructor, in LvwClos]
validComp_star [lemma, in LvwClos]
validComp_closed [lemma, in LvwClos]
validComp_step [lemma, in LvwClos]
validEnv [definition, in LvwClos]
validEnv_cons [lemma, in LvwClos]
validEnv' [definition, in LvwClos]
validEnv'_cons [lemma, in LvwClos]
var [constructor, in Lvw]
Var [definition, in Encoding]

other

_ >[]* _ (LvwClos) [notation, in LvwClos]
_ >[]> _ (LvwClos) [notation, in LvwClos]
_ ⇓ _ _ [notation, in Seval]
_ ⇓ _ [notation, in Seval]
_ =[]= _ [notation, in LvwClos]
_ =[]> _ [notation, in LvwClos]
_ ~> _ [notation, in internalize_def]
_ =2 _ [notation, in ARS]
_ <=2 _ [notation, in ARS]
_ =1 _ [notation, in ARS]
_ <=1 _ [notation, in ARS]
_ == _ [notation, in Lvw]
_ >* _ [notation, in Lvw]
_ >^ _ _ [notation, in Lvw]
_ >> _ [notation, in Lvw]
_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
internalized _ [notation, in internalize_tac]
!! _ [notation, in Lvw]
! _ [notation, in internalize_def]
# _ [notation, in Lvw]
(λ _ ) [notation, in Lvw]
.\ _ , .. , _ ; _ [notation, in Lvw]
| _ | [notation, in Base]
λ _ , .. , _ ; _ [notation, in Lvw]

Notation Index

P

_ .[ _ ] [in Base]

other

_ >[]* _ (LvwClos) [in LvwClos]
_ >[]> _ (LvwClos) [in LvwClos]
_ ⇓ _ _ [in Seval]
_ ⇓ _ [in Seval]
_ =[]= _ [in LvwClos]
_ =[]> _ [in LvwClos]
_ ~> _ [in internalize_def]
_ =2 _ [in ARS]
_ <=2 _ [in ARS]
_ =1 _ [in ARS]
_ <=1 _ [in ARS]
_ == _ [in Lvw]
_ >* _ [in Lvw]
_ >^ _ _ [in Lvw]
_ >> _ [in Lvw]
_ === _ [in Base]
_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
internalized _ [in internalize_tac]
!! _ [in Lvw]
! _ [in internalize_def]
# _ [in Lvw]
(λ _ ) [in Lvw]
.\ _ , .. , _ ; _ [in Lvw]
| _ | [in Base]
λ _ , .. , _ ; _ [in Lvw]

Module Index

F

FCI [in Base]

Variable Index

B

bijections.A [in bijection]
bijections.B [in bijection]

C

Cardinality.X [in Base]

D

DupfreeLength.X [in Base]
Dupfree.X [in Base]

E

Equi.X [in Base]

F

FCI.FCI.step [in Base]
FCI.FCI.V [in Base]
FCI.FCI.X [in Base]
FilterComm.p [in Base]
FilterComm.q [in Base]
FilterComm.X [in Base]
FilterLemmas_pq.q [in Base]
FilterLemmas_pq.p [in Base]
FilterLemmas_pq.X [in Base]
FilterLemmas.p [in Base]
FilterLemmas.X [in Base]
FixX.X [in ARS]
Fix_X.intX [in Lists]
Fix_X.X [in Lists]
Fix_X.intX [in LOptions]
Fix_X.X [in LOptions]
Fix_X.eq_dec_X [in BaseLists]
Fix_X.X [in BaseLists]
Fix_XY.intY [in LProd]
Fix_XY.Y [in LProd]
Fix_XY.intX [in LProd]
Fix_XY.X [in LProd]

I

Inclusion.X [in Base]
Iteration.f [in Base]
Iteration.X [in Base]

M

MuRecursor.dec'_P [in MuRec]
MuRecursor.P [in MuRec]
MuRecursor.P_proc [in MuRec]

P

pos.X [in Base]
PowerRep.X [in Base]

R

Removal.X [in Base]

U

Undup.X [in Base]

Library Index

A

Acceptability
AD
ARS

B

Base
BaseLists
bijection

C

Computability
crush_no_refl_ideas

D

Decidability

E

Encoding
Equality
Eval

F

Fixpoints

I

intermediate
internalize_tac
internalize_demo
internalize_def

L

LBool
Lists
LNat
LOptions
LProd
LProp
LTactics
Lvw
LvwClos
LvwClos_Eval

M

MoreAcc
MuRec

P

Por
Proc

R

Reflection
Rice

S

Scott
Seval
Size
StringBase
Subst
SumBool

T

Tactics_old

U

Unenc

Lemma Index

A

acc_conj_correct [in Acceptability]
AD [in AD]
app_converges [in Seval]
app_closed [in Lvw]
app_eq_proper [in crush_no_refl_ideas]

B

bool_enc_correct [in LBool]
bool_enc_inv_correct [in Computability]

C

card_0 [in Base]
card_cons_rem [in Base]
card_cons [in Base]
card_ex [in Base]
card_or [in Base]
card_lt [in Base]
card_equi [in Base]
card_eq [in Base]
card_le [in Base]
church_rosser [in Lvw]
closed_star [in Lvw]
closed_step [in Lvw]
closed_subst [in Lvw]
closed_app [in Lvw]
closed_dcl [in Lvw]
closed_k_dclosed [in Lvw]
closed_dcl_x [in LTactics]
clR [in crush_no_refl_ideas]
clR' [in crush_no_refl_ideas]
comb_proc_red [in Lvw]
CompBeta_sound [in LvwClos_Eval]
CompBeta_validComp [in LvwClos_Eval]
complete_induction [in Base]
CompSeval_sound [in LvwClos_Eval]
CompSeval_validComp [in LvwClos_Eval]
CompStep_correct2 [in LvwClos]
CompStep_correct2' [in LvwClos]
confluence [in Lvw]
confluent_CR [in ARS]
converges_equiv [in Lvw]
CStep_equivC [in LvwClos]
CStep_reduceC [in LvwClos]
C27 [in Scott]
C27_proc [in Scott]

D

database_dummy [in Tactics_old]
dclosedb_spec [in Proc]
dclosed_closed [in Lvw]
dclosed_gt [in Lvw]
dclosed_ge [in Lvw]
dclosed_closed_k [in Lvw]
deClos_lam [in LvwClos]
deClos_correct_star [in LvwClos]
deClos_correct' [in LvwClos]
deClos_correct'' [in LvwClos]
deClos_validEnv [in LvwClos]
deClos_valComp [in LvwClos]
dec_acc [in Acceptability]
dec_lacc [in Acceptability]
dec_P [in MuRec]
dec_pdec [in Computability]
dec_ldec [in Decidability]
dec_enc [in LNat]
dec_prop_iff [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
denoteTerm_correct [in Reflection]
diamond_to_confluent [in ARS]
diamond_to_semi_confluent [in ARS]
disjoint_cons [in Base]
disjoint_forall [in Base]
dupfree_elAt [in Base]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_equi [in Base]
dupfree_ex [in Base]
dupfree_lt [in Base]
dupfree_eq [in Base]
dupfree_le [in Base]
dupfree_reorder [in Base]
dupfree_undup [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_inv [in Base]

E

ecl_sym [in ARS]
ecl_trans [in ARS]
elAt_el [in Base]
elAt_app [in Base]
el_elAt [in Base]
el_pos [in Base]
enc_extinj [in Computability]
eproc_equiv [in Seval]
eqApp [in Lvw]
eqStarT [in Lvw]
equivC_deClos [in LvwClos]
equivC_if [in LvwClos]
equiv_eva [in Seval]
equiv_lambda [in Lvw]
equiv_ecl [in Lvw]
equiv_trans_r [in Tactics_old]
equi_rotate [in Base]
equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
eq_term_dec [in Computability]
eq_ref [in ARS]
Eq_ldec [in Scott]
Eta [in Lvw]
eval_seval [in Seval]
eval_step [in Seval]
eval_converges [in Seval]
Eval_converges [in Eval]
eval_converges [in Eval]
Eval_eval [in Eval]
eval_Eval [in Eval]
Eval_correct [in Eval]
eva_Sn_n [in Seval]
eva_n_Sn [in Seval]
eva_equiv [in Seval]
eva_seval [in Seval]
eva_lam [in Seval]
expandDenote [in Reflection]

F

FCI.closure [in Base]
FCI.fp [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
filter_comm [in Base]
filter_and [in Base]
filter_pq_eq [in Base]
filter_pq_mono [in Base]
filter_fst' [in Base]
filter_app [in Base]
filter_fst [in Base]
filter_mono [in Base]
filter_incl [in Base]
FirstFixedPoint [in Fixpoints]
from_sumbool_elim [in SumBool]

I

inb_spec [in Lists]
incl_lrcons [in Base]
incl_rcons [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
intApp [in LTactics]
intAppTest [in LTactics]
intFApp [in LTactics]
intFEquiv [in LTactics]
inv2bij [in bijection]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
it_fp [in Base]
it_ind [in Base]
I_neq_Omega [in Scott]
I_proc [in LTactics]

K

K_proc [in LTactics]

L

lacc_disj [in Acceptability]
lacc_conj [in Acceptability]
lambda_lam [in Lvw]
lamComp_star [in LvwClos]
lamComp_noStep [in LvwClos]
lamOmega [in Rice]
lam_app_proper [in crush_no_refl_ideas]
lcomp_comp [in Computability]
ldec_dec [in Computability]
ldec_disj [in Decidability]
ldec_conj [in Decidability]
ldec_complement [in Decidability]
ldec_proc [in Proc]
ldec_closed [in Proc]
ldec_lambda [in Proc]
left_inv_inj [in bijection]
liftPhi_correct [in Reflection]
list_enc_correct [in Lists]
list_cc [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
lStep [in crush_no_refl_ideas]

M

map_ext' [in Reflection]
mu_complete [in MuRec]
mu_sound [in MuRec]
mu_proc [in MuRec]
mu'_complete [in MuRec]
mu'_sound [in MuRec]
mu'_n_true [in MuRec]
mu'_0_false [in MuRec]
mu'_n_false [in MuRec]
mu'_proc [in MuRec]

N

nat_enc_proc [in LNat]
nat_enc_correct [in LNat]
normComp_valid [in LvwClos]
normComp_idem [in LvwClos]
normComp_star [in LvwClos]
normComp_deClos [in LvwClos]
normComp'_valid [in LvwClos]
normComp'_idem [in LvwClos]
normComp'_star [in LvwClos]
normComp'_deClos [in LvwClos]
nth_error_none [in Base]

O

oenc_correct_some [in LOptions]
Omega_diverges [in Seval]
Omega_closed [in LTactics]
omega_proc [in LTactics]
option_enc_correct [in LOptions]

P

parametrized_confluence [in ARS]
parametrized_semi_confluence [in ARS]
Por_correct' [in Por]
Por_correct_2 [in Por]
Por_correct_1 [in Por]
Por_correct_1b [in Por]
Por_correct_1a [in Por]
Por_proc [in Por]
pos_length [in BaseLists]
pos_second_S [in BaseLists]
pos_first_S [in BaseLists]
pos_None [in BaseLists]
pos_elAt [in Base]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
powSk [in Lvw]
pow_add [in ARS]
pow_star [in ARS]
pow_trans_lam [in Lvw]
pow_trans_lam' [in Lvw]
proc_dec [in Lvw]
proc_lambda [in Tactics_old]
proc_closed [in Tactics_old]
prod_enc_correct [in LProd]

R

rClosed_decb_correct [in Reflection]
rClosed_decb'_correct [in Reflection]
rClosed_valid [in Reflection]
rCompBeta_rValidComp [in Reflection]
rCompBeta_sound [in Reflection]
rCompSeval_rValidComp [in Reflection]
rCompSeval_sound [in Reflection]
rcomp_comm [in ARS]
rcomp_1 [in ARS]
rcomp_eq [in ARS]
rDeClos_rValidComp [in Reflection]
rDeClos_reduce [in Reflection]
reduceC_if [in LvwClos]
reflect_dec [in SumBool]
rem_fst' [in Base]
rem_fst [in Base]
rem_comm [in Base]
rem_equi [in Base]
rem_app' [in Base]
rem_app [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_cons' [in Base]
rem_cons [in Base]
rem_mono [in Base]
rem_incl [in Base]
rem_not_in [in Base]
replace_pos [in BaseLists]
replace_diff [in BaseLists]
replace_same [in BaseLists]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]
rEquivIntro [in Reflection]
rho_cls [in LTactics]
rho_lambda [in LTactics]
rho_inj [in LTactics]
rho_correct [in LTactics]
rho_dcls [in LTactics]
Rice [in Rice]
Rice_classical [in Rice]
Rice1 [in Rice]
Rice2 [in Rice]
right_inv_surj [in bijection]
rReduceIntro [in Reflection]
rStandardize [in Reflection]
rStandardizeGoal [in Reflection]
rStandardizeGoalLeft [in Reflection]
rStandardizeGoalLeft' [in Reflection]
rStandardizeHypo [in Reflection]
rStandardizeUse [in Reflection]
rStar'_trans_r [in LvwClos]
rStar'_trans_l [in LvwClos]
rSubstList_correct [in Reflection]

S

Scott [in Scott]
SecondFixedPoint [in Fixpoints]
self_div_comb [in Rice]
self_div [in Rice]
semi_confluent_confluent [in ARS]
seval_eva [in Seval]
seval_S [in Seval]
seval_eval [in Seval]
seval_Eval [in Eval]
size_surj [in Size]
size_induction [in Base]
starC_equivC [in LvwClos]
star_ecl [in ARS]
star_pow [in ARS]
star_trans [in ARS]
star_simpl_ind [in ARS]
star_equiv [in Lvw]
star_trans_r [in Lvw]
star_trans_l [in Lvw]
step_star [in Lvw]
step_value [in Lvw]
stHypo [in LTactics]
substList_nil [in LvwClos]
substList_closed' [in LvwClos]
substList_is_dclosed [in LvwClos]
substList_var [in LvwClos]
substList_var' [in LvwClos]
substList_closed [in LvwClos]
substList_dclosed [in LvwClos]
subst_substList [in LvwClos]
subst'_rho [in crush_no_refl_ideas]
subst'_eq_proper [in crush_no_refl_ideas]
subst'_enc [in crush_no_refl_ideas]
subst'_int [in crush_no_refl_ideas]
subst'_cls [in crush_no_refl_ideas]
subst'_eq [in crush_no_refl_ideas]
sumbool_enc_correct [in SumBool]

T

term_enc_correct [in Encoding]
test_Some_nat [in internalize_demo]
totality [in MoreAcc]
totality_compl [in MoreAcc]
totality_proc [in MoreAcc]

U

undup_idempotent [in Base]
undup_eq [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_fp_equi [in Base]
unenc_correct2 [in LNat]
unenc_correct [in LNat]
uniform_confluence [in Lvw]
unique_normal_forms [in Lvw]

V

validComp_star [in LvwClos]
validComp_closed [in LvwClos]
validComp_step [in LvwClos]
validEnv_cons [in LvwClos]
validEnv'_cons [in LvwClos]

Constructor Index

A

app [in Lvw]

B

bapp [in Lvw]
blam [in Lvw]
bter [in Lvw]
bvar [in Lvw]

C

CompApp [in LvwClos]
CompClos [in LvwClos]
CompVar [in LvwClos]
CStepApp [in LvwClos]
CStepAppL [in LvwClos]
CStepAppR [in LvwClos]
CStepVal [in LvwClos]
CStepVar [in LvwClos]

D

dclApp [in Lvw]
dcllam [in Lvw]
dclvar [in Lvw]
dupfreeC [in Base]
dupfreeN [in Base]

E

eclC [in ARS]
eclR [in ARS]
eclS [in ARS]
eqC [in LvwClos]
eqRef [in Lvw]
eqStep [in Lvw]
eqSym [in Lvw]
eqTrans [in Lvw]

I

iApp [in intermediate]
iConst [in intermediate]
iFix [in intermediate]
iLam [in intermediate]
iMatch [in intermediate]
is_bijective [in bijection]
iType [in intermediate]
iVar [in intermediate]

L

lam [in Lvw]
lambdaComp [in LvwClos]

M

mk_inj_reg [in internalize_def]
mk_registered [in internalize_def]

R

rApp [in Reflection]
rCompApp [in Reflection]
rCompClos [in Reflection]
rCompVar [in Reflection]
rConst [in Reflection]
redC [in LvwClos]
rLam [in Reflection]
rVar [in Reflection]

S

sevalR [in Seval]
sevalS [in Seval]
starC [in ARS]
starR [in ARS]
stepApp [in Lvw]
stepAppL [in Lvw]
stepAppR [in Lvw]

T

TyAll [in internalize_def]
TyB [in internalize_def]
TyElim [in internalize_def]

V

validCompApp [in LvwClos]
validCompClos [in LvwClos]
var [in Lvw]

Inductive Index

B

bijective [in bijection]
bterm [in Lvw]

C

Comp [in LvwClos]
CStep [in LvwClos]

D

dclosed [in Lvw]
dupfree [in Base]

E

ecl [in ARS]
equiv [in Lvw]
equivC [in LvwClos]

I

iTerm [in intermediate]

L

lamComp [in LvwClos]

R

rComp [in Reflection]
reduceC [in LvwClos]
rTerm [in Reflection]

S

seval [in Seval]
star [in ARS]
step [in Lvw]

T

term [in Lvw]
TT [in internalize_def]

V

validComp [in LvwClos]

Projection Index

C

correct_t [in internalize_def]

E

enc_f [in internalize_def]

I

inj_enc [in internalize_def]
internalizer [in internalize_def]

P

proc_t [in internalize_def]
proc_enc [in internalize_def]

Section Index

B

bijections [in bijection]

C

Cardinality [in Base]

D

Dupfree [in Base]
DupfreeLength [in Base]

E

Equi [in Base]

F

FCI.FCI [in Base]
FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
FixX [in ARS]
Fix_X [in Lists]
Fix_X [in LOptions]
Fix_X [in BaseLists]
Fix_XY [in LProd]

I

Inclusion [in Base]
Iteration [in Base]

M

MuRecursor [in MuRec]

P

pos [in Base]
PowerRep [in Base]

R

Removal [in Base]

U

Undup [in Base]

Instance Index

A

and_dec [in Base]
app_equi_proper [in Base]

B

bool_enc_inj [in LBool]
bool_eq_dec [in Base]

C

card_equi_proper [in Base]
closed_dec [in Lvw]
cons_equi_proper [in Base]
converges_proper [in Lvw]
CStep_star_subrelation [in LvwClos]

D

dclosed_dec [in Lvw]

E

equivC_App_proper [in LvwClos]
equivC_Equivalence [in LvwClos]
equiv_app_proper [in Lvw]
equiv_Equivalence [in Lvw]
equi_Equivalence [in Base]
eq_dec_string [in Lvw]

F

False_dec [in Base]

I

iff_dec [in Base]
impl_dec [in Base]
incl_preorder [in Base]
incl_equi_proper [in Base]
intApp' [in LTactics]
in_equi_proper [in Base]

L

lambda_dec [in Lvw]
list_enc_inj [in Lists]
list_exists_dec [in Base]
list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]

N

nat_enc_inj [in LNat]
nat_le_dec [in Base]
nat_eq_dec [in Base]
not_dec [in Base]

O

option_enc_inj [in LOptions]
option_enc_inj [in LProd]
or_dec [in Base]

P

prod_eq_dec [in Base]
prop_term [in LProp]

R

reduceC_App_proper [in LvwClos]
reduceC_PreOrder [in LvwClos]
register_list [in Lists]
register_Prop_el [in LProp]
register_bool [in LBool]
register_option [in LOptions]
register_nat [in LNat]
register_unit [in internalize_demo]
register_unit [in internalize_demo]
register_prod [in LProd]
register_term [in Encoding]
rEquiv_rApp_proper [in Reflection]
rEquiv_Equivalence [in Reflection]
rReduce_rEquiv_subrelation [in Reflection]
rReduce_rApp_proper [in Reflection]
rReduce_PreOrder [in Reflection]
rStar'_App_proper [in LvwClos]
rStar'_PreOrder [in LvwClos]

S

star_equiv_subrelation [in Lvw]
star_closed_proper [in Lvw]
star_step_app_proper [in Lvw]
star_PreOrder [in Lvw]
step_equiv_subrelation [in Lvw]
step_star_subrelation [in Lvw]
sumbool_term [in SumBool]

T

term_term_eq_dec [in Equality]
term_term_eqb [in Equality]
term_nat_eq_dec [in Equality]
term_nat_eqb [in Equality]
term_elAt [in Lists]
term_nth_error [in Lists]
term_map [in Lists]
term_pos [in Lists]
term_list_in_dec [in Lists]
term_inb [in Lists]
term_nth [in Lists]
term_filter [in Lists]
term_append [in Lists]
term_cons [in Lists]
term_nil [in Lists]
term_size [in Size]
term_subst [in Subst]
term_orb [in LBool]
term_andb [in LBool]
term_negb [in LBool]
term_false [in LBool]
term_true [in LBool]
term_option_map [in LOptions]
term_Some [in LOptions]
term_None [in LOptions]
term_nat_le_dec [in LNat]
term_leb [in LNat]
term_mult [in LNat]
term_plus [in LNat]
term_pred [in LNat]
term_S [in LNat]
term_O [in LNat]
term_not_dec [in SumBool]
term_impl_dec [in SumBool]
term_from_sumbool [in SumBool]
term_to_sumbool [in SumBool]
term_right [in SumBool]
term_left [in SumBool]
term_False_dec [in SumBool]
term_True_dec [in SumBool]
term_eq_dec [in Lvw]
term_nat_eqb [in internalize_demo]
term_option_map [in internalize_demo]
term_on0 [in internalize_demo]
term_prod_eq_dec [in LProd]
term_snd [in LProd]
term_fst [in LProd]
term_pair [in LProd]
term_doesHaltIn [in Eval]
term_eva [in Eval]
term_term_enc [in Encoding]
term_nat_enc [in Encoding]
term_lam [in Encoding]
term_app [in Encoding]
term_var [in Encoding]
term_enc_inj [in Encoding]
term_lambda_dec [in Proc]
term_closed_dec [in Proc]
term_dclosed_dec [in Proc]
term_dclosedb [in Proc]
term_unenc [in Unenc]
test [in internalize_demo]
True_dec [in Base]

Definition Index

A

acc_conj [in Acceptability]
App [in Encoding]

B

benchTerm [in Reflection]
bool_enc [in LBool]
bool_enc_inv [in Computability]

C

card [in Base]
cChoice [in Computability]
church_rosser [in ARS]
closed [in Lvw]
CompBeta [in LvwClos_Eval]
complement [in Decidability]
CompSeval [in LvwClos_Eval]
Comp_ind_deep [in LvwClos]
Comp_ind_deep' [in LvwClos]
confluent [in ARS]
conj [in Decidability]
converges [in Lvw]
convert [in Lvw]
convert' [in Lvw]
convI [in LTactics]
correct [in internalize_def]

D

dclosedb [in Proc]
dec [in Base]
decides [in Decidability]
decision [in Base]
deClos [in LvwClos]
denoteComp [in Reflection]
denoteTerm [in Reflection]
diamond [in ARS]
disj [in Decidability]
disjoint [in Base]
doesHaltIn [in Eval]

E

elAt [in Base]
elAt' [in internalize_tac]
enc [in internalize_def]
equi [in Base]
eva [in Seval]
eval [in Seval]
Eval [in Eval]

F

FCI.C [in Base]
FCI.F [in Base]
filter [in Base]
FP [in Base]
from_sumbool [in SumBool]
functional [in ARS]

H

helper [in intermediate]

I

I [in Lvw]
inb [in Lists]
inclp [in Base]
injective [in bijection]
int [in internalize_def]
internalizesF [in internalize_def]
inverse [in bijection]
it [in Base]

J

joinable [in ARS]

K

K [in Lvw]

L

lacc [in Acceptability]
Lam [in Encoding]
lambda [in Lvw]
ldec [in Decidability]
left_inverse [in bijection]
liftPhi [in Reflection]
lists_cons [in Lists]
list_enc [in Lists]

M

mu [in MuRec]
mu' [in MuRec]

N

name_after_dot [in StringBase]
name_after_dot' [in StringBase]
nat_S [in LNat]
nat_enc [in LNat]
normComp [in LvwClos]
normComp' [in LvwClos]

O

Omega [in Lvw]
omega [in Lvw]
on0 [in internalize_demo]
option_some [in LOptions]
option_none [in LOptions]
option_enc [in LOptions]

P

pi [in Acceptability]
Por [in Por]
pos [in Base]
pow [in ARS]
power [in Base]
Proc [in Reflection]
proc [in Lvw]
prod_enc [in LProd]
prop_enc [in LProp]

R

R [in Lvw]
r [in Lvw]
rClosed [in Reflection]
rClosed_decb [in Reflection]
rClosed_decb' [in Reflection]
rcomp [in ARS]
rCompBeta [in Reflection]
rCompSeval [in Reflection]
rCompSeval' [in Reflection]
rComp_ind_deep [in Reflection]
rComp_ind_deep' [in Reflection]
rDeClos [in Reflection]
reflection_1 [in SumBool]
reflection_2 [in SumBool]
reflexive [in ARS]
rem [in Base]
rep [in Base]
replace [in BaseLists]
rEquiv [in Reflection]
rev_string [in StringBase]
rho [in Lvw]
right_inverse [in bijection]
rReduce [in Reflection]
rSubstList [in Reflection]
rValidComp [in Reflection]

S

self_diverging_comb [in Rice]
self_diverging [in Rice]
semi_confluent [in ARS]
size [in Lvw]
String [in internalize_tac]
subst [in Lvw]
substList [in LvwClos]
subst' [in crush_no_refl_ideas]
sumbool_enc [in SumBool]
surjective [in bijection]
symmetric [in ARS]

T

tcompl [in Decidability]
tconj [in Decidability]
tdisj [in Decidability]
term_eqb [in Equality]
term_eq_dec_proc [in Lvw]
term_enc [in Encoding]
testT [in internalize_demo]
to_list [in StringBase]
to_string [in StringBase]
to_sumbool [in SumBool]
transform [in internalize_tac]
transitive [in ARS]

U

undup [in Base]
unenc [in LNat]
uniform_confluent [in ARS]
unit_enc [in internalize_demo]

V

validEnv [in LvwClos]
validEnv' [in LvwClos]
Var [in Encoding]

Record Index

I

inj_reg [in internalize_def]
internalizedClass [in internalize_def]

R

registered [in internalize_def]

Global Index

other

(837 entries)

Notation Index

other

(28 entries)

Module Index

other

(1 entry)

Variable Index

other

(38 entries)

Library Index

other

(41 entries)

Lemma Index

other

(352 entries)

Constructor Index

other

(59 entries)

Inductive Index

other

(20 entries)

Projection Index

other

(6 entries)

Section Index

other

(21 entries)

Instance Index

other

(126 entries)

Definition Index

other

(142 entries)

Record Index

other

(3 entries)