| 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 | (988 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 | (21 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 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 | (43 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 | (304 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 | (65 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 | (15 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 | (22 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 | (177 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 | (31 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 | (2 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 | (226 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 | (7 entries) |
Global Index
A
ackermann [definition, in L.Functions.Ackermann]Ackermann [library]
Ack_pos [lemma, in L.Functions.Ackermann]
app [constructor, in L.L]
app_closed [lemma, in L.L]
app_converges [lemma, in L.Computability.Seval]
argument_types [definition, in L.Tactics.Extract]
ARS [library]
B
benchTerm [definition, in L.Tactics.Reflection]bool_enc_inv_correct [lemma, in L.Computability.Computability]
bool_enc_inv [definition, in L.Computability.Computability]
both_cons [definition, in L.Reductions.MPCP_PCP]
bound [inductive, in L.L]
bound_dec [instance, in L.L]
bound_closed [lemma, in L.L]
bound_gt [lemma, in L.L]
bound_ge [lemma, in L.L]
bound_closed_k [lemma, in L.L]
C
C [constructor, in L.Computability.Synthetic]callTime2 [definition, in L.Tactics.ComputableTime]
card1 [definition, in L.Reductions.SRH_SR]
card2 [definition, in L.Reductions.SRH_SR]
cast_registeredAs [lemma, in L.Tactics.Computable]
cast_registeredAs_TimeComplexity [lemma, in L.Tactics.ComputableTime]
cast_computableTime [lemma, in L.Tactics.ComputableTactics]
cast_computable [lemma, in L.Tactics.ComputableTactics]
cChoice [definition, in L.Computability.Computability]
changeResType [definition, in L.Tactics.Computable]
changeResType_TimeComplexity [definition, in L.Tactics.ComputableTime]
church_rosser [lemma, in L.L]
church_rosser [definition, in L.Prelim.ARS]
closed [definition, in L.L]
closed_dcl_x [lemma, in L.L]
closed_star [lemma, in L.L]
closed_step [lemma, in L.L]
closed_subst [lemma, in L.L]
closed_dec [instance, in L.L]
closed_app [lemma, in L.L]
closed_dcl [lemma, in L.L]
closed_k_bound [lemma, in L.L]
cnst [definition, in L.Tactics.ComputableTime]
comb_proc_red [lemma, in L.L]
comeUp_timebound [lemma, in L.Tactics.ComputableDemo]
comeUp_timebound_withInternalTactics [definition, in L.Tactics.ComputableDemo]
Comp [inductive, in L.Tactics.LClos]
CompApp [constructor, in L.Tactics.LClos]
CompAppCount [definition, in L.Tactics.LClos_Eval]
CompBeta [definition, in L.Tactics.LClos_Eval]
CompBeta_sound [lemma, in L.Tactics.LClos_Eval]
CompBeta_validComp [lemma, in L.Tactics.LClos_Eval]
CompClos [constructor, in L.Tactics.LClos]
CompSeval [definition, in L.Tactics.LClos_Eval]
CompSeval_sound [lemma, in L.Tactics.LClos_Eval]
CompSeval_sound' [lemma, in L.Tactics.LClos_Eval]
CompSeval_validComp [lemma, in L.Tactics.LClos_Eval]
Computability [library]
computable [record, in L.Tactics.Computable]
Computable [library]
ComputableDemo [library]
computableExt [lemma, in L.Tactics.Computable]
ComputableTactics [library]
computableTime [record, in L.Tactics.ComputableTime]
ComputableTime [library]
computableTimeExt [lemma, in L.Tactics.ComputableTime]
computableTime_computable [lemma, in L.Tactics.ComputableTime]
computable_test [lemma, in L.Reductions.MPCP_PCP]
computable_P [instance, in L.Reductions.MPCP_PCP]
computable_hash_l_r [instance, in L.Reductions.MPCP_PCP]
computable_both_cons [instance, in L.Reductions.MPCP_PCP]
computable_is_cons [instance, in L.Reductions.MPCP_PCP]
computable_e [instance, in L.Reductions.MPCP_PCP]
computable_d [instance, in L.Reductions.MPCP_PCP]
computable_hash_r [instance, in L.Reductions.MPCP_PCP]
computable_hash_l [instance, in L.Reductions.MPCP_PCP]
computable_hash [instance, in L.Reductions.MPCP_PCP]
computable_dollar [instance, in L.Reductions.MPCP_PCP]
computable_Sigma [instance, in L.Reductions.MPCP_PCP]
computable_sym [instance, in L.Reductions.MPCP_PCP]
computable_fresh [instance, in L.Reductions.MPCP_PCP]
computable_hash [instance, in L.Reductions.SR_MPCP]
computable_dollar [instance, in L.Reductions.SR_MPCP]
computable_Sigma [instance, in L.Reductions.SR_MPCP]
computable_Sigma [instance, in L.Reductions.SRH_SR]
computable_gamma [instance, in L.Reductions.PCP_CFG]
computable_fn [instance, in L.Reductions.PCP_CFG]
computable_red [instance, in L.Reductions.PCP_CFG]
computable_gamma2 [instance, in L.Reductions.PCP_CFG]
computable_fn2 [instance, in L.Reductions.PCP_CFG]
computable_gamma1 [instance, in L.Reductions.PCP_CFG]
computable_fn1 [instance, in L.Reductions.PCP_CFG]
computes [definition, in L.Tactics.Computable]
computesExp [definition, in L.Tactics.Computable]
computesExpStart [lemma, in L.Tactics.Computable]
computesExpStep [lemma, in L.Tactics.Computable]
computesExt [lemma, in L.Tactics.Computable]
computesProc [lemma, in L.Tactics.Computable]
computesTime [definition, in L.Tactics.ComputableTime]
computesTimeExp [definition, in L.Tactics.ComputableTime]
computesTimeExpStart [lemma, in L.Tactics.ComputableTime]
computesTimeExpStep [lemma, in L.Tactics.ComputableTime]
computesTimeExt [lemma, in L.Tactics.ComputableTime]
computesTimeIf [definition, in L.Tactics.ComputableTime]
computesTimeIfStart [lemma, in L.Tactics.ComputableTime]
computesTimeProc [lemma, in L.Tactics.ComputableTime]
computesTimeTyArr_helper [lemma, in L.Tactics.ComputableTime]
computesTimeTyB [lemma, in L.Tactics.ComputableTime]
computesTime_computes_intern [lemma, in L.Tactics.ComputableTime]
computesTyArr [lemma, in L.Tactics.Computable]
computesTyB [lemma, in L.Tactics.Computable]
CompVar [constructor, in L.Tactics.LClos]
Comp_ind_deep [definition, in L.Tactics.LClos]
Comp_ind_deep' [definition, in L.Tactics.LClos]
confluence [lemma, in L.L]
confluent [definition, in L.Prelim.ARS]
confluent_CR [lemma, in L.Prelim.ARS]
cons' [definition, in L.Reductions.H10]
conv [definition, in L.Reductions.H10]
converges [definition, in L.L]
converges_proper [instance, in L.L]
converges_equiv [lemma, in L.L]
convert [definition, in L.L]
correctness_example [definition, in L.Tactics.ComputableDemo]
correct_recursive [definition, in L.Tactics.ComputableDemo]
CPow [inductive, in L.Tactics.LClos]
CPowApp [constructor, in L.Tactics.LClos]
CPowAppL [constructor, in L.Tactics.LClos]
CPowAppR [constructor, in L.Tactics.LClos]
CPowRefl [constructor, in L.Tactics.LClos]
CPowTrans [constructor, in L.Tactics.LClos]
CPowVal [constructor, in L.Tactics.LClos]
CPowVar [constructor, in L.Tactics.LClos]
CPow_trans [lemma, in L.Tactics.LClos]
CPow_congR [lemma, in L.Tactics.LClos]
CPow_congL [lemma, in L.Tactics.LClos]
CPow'_App_properR [instance, in L.Tactics.LClos]
cstate [projection, in L.TM.TM]
ctapes [projection, in L.TM.TM]
current [definition, in L.TM.TM]
current_chars [definition, in L.TM.TM]
D
dclApp [constructor, in L.L]dcllam [constructor, in L.L]
dclvar [constructor, in L.L]
deClos [definition, in L.Tactics.LClos]
deClos_correct [lemma, in L.Tactics.LClos]
deClos_validEnv [lemma, in L.Tactics.LClos]
deClos_valComp [lemma, in L.Tactics.LClos]
dec_P [lemma, in L.Computability.MuRec]
demo [section, in L.Tactics.ComputableDemo]
demo.PaperExample [section, in L.Tactics.ComputableDemo]
denoteComp [definition, in L.Tactics.Reflection]
denoteTerm [definition, in L.Tactics.Reflection]
denoteTerm_correct [lemma, in L.Tactics.Reflection]
dependentArgs [definition, in L.Tactics.Extract]
diamond [definition, in L.Prelim.ARS]
diamond_to_confluent [lemma, in L.Prelim.ARS]
diamond_to_semi_confluent [lemma, in L.Prelim.ARS]
doAct [definition, in L.TM.TM]
doAct_nop [lemma, in L.TM.TM]
doAct_multi [definition, in L.TM.TM]
E
ecl [inductive, in L.Prelim.ARS]eclC [constructor, in L.Prelim.ARS]
eclR [constructor, in L.Prelim.ARS]
eclS [constructor, in L.Prelim.ARS]
ecl_sym [lemma, in L.Prelim.ARS]
ecl_trans [lemma, in L.Prelim.ARS]
enc [projection, in L.Tactics.Computable]
encodable [record, in L.Tactics.Extract]
encodable [inductive, in L.Tactics.Extract]
encode_arguments [definition, in L.Tactics.GenEncode]
encode_arguments [definition, in L.Tactics.Extract]
enc_f [projection, in L.Tactics.Extract]
enc_f [constructor, in L.Tactics.Extract]
enc_extinj [lemma, in L.Computability.Computability]
enumerates [abbreviation, in L.Computability.Synthetic]
enum_poly [instance, in L.Reductions.H10]
eproc_equiv [lemma, in L.Computability.Seval]
eqApp [lemma, in L.L]
eqRef [constructor, in L.L]
eqStarT [lemma, in L.L]
eqStep [constructor, in L.L]
eqSym [constructor, in L.L]
eqTrans [constructor, in L.L]
Equality [library]
equiv [inductive, in L.L]
equiv_eval_proper [instance, in L.L]
equiv_app_proper [instance, in L.L]
equiv_lambda [lemma, in L.L]
equiv_ecl [lemma, in L.L]
equiv_Equivalence [instance, in L.L]
equiv_eva [lemma, in L.Computability.Seval]
eq_ref [lemma, in L.Prelim.ARS]
eq_inductive [definition, in L.Tactics.Extract]
eq_term_dec [lemma, in L.Computability.Computability]
error [definition, in L.Tactics.Extract]
Eta [lemma, in L.L]
eva [definition, in L.Computability.Seval]
eval [definition, in L.L]
eval [definition, in L.Reductions.H10]
evalIn [definition, in L.L]
evalIn_trans [lemma, in L.L]
evalIn_evalLe_subrelation [instance, in L.L]
evalIn_refl [lemma, in L.Tactics.Lbeta]
evalLe [definition, in L.L]
evalLe_trans_rev [lemma, in L.L]
evalLe_trans [lemma, in L.L]
evalLe_redLe_subrelation [instance, in L.L]
evalLe_eval_subrelation [instance, in L.L]
evalTime [definition, in L.Tactics.ComputableTime]
eval_star_subrelation [instance, in L.L]
eval_L_from [lemma, in L.Reductions.H10]
eval_refl [lemma, in L.Tactics.Lbeta]
eval_helper [lemma, in L.Tactics.Lbeta]
eval_seval [lemma, in L.Computability.Seval]
eval_step [lemma, in L.Computability.Seval]
eval_converges [lemma, in L.Computability.Seval]
eva_Sn_n [lemma, in L.Computability.Seval]
eva_n_Sn [lemma, in L.Computability.Seval]
eva_equiv [lemma, in L.Computability.Seval]
eva_seval [lemma, in L.Computability.Seval]
eva_lam [lemma, in L.Computability.Seval]
expandDenote [lemma, in L.Tactics.Reflection]
ext [projection, in L.Tactics.Computable]
extApp [lemma, in L.Tactics.Computable]
extApp' [instance, in L.Tactics.Computable]
extCorrect [projection, in L.Tactics.Computable]
extEq [definition, in L.Tactics.Computable]
extEq_refl [instance, in L.Tactics.Computable]
extract [definition, in L.Tactics.Extract]
Extract [library]
extracted [record, in L.Tactics.Extract]
extracted [inductive, in L.Tactics.Extract]
extract_constr [definition, in L.Tactics.Extract]
extT [projection, in L.Tactics.ComputableTime]
extTApp [lemma, in L.Tactics.ComputableTime]
extTApp' [instance, in L.Tactics.ComputableTime]
extTCorrect [projection, in L.Tactics.ComputableTime]
extT_is_enc [lemma, in L.Tactics.ComputableTime]
ext_is_enc [lemma, in L.Tactics.Computable]
F
FinR [definition, in L.TM.Prelim]finType_eqb [section, in L.TM.TMEncoding]
finType_eqb_reflect [lemma, in L.TM.TMEncoding]
finType_eqb [definition, in L.TM.TMEncoding]
FixX [section, in L.Prelim.ARS]
FixX.X [variable, in L.Prelim.ARS]
Fix_Sigma.sig [variable, in L.TM.TM]
Fix_Sigma [section, in L.TM.TM]
Fix_X.X_eqb_spec [variable, in L.Datatypes.Lists]
Fix_X.X_eqb [variable, in L.Datatypes.Lists]
Fix_X.X [variable, in L.Datatypes.Lists]
Fix_X [section, in L.Datatypes.Lists]
fix_sig.reg_tapes [section, in L.TM.TMEncoding]
fix_sig.sig [variable, in L.TM.TMEncoding]
fix_sig [section, in L.TM.TMEncoding]
Fix_X.intX [variable, in L.Datatypes.LOptions]
Fix_X.X [variable, in L.Datatypes.LOptions]
Fix_X [section, in L.Datatypes.LOptions]
Fix_XY.intY [variable, in L.Datatypes.LProd]
Fix_XY.intX [variable, in L.Datatypes.LProd]
Fix_XY.Y [variable, in L.Datatypes.LProd]
Fix_XY.X [variable, in L.Datatypes.LProd]
Fix_XY [section, in L.Datatypes.LProd]
fn [definition, in L.Reductions.PCP_CFG]
fn1 [definition, in L.Reductions.PCP_CFG]
fn2 [definition, in L.Reductions.PCP_CFG]
freeVars [definition, in L.Tactics.Extract]
FUEL [abbreviation, in L.Tactics.Extract]
functional [definition, in L.Prelim.ARS]
funTable [definition, in L.TM.TMEncoding]
funTable [section, in L.TM.TMEncoding]
funTable.eqb [variable, in L.TM.TMEncoding]
funTable.f [variable, in L.TM.TMEncoding]
funTable.Heqb [variable, in L.TM.TMEncoding]
funTable.X [variable, in L.TM.TMEncoding]
funTable.Y [variable, in L.TM.TMEncoding]
G
GenEncode [library]gen_constructor [definition, in L.Tactics.Extract]
H
ha [constructor, in L.L]halt [projection, in L.TM.TM]
Halt [definition, in L.TM.TMEncoding]
haltConf [definition, in L.TM.TM]
haltTime [definition, in L.TM.TMEncoding]
Halt_red [lemma, in L.TM.TMEncoding]
Halt_eva [lemma, in L.Reductions.TM]
Halt' [definition, in L.TM.TMEncoding]
hash_l_r [definition, in L.Reductions.MPCP_PCP]
hd [definition, in L.Tactics.Extract]
head_of_const [definition, in L.Tactics.Extract]
hl [constructor, in L.L]
hoas [inductive, in L.L]
hter [constructor, in L.L]
hv [constructor, in L.L]
H10 [library]
H10_converges [lemma, in L.Reductions.H10]
H10_enumerable [lemma, in L.Reductions.H10]
I
I [definition, in L.L]inb [definition, in L.Datatypes.Lists]
inb_spec [lemma, in L.Datatypes.Lists]
inj_enc [projection, in L.Tactics.Computable]
insertCast [definition, in L.Tactics.Computable]
insert_params [definition, in L.Tactics.Extract]
int [section, in L.Datatypes.Lists]
int [section, in L.Datatypes.LOptions]
Intern [module, in L.Tactics.ComputableTactics]
internalize_red [instance, in L.Reductions.SR_MPCP]
internalize_P [instance, in L.Reductions.SR_MPCP]
internalize_singcard [instance, in L.Reductions.SR_MPCP]
internalize_e [instance, in L.Reductions.SR_MPCP]
internalize_d [instance, in L.Reductions.SR_MPCP]
internalize_red [instance, in L.Reductions.SRH_SR]
internalize_P [instance, in L.Reductions.SRH_SR]
internalize_card2 [instance, in L.Reductions.SRH_SR]
internalize_card1 [instance, in L.Reductions.SRH_SR]
internalize_red' [instance, in L.Reductions.PCP_CFG]
internalize_Sigma [instance, in L.Reductions.PCP_CFG]
int_ext [projection, in L.Tactics.Extract]
int_ext [constructor, in L.Tactics.Extract]
int.X [variable, in L.Datatypes.LOptions]
isSome [definition, in L.Datatypes.LOptions]
is_computable [inductive, in L.Computability.Synthetic]
it_i [definition, in L.Tactics.Extract]
it_i' [definition, in L.Tactics.Extract]
it_i.f [variable, in L.Tactics.Extract]
it_i.X [variable, in L.Tactics.Extract]
it_i [section, in L.Tactics.Extract]
I_proc [lemma, in L.Tactics.Lsimpl]
J
joinable [definition, in L.Prelim.ARS]K
K [definition, in L.L]K_proc [lemma, in L.Tactics.Lsimpl]
L
L [constructor, in L.TM.TM]L [library]
lam [constructor, in L.L]
lambda [definition, in L.L]
lambdaComp [constructor, in L.Tactics.LClos]
lambda_dec [instance, in L.L]
lambda_lam [lemma, in L.L]
lamComp [inductive, in L.Tactics.LClos]
Lbeta [library]
LBool [library]
LClos [library]
LClos_Eval [library]
lcomp_comp [lemma, in L.Computability.Computability]
left [definition, in L.TM.TM]
leftof [constructor, in L.TM.TM]
length_concat [lemma, in L.Prelim.MoreList]
lenumerates [definition, in L.Computability.Synthetic]
le_evalLe_proper [instance, in L.L]
le_redLe_proper [instance, in L.L]
le_preorder [instance, in L.Prelim.MoreBase]
liftPhi [definition, in L.Tactics.Reflection]
liftPhi_correct [lemma, in L.Tactics.Reflection]
Lists [library]
list_constructors [definition, in L.Tactics.Extract]
list_prod [section, in L.Datatypes.Lists]
list_eqbTime_leq [definition, in L.Datatypes.Lists]
list_eqbTime [definition, in L.Datatypes.Lists]
list_eqb_spec [lemma, in L.Datatypes.Lists]
list_eqb [definition, in L.Datatypes.Lists]
list_eqb.spec [variable, in L.Datatypes.Lists]
list_eqb.eqb [variable, in L.Datatypes.Lists]
list_eqb.X [variable, in L.Datatypes.Lists]
list_eqb [section, in L.Datatypes.Lists]
LNat [library]
lookup [definition, in L.TM.TMEncoding]
Lookup [section, in L.TM.TMEncoding]
lookupTime [definition, in L.TM.TMEncoding]
lookupTime_leq [lemma, in L.TM.TMEncoding]
lookup_funTable [lemma, in L.TM.TMEncoding]
Lookup.eqb [variable, in L.TM.TMEncoding]
Lookup.X [variable, in L.TM.TMEncoding]
Lookup.Y [variable, in L.TM.TMEncoding]
loop [definition, in L.TM.Prelim]
Loop [section, in L.TM.Prelim]
LoopLift [section, in L.TM.Prelim]
LoopLift.A [variable, in L.TM.Prelim]
LoopLift.B [variable, in L.TM.Prelim]
LoopLift.f [variable, in L.TM.Prelim]
LoopLift.f' [variable, in L.TM.Prelim]
LoopLift.h [variable, in L.TM.Prelim]
LoopLift.halt_lift_comp [variable, in L.TM.Prelim]
LoopLift.h' [variable, in L.TM.Prelim]
LoopLift.lift [variable, in L.TM.Prelim]
LoopLift.step_lift_comp [variable, in L.TM.Prelim]
loopM [definition, in L.TM.TM]
loopM [section, in L.TM.TMEncoding]
LoopMerge [section, in L.TM.Prelim]
LoopMerge.A [variable, in L.TM.Prelim]
LoopMerge.f [variable, in L.TM.Prelim]
LoopMerge.h [variable, in L.TM.Prelim]
LoopMerge.halt_comp [variable, in L.TM.Prelim]
LoopMerge.h' [variable, in L.TM.Prelim]
loopM.M [variable, in L.TM.TMEncoding]
loopM.n [variable, in L.TM.TMEncoding]
loopM.reg_states [variable, in L.TM.TMEncoding]
loopM.reg_sig [variable, in L.TM.TMEncoding]
loopTime [definition, in L.TM.TMEncoding]
loop_split [lemma, in L.TM.Prelim]
loop_merge [lemma, in L.TM.Prelim]
loop_unlift [lemma, in L.TM.Prelim]
loop_lift [lemma, in L.TM.Prelim]
loop_monotone [lemma, in L.TM.Prelim]
loop_eq_0 [lemma, in L.TM.Prelim]
loop_0 [lemma, in L.TM.Prelim]
loop_fulfills [lemma, in L.TM.Prelim]
loop_injective [lemma, in L.TM.Prelim]
loop_step [lemma, in L.TM.Prelim]
Loop.A [variable, in L.TM.Prelim]
Loop.f [variable, in L.TM.Prelim]
Loop.p [variable, in L.TM.Prelim]
LOptions [library]
Lproc [library]
LProd [library]
Lrewrite [library]
LrewriteTime_helper [lemma, in L.Tactics.Lrewrite]
Lrewrite_in_helper [lemma, in L.Tactics.Lrewrite]
Lrewrite_equiv_helper [lemma, in L.Tactics.Lrewrite]
Lrewrite_helper [lemma, in L.Tactics.Lrewrite]
Lsimpl [library]
LTactics [library]
LTerm [library]
LUnit [library]
L_enumerable_halt [lemma, in L.Computability.Synthetic]
L_enumerable_enum [lemma, in L.Computability.Synthetic]
L_enumerable_ext [lemma, in L.Computability.Synthetic]
L_enum [definition, in L.Computability.Synthetic]
L_nat [definition, in L.Computability.Synthetic]
L_enumerable_recognisable [lemma, in L.Computability.Synthetic]
L_enum_rec.H_d [variable, in L.Computability.Synthetic]
L_enum_rec.c_d [variable, in L.Computability.Synthetic]
L_enum_rec.d [variable, in L.Computability.Synthetic]
L_enum_rec.H_f [variable, in L.Computability.Synthetic]
L_enum_rec.c_f [variable, in L.Computability.Synthetic]
L_enum_rec.f [variable, in L.Computability.Synthetic]
L_enum_rec.p [variable, in L.Computability.Synthetic]
L_enum_rec.X [variable, in L.Computability.Synthetic]
L_enum_rec [section, in L.Computability.Synthetic]
L_recognisable [definition, in L.Computability.Synthetic]
L_enumerable [definition, in L.Computability.Synthetic]
L_decidable [definition, in L.Computability.Synthetic]
L_nth [lemma, in L.Reductions.H10]
L_from [definition, in L.Reductions.H10]
L_poly [definition, in L.Reductions.H10]
M
Map [section, in L.TM.Prelim]mapTape [definition, in L.TM.TM]
MapTape [section, in L.TM.TM]
mapTapes [definition, in L.TM.TM]
mapTape_local [lemma, in L.TM.TM]
mapTape_id [lemma, in L.TM.TM]
mapTape_ext [lemma, in L.TM.TM]
mapTape_mapTape [lemma, in L.TM.TM]
mapTape_inv_midtape [lemma, in L.TM.TM]
mapTape_inv_leftof [lemma, in L.TM.TM]
mapTape_inv_rightof [lemma, in L.TM.TM]
mapTape_inv_niltap [lemma, in L.TM.TM]
mapTape_move_right [lemma, in L.TM.TM]
mapTape_move_left [lemma, in L.TM.TM]
mapTape_right [lemma, in L.TM.TM]
mapTape_left [lemma, in L.TM.TM]
mapTape_current [lemma, in L.TM.TM]
MapTape.g [variable, in L.TM.TM]
MapTape.sig [variable, in L.TM.TM]
MapTape.tau [variable, in L.TM.TM]
map_snd [definition, in L.TM.Prelim]
map_fst [definition, in L.TM.Prelim]
map_inr [definition, in L.TM.Prelim]
map_inl [definition, in L.TM.Prelim]
map_opt [definition, in L.TM.Prelim]
map_ext' [lemma, in L.Tactics.Reflection]
Map.X [variable, in L.TM.Prelim]
Map.Y [variable, in L.TM.Prelim]
Map.Z [variable, in L.TM.Prelim]
matchlem [definition, in L.Tactics.GenEncode]
MatchTapes [section, in L.TM.TM]
MatchTapes.sig [variable, in L.TM.TM]
maxP [definition, in L.Prelim.MoreBase]
max_le_proper [instance, in L.Prelim.MoreBase]
mconfig [record, in L.TM.TM]
mconfigAsPair [definition, in L.TM.TMEncoding]
midtape [constructor, in L.TM.TM]
midtape_tape_local_l_cons_right [lemma, in L.TM.TM]
midtape_tape_local_l_cons [lemma, in L.TM.TM]
midtape_tape_local_cons_left [lemma, in L.TM.TM]
midtape_tape_local_cons [lemma, in L.TM.TM]
min_le_proper [instance, in L.Prelim.MoreBase]
MirrorTape [section, in L.TM.TM]
MirrorTape.n [variable, in L.TM.TM]
MirrorTape.sig [variable, in L.TM.TM]
mirror_tape_move_right' [lemma, in L.TM.TM]
mirror_tape_move_left' [lemma, in L.TM.TM]
mirror_tapes_nth [lemma, in L.TM.TM]
mirror_move_involution [lemma, in L.TM.TM]
mirror_move [definition, in L.TM.TM]
mirror_tapes_injective [lemma, in L.TM.TM]
mirror_tapes_involution [lemma, in L.TM.TM]
mirror_tapes [definition, in L.TM.TM]
mirror_tape_inv_niltape' [lemma, in L.TM.TM]
mirror_tape_inv_rightof' [lemma, in L.TM.TM]
mirror_tape_inv_leftof' [lemma, in L.TM.TM]
mirror_tape_inv_midtape' [lemma, in L.TM.TM]
mirror_tape_inv_niltape [lemma, in L.TM.TM]
mirror_tape_inv_rightof [lemma, in L.TM.TM]
mirror_tape_inv_leftof [lemma, in L.TM.TM]
mirror_tape_inv_midtape [lemma, in L.TM.TM]
mirror_tape_move_right [lemma, in L.TM.TM]
mirror_tape_move_left [lemma, in L.TM.TM]
mirror_tape_injective [lemma, in L.TM.TM]
mirror_tape_involution [lemma, in L.TM.TM]
mirror_tape_current [lemma, in L.TM.TM]
mirror_tape_right [lemma, in L.TM.TM]
mirror_tape_left [lemma, in L.TM.TM]
mirror_tape [definition, in L.TM.TM]
mixedTactics [library]
mkApp [definition, in L.Tactics.Extract]
mkAppList [definition, in L.Tactics.Extract]
mkFixMatch [definition, in L.Tactics.Extract]
mkLam [definition, in L.Tactics.Extract]
mkLApp [definition, in L.Tactics.GenEncode]
mkMatch [definition, in L.Tactics.GenEncode]
mkNat [definition, in L.Tactics.Extract]
mkVar [definition, in L.Tactics.Extract]
mk_registered [constructor, in L.Tactics.Computable]
mk_mconfig [constructor, in L.TM.TM]
MoreBase [library]
MoreList [library]
move [inductive, in L.TM.TM]
move_finC [instance, in L.TM.TM]
move_eq_dec [instance, in L.TM.TM]
MPCP_PCP [library]
mTM [record, in L.TM.TM]
mu [definition, in L.Computability.MuRec]
mult_le_proper [instance, in L.Prelim.MoreBase]
MuRec [library]
MuRecursor [section, in L.Computability.MuRec]
MuRecursor.dec'_P [variable, in L.Computability.MuRec]
MuRecursor.P [variable, in L.Computability.MuRec]
MuRecursor.P_proc [variable, in L.Computability.MuRec]
mu_complete [lemma, in L.Computability.MuRec]
mu_sound [lemma, in L.Computability.MuRec]
mu_proc [lemma, in L.Computability.MuRec]
mu' [definition, in L.Computability.MuRec]
mu'_complete [lemma, in L.Computability.MuRec]
mu'_sound [lemma, in L.Computability.MuRec]
mu'_n_true [lemma, in L.Computability.MuRec]
mu'_0_false [lemma, in L.Computability.MuRec]
mu'_n_false [lemma, in L.Computability.MuRec]
mu'_proc [lemma, in L.Computability.MuRec]
N
N [constructor, in L.TM.TM]name_of [definition, in L.Tactics.Extract]
name_after_dot [definition, in L.Prelim.StringBase]
name_after_dot' [definition, in L.Prelim.StringBase]
natsLess [definition, in L.Prelim.MoreList]
natsLess_S [lemma, in L.Prelim.MoreList]
natsLess_in_iff [lemma, in L.Prelim.MoreList]
niltape [constructor, in L.TM.TM]
nop_action [definition, in L.TM.TM]
Nop_Action.sig [variable, in L.TM.TM]
Nop_Action.n [variable, in L.TM.TM]
Nop_Action [section, in L.TM.TM]
notHigherOrder [definition, in L.Tactics.ComputableTime]
nth_map2' [lemma, in L.TM.TM]
nth_map' [lemma, in L.TM.TM]
nth_error_Some_lt [lemma, in L.Prelim.MoreBase]
O
Omega [definition, in L.L]omega [definition, in L.L]
Omega_diverges [lemma, in L.Computability.Seval]
Omega_closed [lemma, in L.Tactics.Lsimpl]
omega_proc [lemma, in L.Tactics.Lsimpl]
on0 [definition, in L.Tactics.ComputableDemo]
option_eqb_spec [lemma, in L.Datatypes.LOptions]
option_eqb [definition, in L.Datatypes.LOptions]
option_eqb.spec [variable, in L.Datatypes.LOptions]
option_eqb.eqb [variable, in L.Datatypes.LOptions]
option_eqb.X [variable, in L.Datatypes.LOptions]
option_eqb [section, in L.Datatypes.LOptions]
P
pair' [definition, in L.Computability.Synthetic]parametrized_confluence [lemma, in L.Prelim.ARS]
parametrized_semi_confluence [lemma, in L.Prelim.ARS]
PCP_CFG [library]
phi_to_L [lemma, in L.Reductions.H10]
plus_le_proper [instance, in L.Prelim.MoreBase]
plus' [definition, in L.TM.Prelim]
poly [inductive, in L.Reductions.H10]
poly_eqb_spec [lemma, in L.Reductions.H10]
poly_eqb [definition, in L.Reductions.H10]
poly_mul' [definition, in L.Reductions.H10]
poly_add' [definition, in L.Reductions.H10]
poly_mul [constructor, in L.Reductions.H10]
poly_add [constructor, in L.Reductions.H10]
poly_var [constructor, in L.Reductions.H10]
poly_cnst [constructor, in L.Reductions.H10]
pos_nondec_spec [lemma, in L.Datatypes.Lists]
pos_nondec [definition, in L.Datatypes.Lists]
pow [definition, in L.Prelim.ARS]
powSk [lemma, in L.L]
pow_trans_lam [lemma, in L.L]
pow_trans_lam' [lemma, in L.L]
pow_redLe_subrelation [instance, in L.L]
pow_star_subrelation [instance, in L.L]
pow_trans [lemma, in L.L]
pow_step_congR [instance, in L.L]
pow_step_congL [instance, in L.L]
pow_trans_eq [lemma, in L.Tactics.Lbeta]
pow_add [lemma, in L.Prelim.ARS]
pow_star [lemma, in L.Prelim.ARS]
pow_app_helper [lemma, in L.Tactics.Lrewrite]
pow0_refl [instance, in L.L]
Prelim [library]
proc [definition, in L.L]
Proc [definition, in L.Tactics.Reflection]
proc_ext [lemma, in L.Tactics.Computable]
proc_enc [projection, in L.Tactics.Computable]
proc_dec [lemma, in L.L]
proc_test [lemma, in L.Computability.Synthetic]
proc_lambda [lemma, in L.Tactics.Lproc]
proc_closed [lemma, in L.Tactics.Lproc]
proc_extT [lemma, in L.Tactics.ComputableTime]
prod_eqb_spec [lemma, in L.Datatypes.LProd]
prod_eqb [definition, in L.Datatypes.LProd]
projection [lemma, in L.Computability.Synthetic]
pTM [definition, in L.TM.TM]
P' [definition, in L.Reductions.MPCP_PCP]
R
R [constructor, in L.TM.TM]R [definition, in L.L]
r [definition, in L.L]
rApp [constructor, in L.Tactics.Reflection]
rClosed [definition, in L.Tactics.Reflection]
rClosed_decb_correct [lemma, in L.Tactics.Reflection]
rClosed_decb [definition, in L.Tactics.Reflection]
rClosed_decb'_correct [lemma, in L.Tactics.Reflection]
rClosed_decb' [definition, in L.Tactics.Reflection]
rClosed_valid [lemma, in L.Tactics.Reflection]
rComp [inductive, in L.Tactics.Reflection]
rcomp [definition, in L.Prelim.ARS]
rCompApp [constructor, in L.Tactics.Reflection]
rCompAppCount [definition, in L.Tactics.Reflection]
rCompBeta [definition, in L.Tactics.Reflection]
rCompBeta_rValidComp [lemma, in L.Tactics.Reflection]
rCompBeta_sound [lemma, in L.Tactics.Reflection]
rCompClos [constructor, in L.Tactics.Reflection]
rCompSeval [definition, in L.Tactics.Reflection]
rCompSeval_rValidComp [lemma, in L.Tactics.Reflection]
rCompSeval_sound [lemma, in L.Tactics.Reflection]
rCompSeval' [definition, in L.Tactics.Reflection]
rCompVar [constructor, in L.Tactics.Reflection]
rComp_ind_deep [definition, in L.Tactics.Reflection]
rComp_ind_deep' [definition, in L.Tactics.Reflection]
rcomp_comm [lemma, in L.Prelim.ARS]
rcomp_1 [lemma, in L.Prelim.ARS]
rcomp_eq [lemma, in L.Prelim.ARS]
rConst [constructor, in L.Tactics.Reflection]
rDeClos [definition, in L.Tactics.Reflection]
rDeClos_rValidComp [lemma, in L.Tactics.Reflection]
rDeClos_reduce [lemma, in L.Tactics.Reflection]
red [definition, in L.Reductions.MPCP_PCP]
red [definition, in L.Reductions.SR_MPCP]
red [lemma, in L.Reductions.H10]
red [definition, in L.Reductions.SRH_SR]
redLe [definition, in L.L]
redLe_refl [instance, in L.L]
redLe_trans_eq [lemma, in L.L]
redLe_trans [lemma, in L.L]
redLe_star_subrelation [instance, in L.L]
redLe_app_helper [lemma, in L.Tactics.Lrewrite]
reduce_eval_proper [instance, in L.L]
redWithMaxSize [inductive, in L.Prelim.ARS]
redWithMaxSizeC [constructor, in L.Prelim.ARS]
redWithMaxSizeR [constructor, in L.Prelim.ARS]
redWithMaxSize_star [lemma, in L.Prelim.ARS]
redWithMaxSize_trans [lemma, in L.Prelim.ARS]
redWithMaxSize_ge [lemma, in L.Prelim.ARS]
Reflection [library]
reflexive [definition, in L.Prelim.ARS]
registerAs [lemma, in L.Tactics.Computable]
registered [record, in L.Tactics.Computable]
registered_mk_mconfig [instance, in L.TM.TMEncoding]
registered_mconfig [instance, in L.TM.TMEncoding]
registered_finType [definition, in L.TM.TMEncoding]
register_unit [instance, in L.Tactics.ComputableDemo]
register_vector [instance, in L.TM.TMEncoding]
reg_is_ext [instance, in L.Tactics.Computable]
reg_is_extT [instance, in L.Tactics.ComputableTime]
resType [definition, in L.Tactics.Computable]
rev_string [definition, in L.Prelim.StringBase]
rho [definition, in L.L]
rho_lambda [lemma, in L.L]
rho_cls [lemma, in L.L]
rho_dcls [lemma, in L.L]
rho_inj [lemma, in L.Tactics.Lsimpl]
rho_correctPow [lemma, in L.Tactics.Lsimpl]
rho_correct [lemma, in L.Tactics.Lsimpl]
right [definition, in L.TM.TM]
rightof [constructor, in L.TM.TM]
rLam [constructor, in L.Tactics.Reflection]
rPow [definition, in L.Tactics.Reflection]
rReduceIntro [lemma, in L.Tactics.Reflection]
rRho [constructor, in L.Tactics.Reflection]
rStandardize [lemma, in L.Tactics.Reflection]
rStandardizeUse [lemma, in L.Tactics.Reflection]
rStandardizeUsePow [lemma, in L.Tactics.Reflection]
rSubstList [definition, in L.Tactics.Reflection]
rSubstList_correct [lemma, in L.Tactics.Reflection]
rTerm [inductive, in L.Tactics.Reflection]
rValidComp [definition, in L.Tactics.Reflection]
rVar [constructor, in L.Tactics.Reflection]
S
Semantics [section, in L.TM.TM]Semantics.sig [variable, in L.TM.TM]
semi_confluent_confluent [lemma, in L.Prelim.ARS]
semi_confluent [definition, in L.Prelim.ARS]
seval [inductive, in L.Computability.Seval]
Seval [library]
sevalR [constructor, in L.Computability.Seval]
sevalS [constructor, in L.Computability.Seval]
seval_eva [lemma, in L.Computability.Seval]
seval_S [lemma, in L.Computability.Seval]
seval_eval [lemma, in L.Computability.Seval]
singcard [definition, in L.Reductions.SR_MPCP]
size [definition, in L.L]
sizeOfmTapes [definition, in L.TM.TM]
sizeOfTape [definition, in L.TM.TM]
size' [definition, in L.L]
split_head_symbol [definition, in L.Tactics.Extract]
SRH_SR [library]
SR_MPCP [library]
stack [definition, in L.Tactics.Extract]
star [inductive, in L.Prelim.ARS]
starC [constructor, in L.Prelim.ARS]
starR [constructor, in L.Prelim.ARS]
start [projection, in L.TM.TM]
star_equiv_subrelation [instance, in L.L]
star_equiv [lemma, in L.L]
star_closed_proper [instance, in L.L]
star_step_app_proper [instance, in L.L]
star_trans_r [lemma, in L.L]
star_trans_l [lemma, in L.L]
star_PreOrder [instance, in L.L]
star_ecl [lemma, in L.Prelim.ARS]
star_pow [lemma, in L.Prelim.ARS]
star_trans [lemma, in L.Prelim.ARS]
star_simpl_ind [lemma, in L.Prelim.ARS]
states [projection, in L.TM.TM]
step [definition, in L.TM.TM]
step [inductive, in L.L]
stepApp [constructor, in L.L]
stepAppL [constructor, in L.L]
stepAppR [constructor, in L.L]
step_equiv_subrelation [instance, in L.L]
step_star_subrelation [instance, in L.L]
step_star [lemma, in L.L]
step_Lproc [lemma, in L.L]
step' [definition, in L.TM.TMEncoding]
stHypo [lemma, in L.Tactics.Lbeta]
StringBase [library]
string_of_int [definition, in L.Tactics.Extract]
subst [definition, in L.L]
substList [definition, in L.Tactics.LClos]
substList_nil [lemma, in L.Tactics.LClos]
substList_closed' [lemma, in L.Tactics.LClos]
substList_is_bound [lemma, in L.Tactics.LClos]
substList_var [lemma, in L.Tactics.LClos]
substList_var' [lemma, in L.Tactics.LClos]
substList_closed [lemma, in L.Tactics.LClos]
substList_bound [lemma, in L.Tactics.LClos]
subst_substList [lemma, in L.Tactics.LClos]
sumn [definition, in L.Prelim.MoreList]
sumn_map_natsLess [lemma, in L.Prelim.MoreList]
sumn_rev [lemma, in L.Prelim.MoreList]
sumn_app [lemma, in L.Prelim.MoreList]
supported3 [lemma, in L.Tactics.ComputableDemo]
symmetric [definition, in L.Prelim.ARS]
Synthetic [library]
S_le_proper [instance, in L.Prelim.MoreBase]
T
tape [inductive, in L.TM.TM]tapes [definition, in L.TM.TM]
tapeToList [definition, in L.TM.TM]
tapeToList_move_L [lemma, in L.TM.TM]
tapeToList_move_R [lemma, in L.TM.TM]
tapeToList_move [lemma, in L.TM.TM]
tape_local_l_move_left' [lemma, in L.TM.TM]
tape_local_move_right' [lemma, in L.TM.TM]
tape_left_move_left' [lemma, in L.TM.TM]
tape_right_move_right' [lemma, in L.TM.TM]
tape_left_move_right' [lemma, in L.TM.TM]
tape_right_move_left' [lemma, in L.TM.TM]
tape_right_move_left [lemma, in L.TM.TM]
tape_left_move_right [lemma, in L.TM.TM]
tape_local_l_move_left [lemma, in L.TM.TM]
tape_local_move_right [lemma, in L.TM.TM]
tape_local_nil [lemma, in L.TM.TM]
tape_local_l_cons_iff [lemma, in L.TM.TM]
tape_local_cons_iff [lemma, in L.TM.TM]
tape_local_l_left [lemma, in L.TM.TM]
tape_local_right [lemma, in L.TM.TM]
tape_local_l_current_cons [lemma, in L.TM.TM]
tape_local_current_cons [lemma, in L.TM.TM]
tape_local_mirror' [lemma, in L.TM.TM]
tape_local_mirror [lemma, in L.TM.TM]
tape_local_l [definition, in L.TM.TM]
tape_local [definition, in L.TM.TM]
Tape_Local.sig [variable, in L.TM.TM]
Tape_Local [section, in L.TM.TM]
tape_write [definition, in L.TM.TM]
tape_move_left_right [lemma, in L.TM.TM]
tape_move_right_left [lemma, in L.TM.TM]
tape_move [definition, in L.TM.TM]
tape_move_left [definition, in L.TM.TM]
tape_move_left' [definition, in L.TM.TM]
tape_move_right [definition, in L.TM.TM]
tape_move_right' [definition, in L.TM.TM]
tape_is_midtape [lemma, in L.TM.TM]
tape_midtape_current_left [lemma, in L.TM.TM]
tape_midtape_current_right [lemma, in L.TM.TM]
term [inductive, in L.L]
termT_nat_eqb [instance, in L.Datatypes.LNat]
termT_leb [instance, in L.Datatypes.LNat]
termT_mult [instance, in L.Datatypes.LNat]
termT_plus [instance, in L.Datatypes.LNat]
termT_pred [instance, in L.Datatypes.LNat]
termT_S [instance, in L.Datatypes.LNat]
termT_nat_eqb [instance, in L.Functions.Universal]
termT_S [instance, in L.Functions.Universal]
termT_append [instance, in L.Datatypes.Lists]
termT_cons [instance, in L.Datatypes.Lists]
termT_ackermann [lemma, in L.Functions.Ackermann]
term_eva [instance, in L.Functions.Universal]
term_substT [instance, in L.Functions.Universal]
term_lam [instance, in L.Functions.Universal]
term_app [instance, in L.Functions.Universal]
term_var [instance, in L.Functions.Universal]
term_eq_dec_proc [definition, in L.L]
term_eq_dec [instance, in L.L]
term_ofNat [instance, in L.Computability.Synthetic]
term_R_nat_nat [instance, in L.Computability.Synthetic]
term_T_nat_nat [instance, in L.Computability.Synthetic]
term_pair' [instance, in L.Computability.Synthetic]
term_L_nat [instance, in L.Computability.Synthetic]
term_test [instance, in L.Computability.Synthetic]
term_poly_beq [instance, in L.Reductions.H10]
term_T_list [instance, in L.Reductions.H10]
term_cons' [instance, in L.Reductions.H10]
term_test_eq [instance, in L.Reductions.H10]
term_L_poly [instance, in L.Reductions.H10]
term_poly_mul' [instance, in L.Reductions.H10]
term_poly_add' [instance, in L.Reductions.H10]
term_eval [instance, in L.Reductions.H10]
term_poly_mul [instance, in L.Reductions.H10]
term_poly_add [instance, in L.Reductions.H10]
term_poly_var [instance, in L.Reductions.H10]
term_poly_cnst [instance, in L.Reductions.H10]
term_orb [instance, in L.Datatypes.LBool]
term_andb [instance, in L.Datatypes.LBool]
term_negb [instance, in L.Datatypes.LBool]
term_list_prod [instance, in L.Datatypes.Lists]
term_list_eqb [instance, in L.Datatypes.Lists]
term_rev [instance, in L.Datatypes.Lists]
term_elAt [instance, in L.Datatypes.Lists]
term_nth_error [instance, in L.Datatypes.Lists]
term_map_noTime [instance, in L.Datatypes.Lists]
term_map [instance, in L.Datatypes.Lists]
term_pos_nondec [instance, in L.Datatypes.Lists]
term_inb_notime [instance, in L.Datatypes.Lists]
term_inb [instance, in L.Datatypes.Lists]
term_nth [instance, in L.Datatypes.Lists]
term_filter_notime [instance, in L.Datatypes.Lists]
term_filter [instance, in L.Datatypes.Lists]
term_lam [instance, in L.Datatypes.LTerm]
term_app [instance, in L.Datatypes.LTerm]
term_var [instance, in L.Datatypes.LTerm]
term_nat_eqb [instance, in L.Tactics.ComputableDemo]
term_map [lemma, in L.Tactics.ComputableDemo]
term_on0 [instance, in L.Tactics.ComputableDemo]
term_eqb_spec [lemma, in L.Functions.Equality]
term_term_eqb [instance, in L.Functions.Equality]
term_eqb [definition, in L.Functions.Equality]
term_test [instance, in L.TM.TMEncoding]
term_loopM [instance, in L.TM.TMEncoding]
term_haltConf [instance, in L.TM.TMEncoding]
term_halt [instance, in L.TM.TMEncoding]
term_step' [instance, in L.TM.TMEncoding]
term_doAct_multi [instance, in L.TM.TMEncoding]
term_doAct [instance, in L.TM.TMEncoding]
term_current_chars [instance, in L.TM.TMEncoding]
term_current [instance, in L.TM.TMEncoding]
term_trans [instance, in L.TM.TMEncoding]
term_vector_eqb [instance, in L.TM.TMEncoding]
term_loop [instance, in L.TM.TMEncoding]
term_ctapes [instance, in L.TM.TMEncoding]
term_cstate [instance, in L.TM.TMEncoding]
term_mconfigAsPair [instance, in L.TM.TMEncoding]
term_tape_write [instance, in L.TM.TMEncoding]
term_right [instance, in L.TM.TMEncoding]
term_left [instance, in L.TM.TMEncoding]
term_tape_move [instance, in L.TM.TMEncoding]
term_tape_move_right [instance, in L.TM.TMEncoding]
term_tape_move_right' [instance, in L.TM.TMEncoding]
term_tape_move_left [instance, in L.TM.TMEncoding]
term_tape_move_left' [instance, in L.TM.TMEncoding]
term_midtape [instance, in L.TM.TMEncoding]
term_rightof [instance, in L.TM.TMEncoding]
term_leftof [instance, in L.TM.TMEncoding]
term_map2 [instance, in L.TM.TMEncoding]
term_vector_map [instance, in L.TM.TMEncoding]
term_to_list [instance, in L.TM.TMEncoding]
term_lookup [instance, in L.TM.TMEncoding]
term_eqb [instance, in L.TM.TMEncoding]
term_index [instance, in L.TM.TMEncoding]
term_isSome [instance, in L.Datatypes.LOptions]
term_option_eqb [instance, in L.Datatypes.LOptions]
term_Some [instance, in L.Datatypes.LOptions]
term_ackermann [lemma, in L.Functions.Ackermann]
term_prod_eqb_notime [instance, in L.Datatypes.LProd]
term_prod_eqb [instance, in L.Datatypes.LProd]
term_snd [instance, in L.Datatypes.LProd]
term_fst [instance, in L.Datatypes.LProd]
term_pair [instance, in L.Datatypes.LProd]
test [definition, in L.Computability.Synthetic]
test_eq [definition, in L.Reductions.H10]
test_Some_nat [lemma, in L.Tactics.ComputableDemo]
TH [definition, in L.L]
timeComplexity [definition, in L.Tactics.ComputableTime]
time_map2_leq [lemma, in L.TM.TMEncoding]
time_map2 [definition, in L.TM.TMEncoding]
TM [library]
TM [library]
tmArgsOfConstructor [definition, in L.Tactics.Extract]
tmDependentArgs [definition, in L.Tactics.Extract]
tmEncode [definition, in L.Tactics.Extract]
TMEncoding [library]
tmExtract [definition, in L.Tactics.Extract]
tmExtractConstr [definition, in L.Tactics.Extract]
tmExtractConstr' [definition, in L.Tactics.Extract]
tmGenEncode [definition, in L.Tactics.GenEncode]
tmGetOption [definition, in L.Tactics.Extract]
tmIsType [definition, in L.Tactics.Extract]
tmMatchCorrect [definition, in L.Tactics.GenEncode]
tmNumConstructors [definition, in L.Tactics.Extract]
tmTryInfer [definition, in L.Tactics.Extract]
tmTypeOf [definition, in L.Tactics.Extract]
tmUnfoldTerm [definition, in L.Tactics.Extract]
to_list_length [lemma, in L.TM.TMEncoding]
to_list [definition, in L.Prelim.StringBase]
to_string [definition, in L.Prelim.StringBase]
trans [projection, in L.TM.TM]
transitive [definition, in L.Prelim.ARS]
transTime [definition, in L.TM.TMEncoding]
TT [inductive, in L.Tactics.Computable]
TyArr [constructor, in L.Tactics.Computable]
TyB [constructor, in L.Tactics.Computable]
T_nat_nat [definition, in L.Computability.Synthetic]
T_list_nat [definition, in L.Reductions.H10]
U
uniform_confluence [lemma, in L.L]uniform_confluent_noloop [lemma, in L.Prelim.ARS]
uniform_confluent [definition, in L.Prelim.ARS]
unique_normal_forms [lemma, in L.L]
unit_enc [definition, in L.Tactics.ComputableDemo]
Universal [library]
unsupported [lemma, in L.Tactics.ComputableDemo]
unsupported2 [lemma, in L.Tactics.ComputableDemo]
V
validComp [inductive, in L.Tactics.LClos]validCompApp [constructor, in L.Tactics.LClos]
validCompClos [constructor, in L.Tactics.LClos]
validComp_closed [lemma, in L.Tactics.LClos]
validComp_step [lemma, in L.Tactics.LClos]
validEnv [definition, in L.Tactics.LClos]
validEnv_cons [lemma, in L.Tactics.LClos]
validEnv' [definition, in L.Tactics.LClos]
validEnv'_cons [lemma, in L.Tactics.LClos]
var [constructor, in L.L]
W
workarround [lemma, in L.Tactics.ComputableDemo]other
_ >[( _ )] _ (LClos) [notation, in L.Tactics.LClos]_ ~> _ [notation, in L.Tactics.Computable]
_ ⇓(<= _ ) _ [notation, in L.L]
_ >(<= _ ) _ [notation, in L.L]
_ ⇓( _ ) _ [notation, in L.L]
_ ⇓ _ [notation, in L.L]
_ == _ [notation, in L.L]
_ >* _ [notation, in L.L]
_ >( _ ) _ [notation, in L.L]
_ >> _ [notation, in L.L]
_ =2 _ [notation, in L.Prelim.ARS]
_ <=2 _ [notation, in L.Prelim.ARS]
_ =1 _ [notation, in L.Prelim.ARS]
_ <=1 _ [notation, in L.Prelim.ARS]
_ ⇓ _ _ [notation, in L.Computability.Seval]
computableTime _ [notation, in L.Tactics.ComputableTactics]
!! _ [notation, in L.L]
! _ [notation, in L.Tactics.Computable]
# _ [notation, in L.L]
↑ _ [notation, in L.Tactics.Extract]
λ _ .. _ , _ [notation, in L.L]
Notation Index
other
_ >[( _ )] _ (LClos) [in L.Tactics.LClos]_ ~> _ [in L.Tactics.Computable]
_ ⇓(<= _ ) _ [in L.L]
_ >(<= _ ) _ [in L.L]
_ ⇓( _ ) _ [in L.L]
_ ⇓ _ [in L.L]
_ == _ [in L.L]
_ >* _ [in L.L]
_ >( _ ) _ [in L.L]
_ >> _ [in L.L]
_ =2 _ [in L.Prelim.ARS]
_ <=2 _ [in L.Prelim.ARS]
_ =1 _ [in L.Prelim.ARS]
_ <=1 _ [in L.Prelim.ARS]
_ ⇓ _ _ [in L.Computability.Seval]
computableTime _ [in L.Tactics.ComputableTactics]
!! _ [in L.L]
! _ [in L.Tactics.Computable]
# _ [in L.L]
↑ _ [in L.Tactics.Extract]
λ _ .. _ , _ [in L.L]
Module Index
I
Intern [in L.Tactics.ComputableTactics]Variable Index
F
FixX.X [in L.Prelim.ARS]Fix_Sigma.sig [in L.TM.TM]
Fix_X.X_eqb_spec [in L.Datatypes.Lists]
Fix_X.X_eqb [in L.Datatypes.Lists]
Fix_X.X [in L.Datatypes.Lists]
fix_sig.sig [in L.TM.TMEncoding]
Fix_X.intX [in L.Datatypes.LOptions]
Fix_X.X [in L.Datatypes.LOptions]
Fix_XY.intY [in L.Datatypes.LProd]
Fix_XY.intX [in L.Datatypes.LProd]
Fix_XY.Y [in L.Datatypes.LProd]
Fix_XY.X [in L.Datatypes.LProd]
funTable.eqb [in L.TM.TMEncoding]
funTable.f [in L.TM.TMEncoding]
funTable.Heqb [in L.TM.TMEncoding]
funTable.X [in L.TM.TMEncoding]
funTable.Y [in L.TM.TMEncoding]
I
int.X [in L.Datatypes.LOptions]it_i.f [in L.Tactics.Extract]
it_i.X [in L.Tactics.Extract]
L
list_eqb.spec [in L.Datatypes.Lists]list_eqb.eqb [in L.Datatypes.Lists]
list_eqb.X [in L.Datatypes.Lists]
Lookup.eqb [in L.TM.TMEncoding]
Lookup.X [in L.TM.TMEncoding]
Lookup.Y [in L.TM.TMEncoding]
LoopLift.A [in L.TM.Prelim]
LoopLift.B [in L.TM.Prelim]
LoopLift.f [in L.TM.Prelim]
LoopLift.f' [in L.TM.Prelim]
LoopLift.h [in L.TM.Prelim]
LoopLift.halt_lift_comp [in L.TM.Prelim]
LoopLift.h' [in L.TM.Prelim]
LoopLift.lift [in L.TM.Prelim]
LoopLift.step_lift_comp [in L.TM.Prelim]
LoopMerge.A [in L.TM.Prelim]
LoopMerge.f [in L.TM.Prelim]
LoopMerge.h [in L.TM.Prelim]
LoopMerge.halt_comp [in L.TM.Prelim]
LoopMerge.h' [in L.TM.Prelim]
loopM.M [in L.TM.TMEncoding]
loopM.n [in L.TM.TMEncoding]
loopM.reg_states [in L.TM.TMEncoding]
loopM.reg_sig [in L.TM.TMEncoding]
Loop.A [in L.TM.Prelim]
Loop.f [in L.TM.Prelim]
Loop.p [in L.TM.Prelim]
L_enum_rec.H_d [in L.Computability.Synthetic]
L_enum_rec.c_d [in L.Computability.Synthetic]
L_enum_rec.d [in L.Computability.Synthetic]
L_enum_rec.H_f [in L.Computability.Synthetic]
L_enum_rec.c_f [in L.Computability.Synthetic]
L_enum_rec.f [in L.Computability.Synthetic]
L_enum_rec.p [in L.Computability.Synthetic]
L_enum_rec.X [in L.Computability.Synthetic]
M
MapTape.g [in L.TM.TM]MapTape.sig [in L.TM.TM]
MapTape.tau [in L.TM.TM]
Map.X [in L.TM.Prelim]
Map.Y [in L.TM.Prelim]
Map.Z [in L.TM.Prelim]
MatchTapes.sig [in L.TM.TM]
MirrorTape.n [in L.TM.TM]
MirrorTape.sig [in L.TM.TM]
MuRecursor.dec'_P [in L.Computability.MuRec]
MuRecursor.P [in L.Computability.MuRec]
MuRecursor.P_proc [in L.Computability.MuRec]
N
Nop_Action.sig [in L.TM.TM]Nop_Action.n [in L.TM.TM]
O
option_eqb.spec [in L.Datatypes.LOptions]option_eqb.eqb [in L.Datatypes.LOptions]
option_eqb.X [in L.Datatypes.LOptions]
S
Semantics.sig [in L.TM.TM]T
Tape_Local.sig [in L.TM.TM]Library Index
A
AckermannARS
C
ComputabilityComputable
ComputableDemo
ComputableTactics
ComputableTime
E
EqualityExtract
G
GenEncodeH
H10L
LLbeta
LBool
LClos
LClos_Eval
Lists
LNat
LOptions
Lproc
LProd
Lrewrite
Lsimpl
LTactics
LTerm
LUnit
M
mixedTacticsMoreBase
MoreList
MPCP_PCP
MuRec
P
PCP_CFGPrelim
R
ReflectionS
SevalSRH_SR
SR_MPCP
StringBase
Synthetic
T
TMTM
TMEncoding
U
UniversalLemma Index
A
Ack_pos [in L.Functions.Ackermann]app_closed [in L.L]
app_converges [in L.Computability.Seval]
B
bool_enc_inv_correct [in L.Computability.Computability]bound_closed [in L.L]
bound_gt [in L.L]
bound_ge [in L.L]
bound_closed_k [in L.L]
C
cast_registeredAs [in L.Tactics.Computable]cast_registeredAs_TimeComplexity [in L.Tactics.ComputableTime]
cast_computableTime [in L.Tactics.ComputableTactics]
cast_computable [in L.Tactics.ComputableTactics]
church_rosser [in L.L]
closed_dcl_x [in L.L]
closed_star [in L.L]
closed_step [in L.L]
closed_subst [in L.L]
closed_app [in L.L]
closed_dcl [in L.L]
closed_k_bound [in L.L]
comb_proc_red [in L.L]
comeUp_timebound [in L.Tactics.ComputableDemo]
CompBeta_sound [in L.Tactics.LClos_Eval]
CompBeta_validComp [in L.Tactics.LClos_Eval]
CompSeval_sound [in L.Tactics.LClos_Eval]
CompSeval_sound' [in L.Tactics.LClos_Eval]
CompSeval_validComp [in L.Tactics.LClos_Eval]
computableExt [in L.Tactics.Computable]
computableTimeExt [in L.Tactics.ComputableTime]
computableTime_computable [in L.Tactics.ComputableTime]
computable_test [in L.Reductions.MPCP_PCP]
computesExpStart [in L.Tactics.Computable]
computesExpStep [in L.Tactics.Computable]
computesExt [in L.Tactics.Computable]
computesProc [in L.Tactics.Computable]
computesTimeExpStart [in L.Tactics.ComputableTime]
computesTimeExpStep [in L.Tactics.ComputableTime]
computesTimeExt [in L.Tactics.ComputableTime]
computesTimeIfStart [in L.Tactics.ComputableTime]
computesTimeProc [in L.Tactics.ComputableTime]
computesTimeTyArr_helper [in L.Tactics.ComputableTime]
computesTimeTyB [in L.Tactics.ComputableTime]
computesTime_computes_intern [in L.Tactics.ComputableTime]
computesTyArr [in L.Tactics.Computable]
computesTyB [in L.Tactics.Computable]
confluence [in L.L]
confluent_CR [in L.Prelim.ARS]
converges_equiv [in L.L]
CPow_trans [in L.Tactics.LClos]
CPow_congR [in L.Tactics.LClos]
CPow_congL [in L.Tactics.LClos]
D
deClos_correct [in L.Tactics.LClos]deClos_validEnv [in L.Tactics.LClos]
deClos_valComp [in L.Tactics.LClos]
dec_P [in L.Computability.MuRec]
denoteTerm_correct [in L.Tactics.Reflection]
diamond_to_confluent [in L.Prelim.ARS]
diamond_to_semi_confluent [in L.Prelim.ARS]
doAct_nop [in L.TM.TM]
E
ecl_sym [in L.Prelim.ARS]ecl_trans [in L.Prelim.ARS]
enc_extinj [in L.Computability.Computability]
eproc_equiv [in L.Computability.Seval]
eqApp [in L.L]
eqStarT [in L.L]
equiv_lambda [in L.L]
equiv_ecl [in L.L]
equiv_eva [in L.Computability.Seval]
eq_ref [in L.Prelim.ARS]
eq_term_dec [in L.Computability.Computability]
Eta [in L.L]
evalIn_trans [in L.L]
evalIn_refl [in L.Tactics.Lbeta]
evalLe_trans_rev [in L.L]
evalLe_trans [in L.L]
eval_L_from [in L.Reductions.H10]
eval_refl [in L.Tactics.Lbeta]
eval_helper [in L.Tactics.Lbeta]
eval_seval [in L.Computability.Seval]
eval_step [in L.Computability.Seval]
eval_converges [in L.Computability.Seval]
eva_Sn_n [in L.Computability.Seval]
eva_n_Sn [in L.Computability.Seval]
eva_equiv [in L.Computability.Seval]
eva_seval [in L.Computability.Seval]
eva_lam [in L.Computability.Seval]
expandDenote [in L.Tactics.Reflection]
extApp [in L.Tactics.Computable]
extTApp [in L.Tactics.ComputableTime]
extT_is_enc [in L.Tactics.ComputableTime]
ext_is_enc [in L.Tactics.Computable]
F
finType_eqb_reflect [in L.TM.TMEncoding]H
Halt_red [in L.TM.TMEncoding]Halt_eva [in L.Reductions.TM]
H10_converges [in L.Reductions.H10]
H10_enumerable [in L.Reductions.H10]
I
inb_spec [in L.Datatypes.Lists]I_proc [in L.Tactics.Lsimpl]
K
K_proc [in L.Tactics.Lsimpl]L
lambda_lam [in L.L]lcomp_comp [in L.Computability.Computability]
length_concat [in L.Prelim.MoreList]
liftPhi_correct [in L.Tactics.Reflection]
list_eqb_spec [in L.Datatypes.Lists]
lookupTime_leq [in L.TM.TMEncoding]
lookup_funTable [in L.TM.TMEncoding]
loop_split [in L.TM.Prelim]
loop_merge [in L.TM.Prelim]
loop_unlift [in L.TM.Prelim]
loop_lift [in L.TM.Prelim]
loop_monotone [in L.TM.Prelim]
loop_eq_0 [in L.TM.Prelim]
loop_0 [in L.TM.Prelim]
loop_fulfills [in L.TM.Prelim]
loop_injective [in L.TM.Prelim]
loop_step [in L.TM.Prelim]
LrewriteTime_helper [in L.Tactics.Lrewrite]
Lrewrite_in_helper [in L.Tactics.Lrewrite]
Lrewrite_equiv_helper [in L.Tactics.Lrewrite]
Lrewrite_helper [in L.Tactics.Lrewrite]
L_enumerable_halt [in L.Computability.Synthetic]
L_enumerable_enum [in L.Computability.Synthetic]
L_enumerable_ext [in L.Computability.Synthetic]
L_enumerable_recognisable [in L.Computability.Synthetic]
L_nth [in L.Reductions.H10]
M
mapTape_local [in L.TM.TM]mapTape_id [in L.TM.TM]
mapTape_ext [in L.TM.TM]
mapTape_mapTape [in L.TM.TM]
mapTape_inv_midtape [in L.TM.TM]
mapTape_inv_leftof [in L.TM.TM]
mapTape_inv_rightof [in L.TM.TM]
mapTape_inv_niltap [in L.TM.TM]
mapTape_move_right [in L.TM.TM]
mapTape_move_left [in L.TM.TM]
mapTape_right [in L.TM.TM]
mapTape_left [in L.TM.TM]
mapTape_current [in L.TM.TM]
map_ext' [in L.Tactics.Reflection]
midtape_tape_local_l_cons_right [in L.TM.TM]
midtape_tape_local_l_cons [in L.TM.TM]
midtape_tape_local_cons_left [in L.TM.TM]
midtape_tape_local_cons [in L.TM.TM]
mirror_tape_move_right' [in L.TM.TM]
mirror_tape_move_left' [in L.TM.TM]
mirror_tapes_nth [in L.TM.TM]
mirror_move_involution [in L.TM.TM]
mirror_tapes_injective [in L.TM.TM]
mirror_tapes_involution [in L.TM.TM]
mirror_tape_inv_niltape' [in L.TM.TM]
mirror_tape_inv_rightof' [in L.TM.TM]
mirror_tape_inv_leftof' [in L.TM.TM]
mirror_tape_inv_midtape' [in L.TM.TM]
mirror_tape_inv_niltape [in L.TM.TM]
mirror_tape_inv_rightof [in L.TM.TM]
mirror_tape_inv_leftof [in L.TM.TM]
mirror_tape_inv_midtape [in L.TM.TM]
mirror_tape_move_right [in L.TM.TM]
mirror_tape_move_left [in L.TM.TM]
mirror_tape_injective [in L.TM.TM]
mirror_tape_involution [in L.TM.TM]
mirror_tape_current [in L.TM.TM]
mirror_tape_right [in L.TM.TM]
mirror_tape_left [in L.TM.TM]
mu_complete [in L.Computability.MuRec]
mu_sound [in L.Computability.MuRec]
mu_proc [in L.Computability.MuRec]
mu'_complete [in L.Computability.MuRec]
mu'_sound [in L.Computability.MuRec]
mu'_n_true [in L.Computability.MuRec]
mu'_0_false [in L.Computability.MuRec]
mu'_n_false [in L.Computability.MuRec]
mu'_proc [in L.Computability.MuRec]
N
natsLess_S [in L.Prelim.MoreList]natsLess_in_iff [in L.Prelim.MoreList]
nth_map2' [in L.TM.TM]
nth_map' [in L.TM.TM]
nth_error_Some_lt [in L.Prelim.MoreBase]
O
Omega_diverges [in L.Computability.Seval]Omega_closed [in L.Tactics.Lsimpl]
omega_proc [in L.Tactics.Lsimpl]
option_eqb_spec [in L.Datatypes.LOptions]
P
parametrized_confluence [in L.Prelim.ARS]parametrized_semi_confluence [in L.Prelim.ARS]
phi_to_L [in L.Reductions.H10]
poly_eqb_spec [in L.Reductions.H10]
pos_nondec_spec [in L.Datatypes.Lists]
powSk [in L.L]
pow_trans_lam [in L.L]
pow_trans_lam' [in L.L]
pow_trans [in L.L]
pow_trans_eq [in L.Tactics.Lbeta]
pow_add [in L.Prelim.ARS]
pow_star [in L.Prelim.ARS]
pow_app_helper [in L.Tactics.Lrewrite]
proc_ext [in L.Tactics.Computable]
proc_dec [in L.L]
proc_test [in L.Computability.Synthetic]
proc_lambda [in L.Tactics.Lproc]
proc_closed [in L.Tactics.Lproc]
proc_extT [in L.Tactics.ComputableTime]
prod_eqb_spec [in L.Datatypes.LProd]
projection [in L.Computability.Synthetic]
R
rClosed_decb_correct [in L.Tactics.Reflection]rClosed_decb'_correct [in L.Tactics.Reflection]
rClosed_valid [in L.Tactics.Reflection]
rCompBeta_rValidComp [in L.Tactics.Reflection]
rCompBeta_sound [in L.Tactics.Reflection]
rCompSeval_rValidComp [in L.Tactics.Reflection]
rCompSeval_sound [in L.Tactics.Reflection]
rcomp_comm [in L.Prelim.ARS]
rcomp_1 [in L.Prelim.ARS]
rcomp_eq [in L.Prelim.ARS]
rDeClos_rValidComp [in L.Tactics.Reflection]
rDeClos_reduce [in L.Tactics.Reflection]
red [in L.Reductions.H10]
redLe_trans_eq [in L.L]
redLe_trans [in L.L]
redLe_app_helper [in L.Tactics.Lrewrite]
redWithMaxSize_star [in L.Prelim.ARS]
redWithMaxSize_trans [in L.Prelim.ARS]
redWithMaxSize_ge [in L.Prelim.ARS]
registerAs [in L.Tactics.Computable]
rho_lambda [in L.L]
rho_cls [in L.L]
rho_dcls [in L.L]
rho_inj [in L.Tactics.Lsimpl]
rho_correctPow [in L.Tactics.Lsimpl]
rho_correct [in L.Tactics.Lsimpl]
rReduceIntro [in L.Tactics.Reflection]
rStandardize [in L.Tactics.Reflection]
rStandardizeUse [in L.Tactics.Reflection]
rStandardizeUsePow [in L.Tactics.Reflection]
rSubstList_correct [in L.Tactics.Reflection]
S
semi_confluent_confluent [in L.Prelim.ARS]seval_eva [in L.Computability.Seval]
seval_S [in L.Computability.Seval]
seval_eval [in L.Computability.Seval]
star_equiv [in L.L]
star_trans_r [in L.L]
star_trans_l [in L.L]
star_ecl [in L.Prelim.ARS]
star_pow [in L.Prelim.ARS]
star_trans [in L.Prelim.ARS]
star_simpl_ind [in L.Prelim.ARS]
step_star [in L.L]
step_Lproc [in L.L]
stHypo [in L.Tactics.Lbeta]
substList_nil [in L.Tactics.LClos]
substList_closed' [in L.Tactics.LClos]
substList_is_bound [in L.Tactics.LClos]
substList_var [in L.Tactics.LClos]
substList_var' [in L.Tactics.LClos]
substList_closed [in L.Tactics.LClos]
substList_bound [in L.Tactics.LClos]
subst_substList [in L.Tactics.LClos]
sumn_map_natsLess [in L.Prelim.MoreList]
sumn_rev [in L.Prelim.MoreList]
sumn_app [in L.Prelim.MoreList]
supported3 [in L.Tactics.ComputableDemo]
T
tapeToList_move_L [in L.TM.TM]tapeToList_move_R [in L.TM.TM]
tapeToList_move [in L.TM.TM]
tape_local_l_move_left' [in L.TM.TM]
tape_local_move_right' [in L.TM.TM]
tape_left_move_left' [in L.TM.TM]
tape_right_move_right' [in L.TM.TM]
tape_left_move_right' [in L.TM.TM]
tape_right_move_left' [in L.TM.TM]
tape_right_move_left [in L.TM.TM]
tape_left_move_right [in L.TM.TM]
tape_local_l_move_left [in L.TM.TM]
tape_local_move_right [in L.TM.TM]
tape_local_nil [in L.TM.TM]
tape_local_l_cons_iff [in L.TM.TM]
tape_local_cons_iff [in L.TM.TM]
tape_local_l_left [in L.TM.TM]
tape_local_right [in L.TM.TM]
tape_local_l_current_cons [in L.TM.TM]
tape_local_current_cons [in L.TM.TM]
tape_local_mirror' [in L.TM.TM]
tape_local_mirror [in L.TM.TM]
tape_move_left_right [in L.TM.TM]
tape_move_right_left [in L.TM.TM]
tape_is_midtape [in L.TM.TM]
tape_midtape_current_left [in L.TM.TM]
tape_midtape_current_right [in L.TM.TM]
termT_ackermann [in L.Functions.Ackermann]
term_map [in L.Tactics.ComputableDemo]
term_eqb_spec [in L.Functions.Equality]
term_ackermann [in L.Functions.Ackermann]
test_Some_nat [in L.Tactics.ComputableDemo]
time_map2_leq [in L.TM.TMEncoding]
to_list_length [in L.TM.TMEncoding]
U
uniform_confluence [in L.L]uniform_confluent_noloop [in L.Prelim.ARS]
unique_normal_forms [in L.L]
unsupported [in L.Tactics.ComputableDemo]
unsupported2 [in L.Tactics.ComputableDemo]
V
validComp_closed [in L.Tactics.LClos]validComp_step [in L.Tactics.LClos]
validEnv_cons [in L.Tactics.LClos]
validEnv'_cons [in L.Tactics.LClos]
W
workarround [in L.Tactics.ComputableDemo]Constructor Index
A
app [in L.L]C
C [in L.Computability.Synthetic]CompApp [in L.Tactics.LClos]
CompClos [in L.Tactics.LClos]
CompVar [in L.Tactics.LClos]
CPowApp [in L.Tactics.LClos]
CPowAppL [in L.Tactics.LClos]
CPowAppR [in L.Tactics.LClos]
CPowRefl [in L.Tactics.LClos]
CPowTrans [in L.Tactics.LClos]
CPowVal [in L.Tactics.LClos]
CPowVar [in L.Tactics.LClos]
D
dclApp [in L.L]dcllam [in L.L]
dclvar [in L.L]
E
eclC [in L.Prelim.ARS]eclR [in L.Prelim.ARS]
eclS [in L.Prelim.ARS]
enc_f [in L.Tactics.Extract]
eqRef [in L.L]
eqStep [in L.L]
eqSym [in L.L]
eqTrans [in L.L]
H
ha [in L.L]hl [in L.L]
hter [in L.L]
hv [in L.L]
I
int_ext [in L.Tactics.Extract]L
L [in L.TM.TM]lam [in L.L]
lambdaComp [in L.Tactics.LClos]
leftof [in L.TM.TM]
M
midtape [in L.TM.TM]mk_registered [in L.Tactics.Computable]
mk_mconfig [in L.TM.TM]
N
N [in L.TM.TM]niltape [in L.TM.TM]
P
poly_mul [in L.Reductions.H10]poly_add [in L.Reductions.H10]
poly_var [in L.Reductions.H10]
poly_cnst [in L.Reductions.H10]
R
R [in L.TM.TM]rApp [in L.Tactics.Reflection]
rCompApp [in L.Tactics.Reflection]
rCompClos [in L.Tactics.Reflection]
rCompVar [in L.Tactics.Reflection]
rConst [in L.Tactics.Reflection]
redWithMaxSizeC [in L.Prelim.ARS]
redWithMaxSizeR [in L.Prelim.ARS]
rightof [in L.TM.TM]
rLam [in L.Tactics.Reflection]
rRho [in L.Tactics.Reflection]
rVar [in L.Tactics.Reflection]
S
sevalR [in L.Computability.Seval]sevalS [in L.Computability.Seval]
starC [in L.Prelim.ARS]
starR [in L.Prelim.ARS]
stepApp [in L.L]
stepAppL [in L.L]
stepAppR [in L.L]
T
TyArr [in L.Tactics.Computable]TyB [in L.Tactics.Computable]
V
validCompApp [in L.Tactics.LClos]validCompClos [in L.Tactics.LClos]
var [in L.L]
Projection Index
C
cstate [in L.TM.TM]ctapes [in L.TM.TM]
E
enc [in L.Tactics.Computable]enc_f [in L.Tactics.Extract]
ext [in L.Tactics.Computable]
extCorrect [in L.Tactics.Computable]
extT [in L.Tactics.ComputableTime]
extTCorrect [in L.Tactics.ComputableTime]
H
halt [in L.TM.TM]I
inj_enc [in L.Tactics.Computable]int_ext [in L.Tactics.Extract]
P
proc_enc [in L.Tactics.Computable]S
start [in L.TM.TM]states [in L.TM.TM]
T
trans [in L.TM.TM]Inductive Index
B
bound [in L.L]C
Comp [in L.Tactics.LClos]CPow [in L.Tactics.LClos]
E
ecl [in L.Prelim.ARS]encodable [in L.Tactics.Extract]
equiv [in L.L]
extracted [in L.Tactics.Extract]
H
hoas [in L.L]I
is_computable [in L.Computability.Synthetic]L
lamComp [in L.Tactics.LClos]M
move [in L.TM.TM]P
poly [in L.Reductions.H10]R
rComp [in L.Tactics.Reflection]redWithMaxSize [in L.Prelim.ARS]
rTerm [in L.Tactics.Reflection]
S
seval [in L.Computability.Seval]star [in L.Prelim.ARS]
step [in L.L]
T
tape [in L.TM.TM]term [in L.L]
TT [in L.Tactics.Computable]
V
validComp [in L.Tactics.LClos]Instance Index
B
bound_dec [in L.L]C
closed_dec [in L.L]computable_P [in L.Reductions.MPCP_PCP]
computable_hash_l_r [in L.Reductions.MPCP_PCP]
computable_both_cons [in L.Reductions.MPCP_PCP]
computable_is_cons [in L.Reductions.MPCP_PCP]
computable_e [in L.Reductions.MPCP_PCP]
computable_d [in L.Reductions.MPCP_PCP]
computable_hash_r [in L.Reductions.MPCP_PCP]
computable_hash_l [in L.Reductions.MPCP_PCP]
computable_hash [in L.Reductions.MPCP_PCP]
computable_dollar [in L.Reductions.MPCP_PCP]
computable_Sigma [in L.Reductions.MPCP_PCP]
computable_sym [in L.Reductions.MPCP_PCP]
computable_fresh [in L.Reductions.MPCP_PCP]
computable_hash [in L.Reductions.SR_MPCP]
computable_dollar [in L.Reductions.SR_MPCP]
computable_Sigma [in L.Reductions.SR_MPCP]
computable_Sigma [in L.Reductions.SRH_SR]
computable_gamma [in L.Reductions.PCP_CFG]
computable_fn [in L.Reductions.PCP_CFG]
computable_red [in L.Reductions.PCP_CFG]
computable_gamma2 [in L.Reductions.PCP_CFG]
computable_fn2 [in L.Reductions.PCP_CFG]
computable_gamma1 [in L.Reductions.PCP_CFG]
computable_fn1 [in L.Reductions.PCP_CFG]
converges_proper [in L.L]
CPow'_App_properR [in L.Tactics.LClos]
E
enum_poly [in L.Reductions.H10]equiv_eval_proper [in L.L]
equiv_app_proper [in L.L]
equiv_Equivalence [in L.L]
evalIn_evalLe_subrelation [in L.L]
evalLe_redLe_subrelation [in L.L]
evalLe_eval_subrelation [in L.L]
eval_star_subrelation [in L.L]
extApp' [in L.Tactics.Computable]
extEq_refl [in L.Tactics.Computable]
extTApp' [in L.Tactics.ComputableTime]
I
internalize_red [in L.Reductions.SR_MPCP]internalize_P [in L.Reductions.SR_MPCP]
internalize_singcard [in L.Reductions.SR_MPCP]
internalize_e [in L.Reductions.SR_MPCP]
internalize_d [in L.Reductions.SR_MPCP]
internalize_red [in L.Reductions.SRH_SR]
internalize_P [in L.Reductions.SRH_SR]
internalize_card2 [in L.Reductions.SRH_SR]
internalize_card1 [in L.Reductions.SRH_SR]
internalize_red' [in L.Reductions.PCP_CFG]
internalize_Sigma [in L.Reductions.PCP_CFG]
L
lambda_dec [in L.L]le_evalLe_proper [in L.L]
le_redLe_proper [in L.L]
le_preorder [in L.Prelim.MoreBase]
M
max_le_proper [in L.Prelim.MoreBase]min_le_proper [in L.Prelim.MoreBase]
move_finC [in L.TM.TM]
move_eq_dec [in L.TM.TM]
mult_le_proper [in L.Prelim.MoreBase]
P
plus_le_proper [in L.Prelim.MoreBase]pow_redLe_subrelation [in L.L]
pow_star_subrelation [in L.L]
pow_step_congR [in L.L]
pow_step_congL [in L.L]
pow0_refl [in L.L]
R
redLe_refl [in L.L]redLe_star_subrelation [in L.L]
reduce_eval_proper [in L.L]
registered_mk_mconfig [in L.TM.TMEncoding]
registered_mconfig [in L.TM.TMEncoding]
register_unit [in L.Tactics.ComputableDemo]
register_vector [in L.TM.TMEncoding]
reg_is_ext [in L.Tactics.Computable]
reg_is_extT [in L.Tactics.ComputableTime]
S
star_equiv_subrelation [in L.L]star_closed_proper [in L.L]
star_step_app_proper [in L.L]
star_PreOrder [in L.L]
step_equiv_subrelation [in L.L]
step_star_subrelation [in L.L]
S_le_proper [in L.Prelim.MoreBase]
T
termT_nat_eqb [in L.Datatypes.LNat]termT_leb [in L.Datatypes.LNat]
termT_mult [in L.Datatypes.LNat]
termT_plus [in L.Datatypes.LNat]
termT_pred [in L.Datatypes.LNat]
termT_S [in L.Datatypes.LNat]
termT_nat_eqb [in L.Functions.Universal]
termT_S [in L.Functions.Universal]
termT_append [in L.Datatypes.Lists]
termT_cons [in L.Datatypes.Lists]
term_eva [in L.Functions.Universal]
term_substT [in L.Functions.Universal]
term_lam [in L.Functions.Universal]
term_app [in L.Functions.Universal]
term_var [in L.Functions.Universal]
term_eq_dec [in L.L]
term_ofNat [in L.Computability.Synthetic]
term_R_nat_nat [in L.Computability.Synthetic]
term_T_nat_nat [in L.Computability.Synthetic]
term_pair' [in L.Computability.Synthetic]
term_L_nat [in L.Computability.Synthetic]
term_test [in L.Computability.Synthetic]
term_poly_beq [in L.Reductions.H10]
term_T_list [in L.Reductions.H10]
term_cons' [in L.Reductions.H10]
term_test_eq [in L.Reductions.H10]
term_L_poly [in L.Reductions.H10]
term_poly_mul' [in L.Reductions.H10]
term_poly_add' [in L.Reductions.H10]
term_eval [in L.Reductions.H10]
term_poly_mul [in L.Reductions.H10]
term_poly_add [in L.Reductions.H10]
term_poly_var [in L.Reductions.H10]
term_poly_cnst [in L.Reductions.H10]
term_orb [in L.Datatypes.LBool]
term_andb [in L.Datatypes.LBool]
term_negb [in L.Datatypes.LBool]
term_list_prod [in L.Datatypes.Lists]
term_list_eqb [in L.Datatypes.Lists]
term_rev [in L.Datatypes.Lists]
term_elAt [in L.Datatypes.Lists]
term_nth_error [in L.Datatypes.Lists]
term_map_noTime [in L.Datatypes.Lists]
term_map [in L.Datatypes.Lists]
term_pos_nondec [in L.Datatypes.Lists]
term_inb_notime [in L.Datatypes.Lists]
term_inb [in L.Datatypes.Lists]
term_nth [in L.Datatypes.Lists]
term_filter_notime [in L.Datatypes.Lists]
term_filter [in L.Datatypes.Lists]
term_lam [in L.Datatypes.LTerm]
term_app [in L.Datatypes.LTerm]
term_var [in L.Datatypes.LTerm]
term_nat_eqb [in L.Tactics.ComputableDemo]
term_on0 [in L.Tactics.ComputableDemo]
term_term_eqb [in L.Functions.Equality]
term_test [in L.TM.TMEncoding]
term_loopM [in L.TM.TMEncoding]
term_haltConf [in L.TM.TMEncoding]
term_halt [in L.TM.TMEncoding]
term_step' [in L.TM.TMEncoding]
term_doAct_multi [in L.TM.TMEncoding]
term_doAct [in L.TM.TMEncoding]
term_current_chars [in L.TM.TMEncoding]
term_current [in L.TM.TMEncoding]
term_trans [in L.TM.TMEncoding]
term_vector_eqb [in L.TM.TMEncoding]
term_loop [in L.TM.TMEncoding]
term_ctapes [in L.TM.TMEncoding]
term_cstate [in L.TM.TMEncoding]
term_mconfigAsPair [in L.TM.TMEncoding]
term_tape_write [in L.TM.TMEncoding]
term_right [in L.TM.TMEncoding]
term_left [in L.TM.TMEncoding]
term_tape_move [in L.TM.TMEncoding]
term_tape_move_right [in L.TM.TMEncoding]
term_tape_move_right' [in L.TM.TMEncoding]
term_tape_move_left [in L.TM.TMEncoding]
term_tape_move_left' [in L.TM.TMEncoding]
term_midtape [in L.TM.TMEncoding]
term_rightof [in L.TM.TMEncoding]
term_leftof [in L.TM.TMEncoding]
term_map2 [in L.TM.TMEncoding]
term_vector_map [in L.TM.TMEncoding]
term_to_list [in L.TM.TMEncoding]
term_lookup [in L.TM.TMEncoding]
term_eqb [in L.TM.TMEncoding]
term_index [in L.TM.TMEncoding]
term_isSome [in L.Datatypes.LOptions]
term_option_eqb [in L.Datatypes.LOptions]
term_Some [in L.Datatypes.LOptions]
term_prod_eqb_notime [in L.Datatypes.LProd]
term_prod_eqb [in L.Datatypes.LProd]
term_snd [in L.Datatypes.LProd]
term_fst [in L.Datatypes.LProd]
term_pair [in L.Datatypes.LProd]
Section Index
D
demo [in L.Tactics.ComputableDemo]demo.PaperExample [in L.Tactics.ComputableDemo]
F
finType_eqb [in L.TM.TMEncoding]FixX [in L.Prelim.ARS]
Fix_Sigma [in L.TM.TM]
Fix_X [in L.Datatypes.Lists]
fix_sig.reg_tapes [in L.TM.TMEncoding]
fix_sig [in L.TM.TMEncoding]
Fix_X [in L.Datatypes.LOptions]
Fix_XY [in L.Datatypes.LProd]
funTable [in L.TM.TMEncoding]
I
int [in L.Datatypes.Lists]int [in L.Datatypes.LOptions]
it_i [in L.Tactics.Extract]
L
list_prod [in L.Datatypes.Lists]list_eqb [in L.Datatypes.Lists]
Lookup [in L.TM.TMEncoding]
Loop [in L.TM.Prelim]
LoopLift [in L.TM.Prelim]
loopM [in L.TM.TMEncoding]
LoopMerge [in L.TM.Prelim]
L_enum_rec [in L.Computability.Synthetic]
M
Map [in L.TM.Prelim]MapTape [in L.TM.TM]
MatchTapes [in L.TM.TM]
MirrorTape [in L.TM.TM]
MuRecursor [in L.Computability.MuRec]
N
Nop_Action [in L.TM.TM]O
option_eqb [in L.Datatypes.LOptions]S
Semantics [in L.TM.TM]T
Tape_Local [in L.TM.TM]Abbreviation Index
E
enumerates [in L.Computability.Synthetic]F
FUEL [in L.Tactics.Extract]Definition Index
A
ackermann [in L.Functions.Ackermann]argument_types [in L.Tactics.Extract]
B
benchTerm [in L.Tactics.Reflection]bool_enc_inv [in L.Computability.Computability]
both_cons [in L.Reductions.MPCP_PCP]
C
callTime2 [in L.Tactics.ComputableTime]card1 [in L.Reductions.SRH_SR]
card2 [in L.Reductions.SRH_SR]
cChoice [in L.Computability.Computability]
changeResType [in L.Tactics.Computable]
changeResType_TimeComplexity [in L.Tactics.ComputableTime]
church_rosser [in L.Prelim.ARS]
closed [in L.L]
cnst [in L.Tactics.ComputableTime]
comeUp_timebound_withInternalTactics [in L.Tactics.ComputableDemo]
CompAppCount [in L.Tactics.LClos_Eval]
CompBeta [in L.Tactics.LClos_Eval]
CompSeval [in L.Tactics.LClos_Eval]
computes [in L.Tactics.Computable]
computesExp [in L.Tactics.Computable]
computesTime [in L.Tactics.ComputableTime]
computesTimeExp [in L.Tactics.ComputableTime]
computesTimeIf [in L.Tactics.ComputableTime]
Comp_ind_deep [in L.Tactics.LClos]
Comp_ind_deep' [in L.Tactics.LClos]
confluent [in L.Prelim.ARS]
cons' [in L.Reductions.H10]
conv [in L.Reductions.H10]
converges [in L.L]
convert [in L.L]
correctness_example [in L.Tactics.ComputableDemo]
correct_recursive [in L.Tactics.ComputableDemo]
current [in L.TM.TM]
current_chars [in L.TM.TM]
D
deClos [in L.Tactics.LClos]denoteComp [in L.Tactics.Reflection]
denoteTerm [in L.Tactics.Reflection]
dependentArgs [in L.Tactics.Extract]
diamond [in L.Prelim.ARS]
doAct [in L.TM.TM]
doAct_multi [in L.TM.TM]
E
encode_arguments [in L.Tactics.GenEncode]encode_arguments [in L.Tactics.Extract]
eq_inductive [in L.Tactics.Extract]
error [in L.Tactics.Extract]
eva [in L.Computability.Seval]
eval [in L.L]
eval [in L.Reductions.H10]
evalIn [in L.L]
evalLe [in L.L]
evalTime [in L.Tactics.ComputableTime]
extEq [in L.Tactics.Computable]
extract [in L.Tactics.Extract]
extract_constr [in L.Tactics.Extract]
F
FinR [in L.TM.Prelim]finType_eqb [in L.TM.TMEncoding]
fn [in L.Reductions.PCP_CFG]
fn1 [in L.Reductions.PCP_CFG]
fn2 [in L.Reductions.PCP_CFG]
freeVars [in L.Tactics.Extract]
functional [in L.Prelim.ARS]
funTable [in L.TM.TMEncoding]
G
gen_constructor [in L.Tactics.Extract]H
Halt [in L.TM.TMEncoding]haltConf [in L.TM.TM]
haltTime [in L.TM.TMEncoding]
Halt' [in L.TM.TMEncoding]
hash_l_r [in L.Reductions.MPCP_PCP]
hd [in L.Tactics.Extract]
head_of_const [in L.Tactics.Extract]
I
I [in L.L]inb [in L.Datatypes.Lists]
insertCast [in L.Tactics.Computable]
insert_params [in L.Tactics.Extract]
isSome [in L.Datatypes.LOptions]
it_i [in L.Tactics.Extract]
it_i' [in L.Tactics.Extract]
J
joinable [in L.Prelim.ARS]K
K [in L.L]L
lambda [in L.L]left [in L.TM.TM]
lenumerates [in L.Computability.Synthetic]
liftPhi [in L.Tactics.Reflection]
list_constructors [in L.Tactics.Extract]
list_eqbTime_leq [in L.Datatypes.Lists]
list_eqbTime [in L.Datatypes.Lists]
list_eqb [in L.Datatypes.Lists]
lookup [in L.TM.TMEncoding]
lookupTime [in L.TM.TMEncoding]
loop [in L.TM.Prelim]
loopM [in L.TM.TM]
loopTime [in L.TM.TMEncoding]
L_enum [in L.Computability.Synthetic]
L_nat [in L.Computability.Synthetic]
L_recognisable [in L.Computability.Synthetic]
L_enumerable [in L.Computability.Synthetic]
L_decidable [in L.Computability.Synthetic]
L_from [in L.Reductions.H10]
L_poly [in L.Reductions.H10]
M
mapTape [in L.TM.TM]mapTapes [in L.TM.TM]
map_snd [in L.TM.Prelim]
map_fst [in L.TM.Prelim]
map_inr [in L.TM.Prelim]
map_inl [in L.TM.Prelim]
map_opt [in L.TM.Prelim]
matchlem [in L.Tactics.GenEncode]
maxP [in L.Prelim.MoreBase]
mconfigAsPair [in L.TM.TMEncoding]
mirror_move [in L.TM.TM]
mirror_tapes [in L.TM.TM]
mirror_tape [in L.TM.TM]
mkApp [in L.Tactics.Extract]
mkAppList [in L.Tactics.Extract]
mkFixMatch [in L.Tactics.Extract]
mkLam [in L.Tactics.Extract]
mkLApp [in L.Tactics.GenEncode]
mkMatch [in L.Tactics.GenEncode]
mkNat [in L.Tactics.Extract]
mkVar [in L.Tactics.Extract]
mu [in L.Computability.MuRec]
mu' [in L.Computability.MuRec]
N
name_of [in L.Tactics.Extract]name_after_dot [in L.Prelim.StringBase]
name_after_dot' [in L.Prelim.StringBase]
natsLess [in L.Prelim.MoreList]
nop_action [in L.TM.TM]
notHigherOrder [in L.Tactics.ComputableTime]
O
Omega [in L.L]omega [in L.L]
on0 [in L.Tactics.ComputableDemo]
option_eqb [in L.Datatypes.LOptions]
P
pair' [in L.Computability.Synthetic]plus' [in L.TM.Prelim]
poly_eqb [in L.Reductions.H10]
poly_mul' [in L.Reductions.H10]
poly_add' [in L.Reductions.H10]
pos_nondec [in L.Datatypes.Lists]
pow [in L.Prelim.ARS]
proc [in L.L]
Proc [in L.Tactics.Reflection]
prod_eqb [in L.Datatypes.LProd]
pTM [in L.TM.TM]
P' [in L.Reductions.MPCP_PCP]
R
R [in L.L]r [in L.L]
rClosed [in L.Tactics.Reflection]
rClosed_decb [in L.Tactics.Reflection]
rClosed_decb' [in L.Tactics.Reflection]
rcomp [in L.Prelim.ARS]
rCompAppCount [in L.Tactics.Reflection]
rCompBeta [in L.Tactics.Reflection]
rCompSeval [in L.Tactics.Reflection]
rCompSeval' [in L.Tactics.Reflection]
rComp_ind_deep [in L.Tactics.Reflection]
rComp_ind_deep' [in L.Tactics.Reflection]
rDeClos [in L.Tactics.Reflection]
red [in L.Reductions.MPCP_PCP]
red [in L.Reductions.SR_MPCP]
red [in L.Reductions.SRH_SR]
redLe [in L.L]
reflexive [in L.Prelim.ARS]
registered_finType [in L.TM.TMEncoding]
resType [in L.Tactics.Computable]
rev_string [in L.Prelim.StringBase]
rho [in L.L]
right [in L.TM.TM]
rPow [in L.Tactics.Reflection]
rSubstList [in L.Tactics.Reflection]
rValidComp [in L.Tactics.Reflection]
S
semi_confluent [in L.Prelim.ARS]singcard [in L.Reductions.SR_MPCP]
size [in L.L]
sizeOfmTapes [in L.TM.TM]
sizeOfTape [in L.TM.TM]
size' [in L.L]
split_head_symbol [in L.Tactics.Extract]
stack [in L.Tactics.Extract]
step [in L.TM.TM]
step' [in L.TM.TMEncoding]
string_of_int [in L.Tactics.Extract]
subst [in L.L]
substList [in L.Tactics.LClos]
sumn [in L.Prelim.MoreList]
symmetric [in L.Prelim.ARS]
T
tapes [in L.TM.TM]tapeToList [in L.TM.TM]
tape_local_l [in L.TM.TM]
tape_local [in L.TM.TM]
tape_write [in L.TM.TM]
tape_move [in L.TM.TM]
tape_move_left [in L.TM.TM]
tape_move_left' [in L.TM.TM]
tape_move_right [in L.TM.TM]
tape_move_right' [in L.TM.TM]
term_eq_dec_proc [in L.L]
term_eqb [in L.Functions.Equality]
test [in L.Computability.Synthetic]
test_eq [in L.Reductions.H10]
TH [in L.L]
timeComplexity [in L.Tactics.ComputableTime]
time_map2 [in L.TM.TMEncoding]
tmArgsOfConstructor [in L.Tactics.Extract]
tmDependentArgs [in L.Tactics.Extract]
tmEncode [in L.Tactics.Extract]
tmExtract [in L.Tactics.Extract]
tmExtractConstr [in L.Tactics.Extract]
tmExtractConstr' [in L.Tactics.Extract]
tmGenEncode [in L.Tactics.GenEncode]
tmGetOption [in L.Tactics.Extract]
tmIsType [in L.Tactics.Extract]
tmMatchCorrect [in L.Tactics.GenEncode]
tmNumConstructors [in L.Tactics.Extract]
tmTryInfer [in L.Tactics.Extract]
tmTypeOf [in L.Tactics.Extract]
tmUnfoldTerm [in L.Tactics.Extract]
to_list [in L.Prelim.StringBase]
to_string [in L.Prelim.StringBase]
transitive [in L.Prelim.ARS]
transTime [in L.TM.TMEncoding]
T_nat_nat [in L.Computability.Synthetic]
T_list_nat [in L.Reductions.H10]
U
uniform_confluent [in L.Prelim.ARS]unit_enc [in L.Tactics.ComputableDemo]
V
validEnv [in L.Tactics.LClos]validEnv' [in L.Tactics.LClos]
Record Index
C
computable [in L.Tactics.Computable]computableTime [in L.Tactics.ComputableTime]
E
encodable [in L.Tactics.Extract]extracted [in L.Tactics.Extract]
M
mconfig [in L.TM.TM]mTM [in L.TM.TM]
R
registered [in L.Tactics.Computable]| 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 | (988 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 | (21 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 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 | (43 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 | (304 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 | (65 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 | (15 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 | (22 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 | (177 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 | (31 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 | (2 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 | (226 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 | (7 entries) |