| 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 | (751 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 | (62 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 | (17 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 | (27 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (324 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 | (108 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 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 | (43 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 | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (163 entries) |
Global Index
A
Add [constructor, in CoqDSC.Constants]app_comm_cons_2 [lemma, in CoqDSC.Misc]
assoc_bind [lemma, in CoqDSC.ErrorMonad]
at_least_one_step_deval [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
at_least_one_step [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
B
base_extended_with_cache [inductive, in CoqDSC.ILambdaALExtensionWithCaches]BExtendNil [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
BExtendWithOldDef [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
BExtendWithTuple [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
bind [definition, in CoqDSC.Environment]
binding [definition, in CoqDSC.ILambdaALCTSProofs]
bind_ret [lemma, in CoqDSC.ErrorMonad]
bind_postbind [lemma, in CoqDSC.Environment]
bind_postbind_nil [lemma, in CoqDSC.Environment]
boxer [constructor, in CoqDSC.LibTactics]
Boxer [inductive, in CoqDSC.LibTactics]
C
cache [definition, in CoqDSC.ILambdaAL]Cache [constructor, in CoqDSC.ILambdaAL]
CacheValue [constructor, in CoqDSC.ILambdaALValues]
cache_update [definition, in CoqDSC.ILambdaAL]
cache_var [inductive, in CoqDSC.ILambdaAL]
cache_of_call [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
cache_strenghening [lemma, in CoqDSC.ILambdaALCTSProofs]
cache_of_term_reverse_environment [lemma, in CoqDSC.ILambdaALCTSProofs]
cache_update_of_term [definition, in CoqDSC.ILambdaALDerive]
cache_of_term [definition, in CoqDSC.ILambdaALDerive]
cache_value [inductive, in CoqDSC.ILambdaALValues]
call [definition, in CoqDSC.ILambdaAL]
call [definition, in CoqDSC.LambdaAL]
call_evaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
call_inversion [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
call_result_in_cache [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
call_evaluation [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
CDCons [constructor, in CoqDSC.LambdaALValues]
CDNil [constructor, in CoqDSC.LambdaALValues]
closure [definition, in CoqDSC.LambdaALValues]
Closure [constructor, in CoqDSC.LambdaALValues]
closure_call_inversion [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
closure_denvironment_of_list_list_of_closure_denvironment [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
closure_environment_of_list [definition, in CoqDSC.ILambdaALOperationalSemantics]
closure_denvironment_of_list [definition, in CoqDSC.LambdaALValues]
closure_denvironment [inductive, in CoqDSC.LambdaALValues]
COIND [definition, in CoqDSC.LibTactics]
commute_bind [lemma, in CoqDSC.ErrorMonad]
compile_binding [definition, in CoqDSC.ILambdaALCTSProofs]
complete_eval [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
congruence_hypothesis [definition, in CoqDSC.LambdaALFundamentalProperty]
ConsHasNoCache [constructor, in CoqDSC.ILambdaALOperationalSemanticsProofs]
Constants [library]
context [definition, in CoqDSC.LambdaAL]
context [definition, in CoqDSC.ILambdaALOperationalSemantics]
correct_dprimitive_curry [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_fixrec [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_push [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_add [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_recompute_primitive [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive [definition, in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_fixrec [lemma, in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_push [lemma, in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_curry [lemma, in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_add [lemma, in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive [definition, in CoqDSC.ILambdaALCTSProofs]
correct_recompute [lemma, in CoqDSC.ILambdaALCTSProofs]
Crush [library]
cts_derive_soundness [lemma, in CoqDSC.ILambdaALDeriveProofs]
cts_derive_cts_dvalue [lemma, in CoqDSC.ILambdaALDeriveProofs]
cts_derive_cts_dvalue_gen [lemma, in CoqDSC.ILambdaALDeriveProofs]
cts_denvironment_inherits_valid_modified_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
cts_closure_denvironment_cts_denvironment [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_environment_has_no_cache [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_denvironment [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_modified_environment2 [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_modified_environment [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_value_injective [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_original_environment [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_environment_preserves_length [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_preserves_length [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_nonvar_has_nonempty_cache [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_dvalues_cts_dbinding_2 [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_binding [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_dbinding [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_lookups [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_lookup [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_app [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_environment_app [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_environment_lookups [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_environment_lookup [lemma, in CoqDSC.ILambdaALCTSProofs]
cts_denvironment [definition, in CoqDSC.ILambdaALDerive]
cts_dbinding [definition, in CoqDSC.ILambdaALDerive]
cts_environment [definition, in CoqDSC.ILambdaALDerive]
cts_binding [definition, in CoqDSC.ILambdaALDerive]
cts_dvalues [definition, in CoqDSC.ILambdaALDerive]
cts_closure_denvironment [definition, in CoqDSC.ILambdaALDerive]
cts_dvalue [definition, in CoqDSC.ILambdaALDerive]
cts_dterm [definition, in CoqDSC.ILambdaALDerive]
cts_values [definition, in CoqDSC.ILambdaALDerive]
cts_value [definition, in CoqDSC.ILambdaALDerive]
cts_derive [definition, in CoqDSC.ILambdaALDerive]
cts_derive_term [definition, in CoqDSC.ILambdaALDerive]
cts_term [definition, in CoqDSC.ILambdaALDerive]
cts_term_aux [definition, in CoqDSC.ILambdaALDerive]
Curry [constructor, in CoqDSC.Constants]
curry_adequacy [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
D
d [constructor, in CoqDSC.LambdaAL]dcall [definition, in CoqDSC.ILambdaAL]
dcall [definition, in CoqDSC.LambdaAL]
dcall_inversion [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
dcall_evaluation [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
dclosure [definition, in CoqDSC.LambdaALValues]
dClosure [constructor, in CoqDSC.LambdaALValues]
dClosureValid [constructor, in CoqDSC.LambdaALValidity]
dclosure_only_applies_to_closure [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
dcontext [definition, in CoqDSC.LambdaAL]
dDef [constructor, in CoqDSC.LambdaAL]
dDefTuple [constructor, in CoqDSC.LambdaAL]
decompose_devaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
decompose_evaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
Def [constructor, in CoqDSC.LambdaAL]
DefTuple [constructor, in CoqDSC.LambdaAL]
demo_clears_all_and_clears_but [lemma, in CoqDSC.LibTactics]
denvironment [definition, in CoqDSC.LambdaALOperationalSemantics]
denvironment [definition, in CoqDSC.ILambdaALOperationalSemantics]
denvironment_of_closure_denvironment [definition, in CoqDSC.LambdaALOperationalSemantics]
denvironment_of_dclosure_denvironment [definition, in CoqDSC.ILambdaALOperationalSemantics]
denvironment_equivalent_modulo_caches_original_evaluation [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_eval_cache [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_values_original [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_original_2 [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_original [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_value_original [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_extend [definition, in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches [definition, in CoqDSC.ILambdaALExtensionWithCaches]
depth_of_binding [lemma, in CoqDSC.ILambdaALCTSProofs]
depth_of_term_graft [lemma, in CoqDSC.ILambdaALCTSProofs]
depth_of_term [definition, in CoqDSC.ILambdaALDerive]
derive [definition, in CoqDSC.LambdaALDerive]
derive_context_ended_with_call [lemma, in CoqDSC.LambdaALDeriveProofs]
derive_context_ended_with_tuple [lemma, in CoqDSC.LambdaALDeriveProofs]
derive_graft_tuple [lemma, in CoqDSC.LambdaALDeriveProofs]
derive_soundness2 [lemma, in CoqDSC.LambdaALDeriveProofs]
derive_soundness [lemma, in CoqDSC.LambdaALDeriveProofs]
derive_binding [definition, in CoqDSC.ILambdaALCTSProofs]
derive_underive [lemma, in CoqDSC.LambdaALDerive]
deterministic_deval [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
deterministic_eval [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
deval [definition, in CoqDSC.LambdaALOperationalSemantics]
deval [inductive, in CoqDSC.ILambdaALOperationalSemantics]
dgraft [definition, in CoqDSC.LambdaAL]
dIClosure [constructor, in CoqDSC.ILambdaALValues]
dIDef [constructor, in CoqDSC.ILambdaAL]
dIDefTuple [constructor, in CoqDSC.ILambdaAL]
dILiteral [constructor, in CoqDSC.ILambdaALValues]
dIPrimitiveNil [constructor, in CoqDSC.ILambdaALValues]
dIReplace [constructor, in CoqDSC.ILambdaALValues]
dIResult [constructor, in CoqDSC.ILambdaAL]
dITuple [constructor, in CoqDSC.ILambdaALValues]
dLiteral [constructor, in CoqDSC.LambdaALValues]
dliteral [inductive, in CoqDSC.Constants]
dliteral [definition, in CoqDSC.ILambdaALValues]
dLitValid [constructor, in CoqDSC.LambdaALValidity]
dNilpdenv [definition, in CoqDSC.LambdaALDerive]
dNilpldvalues [definition, in CoqDSC.LambdaALDerive]
dNil' [definition, in CoqDSC.LambdaALDerive]
done [definition, in CoqDSC.Crush]
dPos [constructor, in CoqDSC.Constants]
dPrimitiveNil [constructor, in CoqDSC.LambdaALValues]
dPrimitiveNilValid [constructor, in CoqDSC.LambdaALValidity]
DrelCons [constructor, in CoqDSC.LambdaALValidity]
DrelNil [constructor, in CoqDSC.LambdaALValidity]
drels [definition, in CoqDSC.LambdaALValidity]
drels_F [definition, in CoqDSC.LambdaALValidity]
drels_type [definition, in CoqDSC.LambdaALValidity]
drel_env_bind_rel_value [lemma, in CoqDSC.LambdaALFundamentalProperty]
drel_value_inversion [lemma, in CoqDSC.LambdaALValidity]
drel_env_dlookups [lemma, in CoqDSC.LambdaALValidity]
drel_value_move_value [lemma, in CoqDSC.LambdaALValidity]
drel_env_lookup2 [lemma, in CoqDSC.LambdaALValidity]
drel_env_lookup [lemma, in CoqDSC.LambdaALValidity]
drel_env_antimonotonic [lemma, in CoqDSC.LambdaALValidity]
drel_value_antimonotonic [lemma, in CoqDSC.LambdaALValidity]
drel_value_replace [lemma, in CoqDSC.LambdaALValidity]
drel_value_literal_inversion [lemma, in CoqDSC.LambdaALValidity]
drel_value_inductive [inductive, in CoqDSC.LambdaALValidity]
drel_env [definition, in CoqDSC.LambdaALValidity]
drel_term [definition, in CoqDSC.LambdaALValidity]
drel_value [definition, in CoqDSC.LambdaALValidity]
drel_term_F [definition, in CoqDSC.LambdaALValidity]
drel_value_F [definition, in CoqDSC.LambdaALValidity]
dReplace [constructor, in CoqDSC.LambdaALValues]
dReplaceValid [constructor, in CoqDSC.LambdaALValidity]
drop [definition, in CoqDSC.Misc]
drop_cons [lemma, in CoqDSC.Misc]
drop_decompose [lemma, in CoqDSC.Misc]
drop_inversion [lemma, in CoqDSC.Misc]
drop_nil [lemma, in CoqDSC.Misc]
drop_app [lemma, in CoqDSC.Misc]
dterm [inductive, in CoqDSC.ILambdaAL]
dterm [inductive, in CoqDSC.LambdaAL]
dttuple [definition, in CoqDSC.LambdaAL]
dtuple [definition, in CoqDSC.ILambdaAL]
dtuple [definition, in CoqDSC.LambdaALValues]
dTuple [constructor, in CoqDSC.LambdaALValues]
dTupleValid [constructor, in CoqDSC.LambdaALValidity]
dup_lemma [lemma, in CoqDSC.LibTactics]
dvalue [inductive, in CoqDSC.LambdaALValues]
dvalue [inductive, in CoqDSC.ILambdaALValues]
dvar [definition, in CoqDSC.ILambdaAL]
dVar [constructor, in CoqDSC.LambdaAL]
dvar [inductive, in CoqDSC.LambdaAL]
DVCons [constructor, in CoqDSC.LambdaALValues]
DVNil [constructor, in CoqDSC.LambdaALValues]
d_und [lemma, in CoqDSC.LambdaAL]
E
environment [definition, in CoqDSC.LambdaALOperationalSemantics]environment [definition, in CoqDSC.ILambdaALOperationalSemantics]
Environment [library]
equatesLemma [section, in CoqDSC.LibTactics]
equatesLemma.A0 [variable, in CoqDSC.LibTactics]
equatesLemma.A1 [variable, in CoqDSC.LibTactics]
equatesLemma.A2 [variable, in CoqDSC.LibTactics]
equatesLemma.A3 [variable, in CoqDSC.LibTactics]
equatesLemma.A4 [variable, in CoqDSC.LibTactics]
equatesLemma.A5 [variable, in CoqDSC.LibTactics]
equatesLemma.A6 [variable, in CoqDSC.LibTactics]
equates_6 [lemma, in CoqDSC.LibTactics]
equates_5 [lemma, in CoqDSC.LibTactics]
equates_4 [lemma, in CoqDSC.LibTactics]
equates_3 [lemma, in CoqDSC.LibTactics]
equates_2 [lemma, in CoqDSC.LibTactics]
equates_1 [lemma, in CoqDSC.LibTactics]
equates_0 [lemma, in CoqDSC.LibTactics]
eq_dec_nat_refl [lemma, in CoqDSC.Misc]
eq' [definition, in CoqDSC.LibTactics]
erase_steps_evaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
error [definition, in CoqDSC.ErrorMonad]
ErrorMonad [library]
eval [definition, in CoqDSC.LambdaALOperationalSemantics]
eval [inductive, in CoqDSC.ILambdaALOperationalSemantics]
eval_primitive [definition, in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_fixrec [definition, in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_push [definition, in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_curry [definition, in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_add [definition, in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_dprimitive [definition, in CoqDSC.LambdaALOperationalSemantics]
eval_dfixrec [definition, in CoqDSC.LambdaALOperationalSemantics]
eval_dcurry [definition, in CoqDSC.LambdaALOperationalSemantics]
eval_dpush [definition, in CoqDSC.LambdaALOperationalSemantics]
eval_dadd [definition, in CoqDSC.LambdaALOperationalSemantics]
eval_dcontext [inductive, in CoqDSC.LambdaALOperationalSemanticsProofs]
eval_context [inductive, in CoqDSC.LambdaALOperationalSemanticsProofs]
eval_cache_update [inductive, in CoqDSC.ILambdaALOperationalSemantics]
eval_dprimitive [definition, in CoqDSC.ILambdaALOperationalSemantics]
eval_dfixrec [definition, in CoqDSC.ILambdaALOperationalSemantics]
eval_dcurry [definition, in CoqDSC.ILambdaALOperationalSemantics]
eval_dpush [definition, in CoqDSC.ILambdaALOperationalSemantics]
eval_dadd [definition, in CoqDSC.ILambdaALOperationalSemantics]
eval_context [inductive, in CoqDSC.ILambdaALOperationalSemantics]
eval_cache [inductive, in CoqDSC.ILambdaALOperationalSemantics]
eval_cache_app_context [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_call_under_modified_extended_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_call_under_old_extended_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_under_extended_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_extended_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_new_extended [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_old_extended [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
eval_primitive [definition, in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_fixrec [definition, in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_curry [definition, in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_push [definition, in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_add [definition, in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_deterministic [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_under_modified_environment_of_eval_cache_update [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_update_of_eval_cache_under_modified_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_deterministic [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_weakening [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_preserves_length [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_primitive_add_cache [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_of_cts_term [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat_gen_nosteps [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat_gen [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_dprimitive_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_primitive_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_fixrec_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_curry_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_push_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_add_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_cache_strenghening [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_context_ended_with_call [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_context_ended_with_tuple [lemma, in CoqDSC.ILambdaALCTSProofs]
eval_context_length [lemma, in CoqDSC.ILambdaALCTSProofs]
extended_with_old_caches_lookup [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_caches_lookups [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_new_caches_lookup_modified_env [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_caches_lookup [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extended_environment [definition, in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_cache [inductive, in CoqDSC.ILambdaALExtensionWithCaches]
ExtendNil [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
ExtendWithNewDef [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
ExtendWithOldDef [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
ExtendWithTuple [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
extend_new_environment_with_call [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extend_old_environment_with_call [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension [inductive, in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup_cts_denvironment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup2 [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension_length_is_depth_of_context [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension_preserves_length [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extension_components [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
extract_original_and_modified_evaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
F
FixRec [constructor, in CoqDSC.Constants]focus_lookup [lemma, in CoqDSC.Environment]
FuncEq [section, in CoqDSC.LibTactics]
FuncEq.A1 [variable, in CoqDSC.LibTactics]
FuncEq.A2 [variable, in CoqDSC.LibTactics]
FuncEq.A3 [variable, in CoqDSC.LibTactics]
FuncEq.A4 [variable, in CoqDSC.LibTactics]
FuncEq.A5 [variable, in CoqDSC.LibTactics]
FuncEq.B [variable, in CoqDSC.LibTactics]
FUNCTOR [section, in CoqDSC.LambdaALValidity]
FUNCTOR.n [variable, in CoqDSC.LambdaALValidity]
FUNCTOR.rec_term [variable, in CoqDSC.LambdaALValidity]
FUNCTOR.rec_value [variable, in CoqDSC.LambdaALValidity]
func_eq_5 [lemma, in CoqDSC.LibTactics]
func_eq_4 [lemma, in CoqDSC.LibTactics]
func_eq_3 [lemma, in CoqDSC.LibTactics]
func_eq_2 [lemma, in CoqDSC.LibTactics]
func_eq_1 [lemma, in CoqDSC.LibTactics]
fundamental_lemma [lemma, in CoqDSC.LambdaALFundamentalProperty]
fun_extensionality [axiom, in CoqDSC.LambdaALValidity]
G
gdeval [inductive, in CoqDSC.LambdaALOperationalSemantics]geval [inductive, in CoqDSC.LambdaALOperationalSemantics]
graft [definition, in CoqDSC.LambdaAL]
graft_binding_depth [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
graft_var_depth [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
graft_hole [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
graft_assoc [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
graft_tuple [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
graft_def [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
H
has_no_cache [inductive, in CoqDSC.ILambdaALOperationalSemanticsProofs]I
IClosure [constructor, in CoqDSC.ILambdaALValues]IDef [constructor, in CoqDSC.ILambdaAL]
IDefTuple [constructor, in CoqDSC.ILambdaAL]
Idx [constructor, in CoqDSC.Index]
iff_intro_swap [lemma, in CoqDSC.LibTactics]
ILambdaAL [library]
ILambdaALCTSProofs [library]
ILambdaALDerive [library]
ILambdaALDeriveProofs [library]
ILambdaALExtensionWithCaches [library]
ILambdaALOperationalSemantics [library]
ILambdaALOperationalSemanticsPrimitives [library]
ILambdaALOperationalSemanticsProofs [library]
ILambdaALValues [library]
ILiteral [constructor, in CoqDSC.ILambdaALValues]
index [definition, in CoqDSC.LambdaALOperationalSemantics]
Index [library]
indexType [inductive, in CoqDSC.LambdaALOperationalSemantics]
induct_height_max2 [lemma, in CoqDSC.LibTactics]
injective_closure_denvironment_of_list [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_underive [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_und [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_und [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_d [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_d [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_injf [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_values_of_list [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
inj_pair2 [axiom, in CoqDSC.LibTactics]
invalid_lookup [lemma, in CoqDSC.Environment]
inverse_move_closure [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
inverse_modified_environment_bind [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
inverse_primitive_call_evaluation [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
inverse_closure_call_evaluation [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
inverse_call_evaluation [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
invert_rel_env [lemma, in CoqDSC.LambdaALEnvValidity]
invert_move_values_cons [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
invert_move_values_nil [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
invert_rel_env_append [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
invert_rel_env_len [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
inv_error_mbind2 [lemma, in CoqDSC.ErrorMonad]
inv_error_mbind [lemma, in CoqDSC.ErrorMonad]
inv_success_mbind2 [lemma, in CoqDSC.ErrorMonad]
inv_success_mbind [lemma, in CoqDSC.ErrorMonad]
IPrimitive [constructor, in CoqDSC.ILambdaALValues]
IResult [constructor, in CoqDSC.ILambdaAL]
ITuple [constructor, in CoqDSC.ILambdaALValues]
IVCons [constructor, in CoqDSC.ILambdaALValues]
IVNil [constructor, in CoqDSC.ILambdaALValues]
L
LambdaAL [library]LambdaALDerive [library]
LambdaALDeriveProofs [library]
LambdaALEnvValidity [library]
LambdaALFundamentalProperty [library]
LambdaALOperationalSemantics [library]
LambdaALOperationalSemanticsPrimitives [library]
LambdaALOperationalSemanticsProofs [library]
LambdaALValidity [library]
LambdaALValues [library]
ldvalues [inductive, in CoqDSC.LambdaALValues]
ldvalues_of_list [definition, in CoqDSC.LambdaALValues]
length_of_eval_context [lemma, in CoqDSC.ILambdaALCTSProofs]
length_tl [lemma, in CoqDSC.Misc]
let_binding_unfold [lemma, in CoqDSC.LibTactics]
let_binding [definition, in CoqDSC.LibTactics]
LibTactics [library]
LibTacticsCompatibility [module, in CoqDSC.LibTactics]
lift [definition, in CoqDSC.Index]
lift_lookup [lemma, in CoqDSC.Environment]
list_of_closure_denvironment_closure_denvironment_of_list [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
list_of_ldvalues_of_ldvalues_of_list [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
list_of_values_of_values_of_list [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
list_of_closure_denvironment [definition, in CoqDSC.ILambdaALOperationalSemantics]
list_of_closure_environment [definition, in CoqDSC.ILambdaALOperationalSemantics]
list_of_closure_denvironment [definition, in CoqDSC.LambdaALValues]
list_of_ldvalues [definition, in CoqDSC.LambdaALValues]
list_of_values [definition, in CoqDSC.LambdaALValues]
list_map_post_cons [lemma, in CoqDSC.ErrorMonad]
list_map_cons [lemma, in CoqDSC.ErrorMonad]
list_map_app [lemma, in CoqDSC.ErrorMonad]
list_map_length [lemma, in CoqDSC.ErrorMonad]
list_map2 [definition, in CoqDSC.ErrorMonad]
list_map [definition, in CoqDSC.ErrorMonad]
list_of_closure_environment_of_closure_environment_of_list [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
list_of_closure_environment_cts_environment [lemma, in CoqDSC.ILambdaALCTSProofs]
list_map_lookup_2 [lemma, in CoqDSC.Environment]
list_map_lookup [lemma, in CoqDSC.Environment]
list_of_values [definition, in CoqDSC.ILambdaALValues]
Literal [constructor, in CoqDSC.LambdaALValues]
literal [inductive, in CoqDSC.Constants]
literal [definition, in CoqDSC.ILambdaALValues]
lookup [definition, in CoqDSC.Environment]
lookups [definition, in CoqDSC.Environment]
lookups_nil [lemma, in CoqDSC.LambdaALValidity]
lookups_modified_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookups_original_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookups_length [lemma, in CoqDSC.Environment]
lookup_move_environment [lemma, in CoqDSC.LambdaALEnvValidity]
lookup_env_of_denv [lemma, in CoqDSC.LambdaALEnvValidity]
lookup_cache [definition, in CoqDSC.ILambdaALOperationalSemantics]
lookup_values [definition, in CoqDSC.ILambdaALOperationalSemantics]
lookup_value [definition, in CoqDSC.ILambdaALOperationalSemantics]
lookup_original_of_extended_environment [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
lookup_value_tail [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
lookup_in_modified_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_modified_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_modified_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_original_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_original_environment [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_unfold [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_value_lookup_2 [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_value_lookup [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_is_cache_independent [lemma, in CoqDSC.ILambdaALCTSProofs]
lookup_value_is_cache_independent [lemma, in CoqDSC.ILambdaALCTSProofs]
lookup_app_2 [lemma, in CoqDSC.Environment]
lookup_app [lemma, in CoqDSC.Environment]
ltac_goal_to_discard_intro [constructor, in CoqDSC.LibTactics]
ltac_goal_to_discard [inductive, in CoqDSC.LibTactics]
ltac_something_show [lemma, in CoqDSC.LibTactics]
ltac_something_hide [lemma, in CoqDSC.LibTactics]
ltac_something_eq [lemma, in CoqDSC.LibTactics]
ltac_something [definition, in CoqDSC.LibTactics]
ltac_to_generalize [definition, in CoqDSC.LibTactics]
ltac_tag_subst [definition, in CoqDSC.LibTactics]
ltac_nat_from_int [definition, in CoqDSC.LibTactics]
ltac_database_provide [lemma, in CoqDSC.LibTactics]
ltac_database [definition, in CoqDSC.LibTactics]
ltac_database_token [constructor, in CoqDSC.LibTactics]
Ltac_database_token [inductive, in CoqDSC.LibTactics]
ltac_mark [constructor, in CoqDSC.LibTactics]
ltac_Mark [inductive, in CoqDSC.LibTactics]
ltac_wilds [constructor, in CoqDSC.LibTactics]
ltac_Wilds [inductive, in CoqDSC.LibTactics]
ltac_wild [constructor, in CoqDSC.LibTactics]
ltac_Wild [inductive, in CoqDSC.LibTactics]
ltac_no_arg [constructor, in CoqDSC.LibTactics]
ltac_No_arg [inductive, in CoqDSC.LibTactics]
lt_lt [lemma, in CoqDSC.Misc]
lt_comp [lemma, in CoqDSC.Misc]
M
map_und_d_id [lemma, in CoqDSC.LambdaAL]map_modified_binding_is_move_values [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
map_lookups [lemma, in CoqDSC.Environment]
map_lookup_2 [lemma, in CoqDSC.Environment]
map_lookup [lemma, in CoqDSC.Environment]
map_equiv_length [lemma, in CoqDSC.Misc]
map_id [lemma, in CoqDSC.Misc]
map_equiv [lemma, in CoqDSC.Misc]
map_map [lemma, in CoqDSC.Misc]
mbind [definition, in CoqDSC.ErrorMonad]
minus_factorize [lemma, in CoqDSC.Misc]
minus_commute [lemma, in CoqDSC.Misc]
Misc [library]
modified_environment_under_rel_env [lemma, in CoqDSC.LambdaALEnvValidity]
modified_environment_of_rel_env [lemma, in CoqDSC.ILambdaALDeriveProofs]
modified_environment [definition, in CoqDSC.LambdaALOperationalSemantics]
modified_env_of_drel_env [lemma, in CoqDSC.LambdaALValidity]
modified_environment_of_closure_denvironment [lemma, in CoqDSC.LambdaALDeriveProofs]
modified_environment_lookups [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_lookup [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_app [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_bind [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment [definition, in CoqDSC.ILambdaALOperationalSemantics]
modified_binding [definition, in CoqDSC.ILambdaALOperationalSemantics]
modified_environment_bind [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
modified_environment_implied_valid_moves [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
move [definition, in CoqDSC.LambdaALOperationalSemantics]
move [definition, in CoqDSC.ILambdaALOperationalSemantics]
move_environment [definition, in CoqDSC.LambdaALOperationalSemantics]
move_values [definition, in CoqDSC.LambdaALOperationalSemantics]
move_closure_environment [definition, in CoqDSC.LambdaALOperationalSemantics]
move_literal [definition, in CoqDSC.LambdaALOperationalSemantics]
move_original_closure_environment [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
move_with_eval_dprimitive [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
move_replace [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
move_tuple [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
move_closure_environment_move_environment [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
move_values [definition, in CoqDSC.ILambdaALOperationalSemantics]
move_closure_environment [definition, in CoqDSC.ILambdaALOperationalSemantics]
move_literal [definition, in CoqDSC.ILambdaALOperationalSemantics]
move_replace [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
move_nil [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
move_closure_environment_cts_denvironment [lemma, in CoqDSC.ILambdaALCTSProofs]
move_closure_environments [lemma, in CoqDSC.ILambdaALCTSProofs]
move_cts_values [lemma, in CoqDSC.ILambdaALCTSProofs]
move_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
N
Nat [constructor, in CoqDSC.Constants]neval [definition, in CoqDSC.LambdaALOperationalSemantics]
New [constructor, in CoqDSC.ILambdaALExtensionWithCaches]
NilHasNoCache [constructor, in CoqDSC.ILambdaALOperationalSemanticsProofs]
nil_literal [definition, in CoqDSC.LambdaALDerive]
NoSteps [constructor, in CoqDSC.LambdaALOperationalSemantics]
O
Old [constructor, in CoqDSC.ILambdaALExtensionWithCaches]original_environment_under_rel_env [lemma, in CoqDSC.LambdaALEnvValidity]
original_environment_of_rel_env [lemma, in CoqDSC.ILambdaALDeriveProofs]
original_environment [definition, in CoqDSC.LambdaALOperationalSemantics]
original_env_of_drel_env [lemma, in CoqDSC.LambdaALValidity]
original_environment_lookups [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_lookup [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_app [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_bind [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment [definition, in CoqDSC.ILambdaALOperationalSemantics]
original_cts_denvironment_has_no_cache [lemma, in CoqDSC.ILambdaALCTSProofs]
Overview [library]
P
postbind [definition, in CoqDSC.Environment]postbind_of_single [lemma, in CoqDSC.Environment]
post_extend_new_with_tuple [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
post_extend_old_with_tuple [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
pre_drel_env__lookup [lemma, in CoqDSC.LambdaALValidity]
pre_drel_env_alt [lemma, in CoqDSC.LambdaALValidity]
pre_drel_env [inductive, in CoqDSC.LambdaALValidity]
Primitive [constructor, in CoqDSC.LambdaALValues]
primitive [inductive, in CoqDSC.Constants]
primitive [definition, in CoqDSC.ILambdaALValues]
primitive_call_inversion [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
prop_extensionality [axiom, in CoqDSC.LambdaALValidity]
Push [constructor, in CoqDSC.Constants]
R
recompute_primitive [definition, in CoqDSC.LambdaALOperationalSemantics]recompute_primitive_eq [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
recompute_primitive [definition, in CoqDSC.ILambdaALOperationalSemantics]
recompute_primitive_eq [lemma, in CoqDSC.ILambdaALCTSProofs]
recurse_valid [lemma, in CoqDSC.LambdaALValidity]
related_tuples [lemma, in CoqDSC.LambdaALFundamentalProperty]
related_calls [lemma, in CoqDSC.LambdaALFundamentalProperty]
related_primitive_calls [lemma, in CoqDSC.LambdaALFundamentalProperty]
related_lookups [lemma, in CoqDSC.LambdaALValidity]
rel_env_lookup_change [lemma, in CoqDSC.LambdaALEnvValidity]
rel_env_length [lemma, in CoqDSC.LambdaALEnvValidity]
rel_env_through_context_evaluation [lemma, in CoqDSC.LambdaALEnvValidity]
rel_env_lookup_value [lemma, in CoqDSC.LambdaALEnvValidity]
rel_env_lookup_value' [lemma, in CoqDSC.LambdaALEnvValidity]
rel_env [definition, in CoqDSC.LambdaALEnvValidity]
rel_value [definition, in CoqDSC.LambdaALEnvValidity]
restrict_lookup_2 [lemma, in CoqDSC.Environment]
restrict_lookup [lemma, in CoqDSC.Environment]
result_in_cache_gen [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
ret [definition, in CoqDSC.ErrorMonad]
reverse_map [lemma, in CoqDSC.Misc]
rev_nil [lemma, in CoqDSC.Misc]
rev_injective [lemma, in CoqDSC.Misc]
rm [definition, in CoqDSC.LibTactics]
S
SCallContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]SClosureCall [constructor, in CoqDSC.LambdaALOperationalSemantics]
SDCallContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]
SDefClosure [constructor, in CoqDSC.LambdaALOperationalSemantics]
SDNilContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]
SDReplaceCall [constructor, in CoqDSC.LambdaALOperationalSemantics]
SDTuple [constructor, in CoqDSC.LambdaALOperationalSemantics]
SDTupleContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]
SDVar [constructor, in CoqDSC.LambdaALOperationalSemantics]
shape_of_cts_generated_cache [lemma, in CoqDSC.ILambdaALCTSProofs]
shift [definition, in CoqDSC.ILambdaALDerive]
shift0 [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
skip_axiom [variable, in CoqDSC.LibTactics]
SNilContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]
sound_dprimitive [lemma, in CoqDSC.LambdaALValidity]
sound_dfixrec [lemma, in CoqDSC.LambdaALValidity]
sound_dcurry [lemma, in CoqDSC.LambdaALValidity]
sound_dpush [lemma, in CoqDSC.LambdaALValidity]
sound_dadd [lemma, in CoqDSC.LambdaALValidity]
sound_recompute [lemma, in CoqDSC.LambdaALValidity]
sound_eval [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
split_at [definition, in CoqDSC.Environment]
split_bind [lemma, in CoqDSC.Environment]
split_lookup [lemma, in CoqDSC.Environment]
SPrimitiveCall [constructor, in CoqDSC.LambdaALOperationalSemantics]
SPrimitiveNil [constructor, in CoqDSC.LambdaALOperationalSemantics]
Steps [constructor, in CoqDSC.LambdaALOperationalSemantics]
step_indexed_evaluation [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
step_indexed_dcall_inversion [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
STuple [constructor, in CoqDSC.LambdaALOperationalSemantics]
STupleContext [constructor, in CoqDSC.LambdaALOperationalSemanticsProofs]
SVar [constructor, in CoqDSC.LambdaALOperationalSemantics]
T
t [definition, in CoqDSC.ErrorMonad]t [definition, in CoqDSC.Environment]
take [definition, in CoqDSC.Misc]
take_drop [lemma, in CoqDSC.Misc]
TCachedVar [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TCachedVarUpdate [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TCallContext [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TClosureCall [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TDClosureChange [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TDPrimitiveNil [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TDReplaceCall [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TDResult [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TDTuple [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TEmptyCache [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TEmptyCacheUpdate [constructor, in CoqDSC.ILambdaALOperationalSemantics]
term [inductive, in CoqDSC.ILambdaAL]
term [inductive, in CoqDSC.LambdaAL]
tl_app [lemma, in CoqDSC.Misc]
TNilContext [constructor, in CoqDSC.ILambdaALOperationalSemantics]
toI [definition, in CoqDSC.LambdaALOperationalSemantics]
TPrimitiveCall [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TResult [constructor, in CoqDSC.ILambdaALOperationalSemantics]
ttuple [definition, in CoqDSC.LambdaAL]
TTuple [constructor, in CoqDSC.ILambdaALOperationalSemantics]
TTupleContext [constructor, in CoqDSC.ILambdaALOperationalSemantics]
tuple [definition, in CoqDSC.ILambdaAL]
tuple [definition, in CoqDSC.LambdaALValues]
Tuple [constructor, in CoqDSC.LambdaALValues]
tuple_result_in_cache [lemma, in CoqDSC.ILambdaALExtensionWithCaches]
U
uncts_values_cts_values [lemma, in CoqDSC.ILambdaALCTSProofs]uncts_value_cts_value [lemma, in CoqDSC.ILambdaALCTSProofs]
uncts_term_cts_term [lemma, in CoqDSC.ILambdaALCTSProofs]
uncts_values [definition, in CoqDSC.ILambdaALDerive]
uncts_value [definition, in CoqDSC.ILambdaALDerive]
uncts_term [definition, in CoqDSC.ILambdaALDerive]
und [definition, in CoqDSC.LambdaAL]
underive [definition, in CoqDSC.LambdaALDerive]
underive_derive [lemma, in CoqDSC.LambdaALDerive]
und_d [lemma, in CoqDSC.LambdaAL]
unfold_drel_term [lemma, in CoqDSC.LambdaALValidity]
unfold_drel_value [lemma, in CoqDSC.LambdaALValidity]
unfold_drels [lemma, in CoqDSC.LambdaALValidity]
uniq_commute [lemma, in CoqDSC.Misc]
V
ValidCons [constructor, in CoqDSC.LambdaALEnvValidity]ValidNil [constructor, in CoqDSC.LambdaALEnvValidity]
valid_denvironment_contains_ok_closure [lemma, in CoqDSC.LambdaALEnvValidity]
valid_denvironment_moves_well [lemma, in CoqDSC.LambdaALEnvValidity]
valid_denvironment_lookups_moves_well [lemma, in CoqDSC.LambdaALEnvValidity]
valid_denvironment_lookup_moves_well [lemma, in CoqDSC.LambdaALEnvValidity]
valid_closure_changes [definition, in CoqDSC.LambdaALEnvValidity]
valid_denvironment [inductive, in CoqDSC.LambdaALEnvValidity]
valid_dprimitive [definition, in CoqDSC.LambdaALValidity]
value [inductive, in CoqDSC.LambdaALValues]
value [inductive, in CoqDSC.ILambdaALValues]
values [inductive, in CoqDSC.LambdaALValues]
values [inductive, in CoqDSC.ILambdaALValues]
values_forall2_change [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
values_of_list_of_list_of_values [lemma, in CoqDSC.LambdaALOperationalSemanticsProofs]
values_forall2 [definition, in CoqDSC.LambdaALValues]
values_forall2_from [definition, in CoqDSC.LambdaALValues]
values_of_list [definition, in CoqDSC.LambdaALValues]
values_mut [definition, in CoqDSC.LambdaALValues]
values_of_list_list_of_values [lemma, in CoqDSC.ILambdaALOperationalSemanticsProofs]
values_of_list [definition, in CoqDSC.ILambdaALValues]
value_mutind [definition, in CoqDSC.LambdaALValues]
value_mut [definition, in CoqDSC.LambdaALValues]
Var [constructor, in CoqDSC.LambdaAL]
var [inductive, in CoqDSC.Index]
VCons [constructor, in CoqDSC.LambdaALValues]
VNil [constructor, in CoqDSC.LambdaALValues]
W
weaken [lemma, in CoqDSC.Environment]_
_3_7 [lemma, in CoqDSC.Overview]_3_6_B_1 [lemma, in CoqDSC.Overview]
_3_5 [lemma, in CoqDSC.Overview]
_3_4 [lemma, in CoqDSC.Overview]
_3_3 [lemma, in CoqDSC.Overview]
_3_2 [lemma, in CoqDSC.Overview]
_3_1 [lemma, in CoqDSC.Overview]
other
[# _ ; _ ; .. ; _ ] (ivalues_scope) [notation, in CoqDSC.ILambdaALValues][# ] (ivalues_scope) [notation, in CoqDSC.ILambdaALValues]
_ ⊕ _ (ivalue_scope) [notation, in CoqDSC.ILambdaALOperationalSemantics]
'let _ : _ := _ in _ (let_scope) [notation, in CoqDSC.LibTactics]
'let _ := _ in _ (let_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> _ (ltac_scope) [notation, in CoqDSC.LibTactics]
>> (ltac_scope) [notation, in CoqDSC.LibTactics]
___ (ltac_scope) [notation, in CoqDSC.LibTactics]
__ (ltac_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
exists _ , _ (type_scope) [notation, in CoqDSC.LibTactics]
[@# _ ; _ ; .. ; _ ] (values_scope) [notation, in CoqDSC.LambdaALValues]
[@# _ ] (values_scope) [notation, in CoqDSC.LambdaALValues]
[@# ] (values_scope) [notation, in CoqDSC.LambdaALValues]
[@ _ ; _ ; .. ; _ ] (values_scope) [notation, in CoqDSC.LambdaALValues]
[@ _ ] (values_scope) [notation, in CoqDSC.LambdaALValues]
[@ ] (values_scope) [notation, in CoqDSC.LambdaALValues]
_ ⊕ _ [notation, in CoqDSC.LambdaALOperationalSemantics]
_ <- _ ; _ [notation, in CoqDSC.ErrorMonad]
_ >>= _ [notation, in CoqDSC.ErrorMonad]
_ =' _ [notation, in CoqDSC.LibTactics]
nosimpl _ [notation, in CoqDSC.LibTactics]
Register _ _ [notation, in CoqDSC.LibTactics]
Something [notation, in CoqDSC.LibTactics]
@#( _ , _ ) [notation, in CoqDSC.ILambdaAL]
@( _ , _ ) [notation, in CoqDSC.LambdaAL]
[# _ ⊢ _ ⇑ _ ] [notation, in CoqDSC.ILambdaALOperationalSemantics]
[# _ ⊢ _ ⇓ _ ] [notation, in CoqDSC.ILambdaALOperationalSemantics]
[ _ ⊢ _ ⇓ _ @ _ ] [notation, in CoqDSC.LambdaALOperationalSemantics]
[ _ ⊢ _ ⇓ _ ] [notation, in CoqDSC.LambdaALOperationalSemantics]
[ _ ⊢ _ ▷ _ ⤳ _ ] [notation, in CoqDSC.LambdaALValidity]
[ _ ⊢ _ ⇑ _ ] [notation, in CoqDSC.LambdaALOperationalSemanticsProofs]
[ _ ⊢ _ ↑ _ ⇾ _ ] [notation, in CoqDSC.ILambdaALExtensionWithCaches]
[[# _ , _ ⊢ _ ⇓ _ ]] [notation, in CoqDSC.ILambdaALOperationalSemantics]
[[ _ ⊢ _ ⇓ _ @ _ ]] [notation, in CoqDSC.LambdaALOperationalSemantics]
[[ _ ⊢ _ ⇓ _ ]] [notation, in CoqDSC.LambdaALOperationalSemantics]
[[ _ ⊢ _ ⇑ _ ]] [notation, in CoqDSC.LambdaALOperationalSemanticsProofs]
[[ _ # _ ⊢ _ ↑ _ ⇾ _ ]] [notation, in CoqDSC.ILambdaALExtensionWithCaches]
⌈# _ ⌉ [notation, in CoqDSC.ILambdaALOperationalSemantics]
⌈ _ ⌉ [notation, in CoqDSC.LambdaALOperationalSemantics]
⌊# _ ⌋ [notation, in CoqDSC.ILambdaALOperationalSemantics]
⌊ _ ⌋ [notation, in CoqDSC.LambdaALOperationalSemantics]
Notation Index
other
[# _ ; _ ; .. ; _ ] (ivalues_scope) [in CoqDSC.ILambdaALValues][# ] (ivalues_scope) [in CoqDSC.ILambdaALValues]
_ ⊕ _ (ivalue_scope) [in CoqDSC.ILambdaALOperationalSemantics]
'let _ : _ := _ in _ (let_scope) [in CoqDSC.LibTactics]
'let _ := _ in _ (let_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ _ (ltac_scope) [in CoqDSC.LibTactics]
>> _ (ltac_scope) [in CoqDSC.LibTactics]
>> (ltac_scope) [in CoqDSC.LibTactics]
___ (ltac_scope) [in CoqDSC.LibTactics]
__ (ltac_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ _ , _ (type_scope) [in CoqDSC.LibTactics]
exists _ , _ (type_scope) [in CoqDSC.LibTactics]
[@# _ ; _ ; .. ; _ ] (values_scope) [in CoqDSC.LambdaALValues]
[@# _ ] (values_scope) [in CoqDSC.LambdaALValues]
[@# ] (values_scope) [in CoqDSC.LambdaALValues]
[@ _ ; _ ; .. ; _ ] (values_scope) [in CoqDSC.LambdaALValues]
[@ _ ] (values_scope) [in CoqDSC.LambdaALValues]
[@ ] (values_scope) [in CoqDSC.LambdaALValues]
_ ⊕ _ [in CoqDSC.LambdaALOperationalSemantics]
_ <- _ ; _ [in CoqDSC.ErrorMonad]
_ >>= _ [in CoqDSC.ErrorMonad]
_ =' _ [in CoqDSC.LibTactics]
nosimpl _ [in CoqDSC.LibTactics]
Register _ _ [in CoqDSC.LibTactics]
Something [in CoqDSC.LibTactics]
@#( _ , _ ) [in CoqDSC.ILambdaAL]
@( _ , _ ) [in CoqDSC.LambdaAL]
[# _ ⊢ _ ⇑ _ ] [in CoqDSC.ILambdaALOperationalSemantics]
[# _ ⊢ _ ⇓ _ ] [in CoqDSC.ILambdaALOperationalSemantics]
[ _ ⊢ _ ⇓ _ @ _ ] [in CoqDSC.LambdaALOperationalSemantics]
[ _ ⊢ _ ⇓ _ ] [in CoqDSC.LambdaALOperationalSemantics]
[ _ ⊢ _ ▷ _ ⤳ _ ] [in CoqDSC.LambdaALValidity]
[ _ ⊢ _ ⇑ _ ] [in CoqDSC.LambdaALOperationalSemanticsProofs]
[ _ ⊢ _ ↑ _ ⇾ _ ] [in CoqDSC.ILambdaALExtensionWithCaches]
[[# _ , _ ⊢ _ ⇓ _ ]] [in CoqDSC.ILambdaALOperationalSemantics]
[[ _ ⊢ _ ⇓ _ @ _ ]] [in CoqDSC.LambdaALOperationalSemantics]
[[ _ ⊢ _ ⇓ _ ]] [in CoqDSC.LambdaALOperationalSemantics]
[[ _ ⊢ _ ⇑ _ ]] [in CoqDSC.LambdaALOperationalSemanticsProofs]
[[ _ # _ ⊢ _ ↑ _ ⇾ _ ]] [in CoqDSC.ILambdaALExtensionWithCaches]
⌈# _ ⌉ [in CoqDSC.ILambdaALOperationalSemantics]
⌈ _ ⌉ [in CoqDSC.LambdaALOperationalSemantics]
⌊# _ ⌋ [in CoqDSC.ILambdaALOperationalSemantics]
⌊ _ ⌋ [in CoqDSC.LambdaALOperationalSemantics]
Module Index
L
LibTacticsCompatibility [in CoqDSC.LibTactics]Variable Index
E
equatesLemma.A0 [in CoqDSC.LibTactics]equatesLemma.A1 [in CoqDSC.LibTactics]
equatesLemma.A2 [in CoqDSC.LibTactics]
equatesLemma.A3 [in CoqDSC.LibTactics]
equatesLemma.A4 [in CoqDSC.LibTactics]
equatesLemma.A5 [in CoqDSC.LibTactics]
equatesLemma.A6 [in CoqDSC.LibTactics]
F
FuncEq.A1 [in CoqDSC.LibTactics]FuncEq.A2 [in CoqDSC.LibTactics]
FuncEq.A3 [in CoqDSC.LibTactics]
FuncEq.A4 [in CoqDSC.LibTactics]
FuncEq.A5 [in CoqDSC.LibTactics]
FuncEq.B [in CoqDSC.LibTactics]
FUNCTOR.n [in CoqDSC.LambdaALValidity]
FUNCTOR.rec_term [in CoqDSC.LambdaALValidity]
FUNCTOR.rec_value [in CoqDSC.LambdaALValidity]
S
skip_axiom [in CoqDSC.LibTactics]Library Index
C
ConstantsCrush
E
EnvironmentErrorMonad
I
ILambdaALILambdaALCTSProofs
ILambdaALDerive
ILambdaALDeriveProofs
ILambdaALExtensionWithCaches
ILambdaALOperationalSemantics
ILambdaALOperationalSemanticsPrimitives
ILambdaALOperationalSemanticsProofs
ILambdaALValues
Index
L
LambdaALLambdaALDerive
LambdaALDeriveProofs
LambdaALEnvValidity
LambdaALFundamentalProperty
LambdaALOperationalSemantics
LambdaALOperationalSemanticsPrimitives
LambdaALOperationalSemanticsProofs
LambdaALValidity
LambdaALValues
LibTactics
M
MiscO
OverviewLemma Index
A
app_comm_cons_2 [in CoqDSC.Misc]assoc_bind [in CoqDSC.ErrorMonad]
at_least_one_step_deval [in CoqDSC.LambdaALOperationalSemanticsProofs]
at_least_one_step [in CoqDSC.LambdaALOperationalSemanticsProofs]
B
bind_ret [in CoqDSC.ErrorMonad]bind_postbind [in CoqDSC.Environment]
bind_postbind_nil [in CoqDSC.Environment]
C
cache_of_call [in CoqDSC.ILambdaALExtensionWithCaches]cache_strenghening [in CoqDSC.ILambdaALCTSProofs]
cache_of_term_reverse_environment [in CoqDSC.ILambdaALCTSProofs]
call_evaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
call_inversion [in CoqDSC.LambdaALOperationalSemanticsProofs]
call_result_in_cache [in CoqDSC.ILambdaALExtensionWithCaches]
call_evaluation [in CoqDSC.ILambdaALOperationalSemanticsProofs]
closure_call_inversion [in CoqDSC.LambdaALOperationalSemanticsProofs]
closure_denvironment_of_list_list_of_closure_denvironment [in CoqDSC.LambdaALOperationalSemanticsProofs]
commute_bind [in CoqDSC.ErrorMonad]
complete_eval [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_curry [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_fixrec [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_push [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_add [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_recompute_primitive [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive_fixrec [in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_push [in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_curry [in CoqDSC.ILambdaALCTSProofs]
correct_dprimitive_add [in CoqDSC.ILambdaALCTSProofs]
correct_recompute [in CoqDSC.ILambdaALCTSProofs]
cts_derive_soundness [in CoqDSC.ILambdaALDeriveProofs]
cts_derive_cts_dvalue [in CoqDSC.ILambdaALDeriveProofs]
cts_derive_cts_dvalue_gen [in CoqDSC.ILambdaALDeriveProofs]
cts_denvironment_inherits_valid_modified_environment [in CoqDSC.ILambdaALExtensionWithCaches]
cts_closure_denvironment_cts_denvironment [in CoqDSC.ILambdaALCTSProofs]
cts_environment_has_no_cache [in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_denvironment [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_modified_environment2 [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_modified_environment [in CoqDSC.ILambdaALCTSProofs]
cts_value_injective [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_original_environment [in CoqDSC.ILambdaALCTSProofs]
cts_environment_preserves_length [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_preserves_length [in CoqDSC.ILambdaALCTSProofs]
cts_nonvar_has_nonempty_cache [in CoqDSC.ILambdaALCTSProofs]
cts_dvalues_cts_dbinding_2 [in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_binding [in CoqDSC.ILambdaALCTSProofs]
cts_values_cts_dbinding [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_lookups [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_lookup [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment_app [in CoqDSC.ILambdaALCTSProofs]
cts_environment_app [in CoqDSC.ILambdaALCTSProofs]
cts_environment_lookups [in CoqDSC.ILambdaALCTSProofs]
cts_environment_lookup [in CoqDSC.ILambdaALCTSProofs]
curry_adequacy [in CoqDSC.LambdaALOperationalSemanticsProofs]
D
dcall_inversion [in CoqDSC.LambdaALOperationalSemanticsProofs]dcall_evaluation [in CoqDSC.ILambdaALOperationalSemanticsProofs]
dclosure_only_applies_to_closure [in CoqDSC.LambdaALOperationalSemanticsProofs]
decompose_devaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
decompose_evaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
demo_clears_all_and_clears_but [in CoqDSC.LibTactics]
denvironment_equivalent_modulo_caches_original_evaluation [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_eval_cache [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_values_original [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_original_2 [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_original [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches_lookup_value_original [in CoqDSC.ILambdaALExtensionWithCaches]
depth_of_binding [in CoqDSC.ILambdaALCTSProofs]
depth_of_term_graft [in CoqDSC.ILambdaALCTSProofs]
derive_context_ended_with_call [in CoqDSC.LambdaALDeriveProofs]
derive_context_ended_with_tuple [in CoqDSC.LambdaALDeriveProofs]
derive_graft_tuple [in CoqDSC.LambdaALDeriveProofs]
derive_soundness2 [in CoqDSC.LambdaALDeriveProofs]
derive_soundness [in CoqDSC.LambdaALDeriveProofs]
derive_underive [in CoqDSC.LambdaALDerive]
deterministic_deval [in CoqDSC.LambdaALOperationalSemanticsProofs]
deterministic_eval [in CoqDSC.LambdaALOperationalSemanticsProofs]
drel_env_bind_rel_value [in CoqDSC.LambdaALFundamentalProperty]
drel_value_inversion [in CoqDSC.LambdaALValidity]
drel_env_dlookups [in CoqDSC.LambdaALValidity]
drel_value_move_value [in CoqDSC.LambdaALValidity]
drel_env_lookup2 [in CoqDSC.LambdaALValidity]
drel_env_lookup [in CoqDSC.LambdaALValidity]
drel_env_antimonotonic [in CoqDSC.LambdaALValidity]
drel_value_antimonotonic [in CoqDSC.LambdaALValidity]
drel_value_replace [in CoqDSC.LambdaALValidity]
drel_value_literal_inversion [in CoqDSC.LambdaALValidity]
drop_cons [in CoqDSC.Misc]
drop_decompose [in CoqDSC.Misc]
drop_inversion [in CoqDSC.Misc]
drop_nil [in CoqDSC.Misc]
drop_app [in CoqDSC.Misc]
dup_lemma [in CoqDSC.LibTactics]
d_und [in CoqDSC.LambdaAL]
E
equates_6 [in CoqDSC.LibTactics]equates_5 [in CoqDSC.LibTactics]
equates_4 [in CoqDSC.LibTactics]
equates_3 [in CoqDSC.LibTactics]
equates_2 [in CoqDSC.LibTactics]
equates_1 [in CoqDSC.LibTactics]
equates_0 [in CoqDSC.LibTactics]
eq_dec_nat_refl [in CoqDSC.Misc]
erase_steps_evaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
eval_cache_app_context [in CoqDSC.ILambdaALExtensionWithCaches]
eval_call_under_modified_extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
eval_call_under_old_extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
eval_under_extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_new_extended [in CoqDSC.ILambdaALExtensionWithCaches]
eval_cache_under_old_extended [in CoqDSC.ILambdaALExtensionWithCaches]
eval_deterministic [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_under_modified_environment_of_eval_cache_update [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_update_of_eval_cache_under_modified_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_deterministic [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_weakening [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_preserves_length [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_primitive_add_cache [in CoqDSC.ILambdaALOperationalSemanticsProofs]
eval_cache_of_cts_term [in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat [in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat_gen_nosteps [in CoqDSC.ILambdaALCTSProofs]
eval_cts_compat_gen [in CoqDSC.ILambdaALCTSProofs]
eval_dprimitive_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_primitive_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_fixrec_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_curry_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_push_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_add_cts_value [in CoqDSC.ILambdaALCTSProofs]
eval_cache_strenghening [in CoqDSC.ILambdaALCTSProofs]
eval_context_ended_with_call [in CoqDSC.ILambdaALCTSProofs]
eval_context_ended_with_tuple [in CoqDSC.ILambdaALCTSProofs]
eval_context_length [in CoqDSC.ILambdaALCTSProofs]
extended_with_old_caches_lookup [in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_caches_lookups [in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_new_caches_lookup_modified_env [in CoqDSC.ILambdaALExtensionWithCaches]
extended_with_caches_lookup [in CoqDSC.ILambdaALExtensionWithCaches]
extend_new_environment_with_call [in CoqDSC.ILambdaALExtensionWithCaches]
extend_old_environment_with_call [in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup_cts_denvironment [in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup2 [in CoqDSC.ILambdaALExtensionWithCaches]
extension_lookup [in CoqDSC.ILambdaALExtensionWithCaches]
extension_length_is_depth_of_context [in CoqDSC.ILambdaALExtensionWithCaches]
extension_preserves_length [in CoqDSC.ILambdaALExtensionWithCaches]
extension_components [in CoqDSC.ILambdaALExtensionWithCaches]
extract_original_and_modified_evaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
F
focus_lookup [in CoqDSC.Environment]func_eq_5 [in CoqDSC.LibTactics]
func_eq_4 [in CoqDSC.LibTactics]
func_eq_3 [in CoqDSC.LibTactics]
func_eq_2 [in CoqDSC.LibTactics]
func_eq_1 [in CoqDSC.LibTactics]
fundamental_lemma [in CoqDSC.LambdaALFundamentalProperty]
G
graft_binding_depth [in CoqDSC.ILambdaALExtensionWithCaches]graft_var_depth [in CoqDSC.ILambdaALExtensionWithCaches]
graft_hole [in CoqDSC.ILambdaALExtensionWithCaches]
graft_assoc [in CoqDSC.ILambdaALExtensionWithCaches]
graft_tuple [in CoqDSC.ILambdaALOperationalSemanticsProofs]
graft_def [in CoqDSC.ILambdaALOperationalSemanticsProofs]
I
iff_intro_swap [in CoqDSC.LibTactics]induct_height_max2 [in CoqDSC.LibTactics]
injective_closure_denvironment_of_list [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_underive [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_und [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_und [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_d [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_d [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_map_injf [in CoqDSC.LambdaALOperationalSemanticsProofs]
injective_values_of_list [in CoqDSC.LambdaALOperationalSemanticsProofs]
invalid_lookup [in CoqDSC.Environment]
inverse_move_closure [in CoqDSC.LambdaALOperationalSemanticsProofs]
inverse_modified_environment_bind [in CoqDSC.LambdaALOperationalSemanticsProofs]
inverse_primitive_call_evaluation [in CoqDSC.ILambdaALOperationalSemanticsProofs]
inverse_closure_call_evaluation [in CoqDSC.ILambdaALOperationalSemanticsProofs]
inverse_call_evaluation [in CoqDSC.ILambdaALOperationalSemanticsProofs]
invert_rel_env [in CoqDSC.LambdaALEnvValidity]
invert_move_values_cons [in CoqDSC.LambdaALOperationalSemanticsProofs]
invert_move_values_nil [in CoqDSC.LambdaALOperationalSemanticsProofs]
invert_rel_env_append [in CoqDSC.ILambdaALExtensionWithCaches]
invert_rel_env_len [in CoqDSC.ILambdaALExtensionWithCaches]
inv_error_mbind2 [in CoqDSC.ErrorMonad]
inv_error_mbind [in CoqDSC.ErrorMonad]
inv_success_mbind2 [in CoqDSC.ErrorMonad]
inv_success_mbind [in CoqDSC.ErrorMonad]
L
length_of_eval_context [in CoqDSC.ILambdaALCTSProofs]length_tl [in CoqDSC.Misc]
let_binding_unfold [in CoqDSC.LibTactics]
lift_lookup [in CoqDSC.Environment]
list_of_closure_denvironment_closure_denvironment_of_list [in CoqDSC.LambdaALOperationalSemanticsProofs]
list_of_ldvalues_of_ldvalues_of_list [in CoqDSC.LambdaALOperationalSemanticsProofs]
list_of_values_of_values_of_list [in CoqDSC.LambdaALOperationalSemanticsProofs]
list_map_post_cons [in CoqDSC.ErrorMonad]
list_map_cons [in CoqDSC.ErrorMonad]
list_map_app [in CoqDSC.ErrorMonad]
list_map_length [in CoqDSC.ErrorMonad]
list_of_closure_environment_of_closure_environment_of_list [in CoqDSC.ILambdaALOperationalSemanticsProofs]
list_of_closure_environment_cts_environment [in CoqDSC.ILambdaALCTSProofs]
list_map_lookup_2 [in CoqDSC.Environment]
list_map_lookup [in CoqDSC.Environment]
lookups_nil [in CoqDSC.LambdaALValidity]
lookups_modified_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookups_original_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookups_length [in CoqDSC.Environment]
lookup_move_environment [in CoqDSC.LambdaALEnvValidity]
lookup_env_of_denv [in CoqDSC.LambdaALEnvValidity]
lookup_original_of_extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
lookup_value_tail [in CoqDSC.ILambdaALExtensionWithCaches]
lookup_in_modified_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_modified_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_modified_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_original_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_original_environment [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_unfold [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_value_lookup_2 [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_value_lookup [in CoqDSC.ILambdaALOperationalSemanticsProofs]
lookup_values_is_cache_independent [in CoqDSC.ILambdaALCTSProofs]
lookup_value_is_cache_independent [in CoqDSC.ILambdaALCTSProofs]
lookup_app_2 [in CoqDSC.Environment]
lookup_app [in CoqDSC.Environment]
ltac_something_show [in CoqDSC.LibTactics]
ltac_something_hide [in CoqDSC.LibTactics]
ltac_something_eq [in CoqDSC.LibTactics]
ltac_database_provide [in CoqDSC.LibTactics]
lt_lt [in CoqDSC.Misc]
lt_comp [in CoqDSC.Misc]
M
map_und_d_id [in CoqDSC.LambdaAL]map_modified_binding_is_move_values [in CoqDSC.ILambdaALOperationalSemanticsProofs]
map_lookups [in CoqDSC.Environment]
map_lookup_2 [in CoqDSC.Environment]
map_lookup [in CoqDSC.Environment]
map_equiv_length [in CoqDSC.Misc]
map_id [in CoqDSC.Misc]
map_equiv [in CoqDSC.Misc]
map_map [in CoqDSC.Misc]
minus_factorize [in CoqDSC.Misc]
minus_commute [in CoqDSC.Misc]
modified_environment_under_rel_env [in CoqDSC.LambdaALEnvValidity]
modified_environment_of_rel_env [in CoqDSC.ILambdaALDeriveProofs]
modified_env_of_drel_env [in CoqDSC.LambdaALValidity]
modified_environment_of_closure_denvironment [in CoqDSC.LambdaALDeriveProofs]
modified_environment_lookups [in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_lookup [in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_app [in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_bind [in CoqDSC.LambdaALOperationalSemanticsProofs]
modified_environment_bind [in CoqDSC.ILambdaALOperationalSemanticsProofs]
modified_environment_implied_valid_moves [in CoqDSC.ILambdaALOperationalSemanticsProofs]
move_original_closure_environment [in CoqDSC.LambdaALOperationalSemanticsProofs]
move_with_eval_dprimitive [in CoqDSC.LambdaALOperationalSemanticsProofs]
move_replace [in CoqDSC.LambdaALOperationalSemanticsProofs]
move_tuple [in CoqDSC.LambdaALOperationalSemanticsProofs]
move_closure_environment_move_environment [in CoqDSC.LambdaALOperationalSemanticsProofs]
move_replace [in CoqDSC.ILambdaALOperationalSemanticsProofs]
move_nil [in CoqDSC.ILambdaALOperationalSemanticsProofs]
move_closure_environment_cts_denvironment [in CoqDSC.ILambdaALCTSProofs]
move_closure_environments [in CoqDSC.ILambdaALCTSProofs]
move_cts_values [in CoqDSC.ILambdaALCTSProofs]
move_cts_value [in CoqDSC.ILambdaALCTSProofs]
O
original_environment_under_rel_env [in CoqDSC.LambdaALEnvValidity]original_environment_of_rel_env [in CoqDSC.ILambdaALDeriveProofs]
original_env_of_drel_env [in CoqDSC.LambdaALValidity]
original_environment_lookups [in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_lookup [in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_app [in CoqDSC.LambdaALOperationalSemanticsProofs]
original_environment_bind [in CoqDSC.LambdaALOperationalSemanticsProofs]
original_cts_denvironment_has_no_cache [in CoqDSC.ILambdaALCTSProofs]
P
postbind_of_single [in CoqDSC.Environment]post_extend_new_with_tuple [in CoqDSC.ILambdaALExtensionWithCaches]
post_extend_old_with_tuple [in CoqDSC.ILambdaALExtensionWithCaches]
pre_drel_env__lookup [in CoqDSC.LambdaALValidity]
pre_drel_env_alt [in CoqDSC.LambdaALValidity]
primitive_call_inversion [in CoqDSC.LambdaALOperationalSemanticsProofs]
R
recompute_primitive_eq [in CoqDSC.LambdaALOperationalSemanticsProofs]recompute_primitive_eq [in CoqDSC.ILambdaALCTSProofs]
recurse_valid [in CoqDSC.LambdaALValidity]
related_tuples [in CoqDSC.LambdaALFundamentalProperty]
related_calls [in CoqDSC.LambdaALFundamentalProperty]
related_primitive_calls [in CoqDSC.LambdaALFundamentalProperty]
related_lookups [in CoqDSC.LambdaALValidity]
rel_env_lookup_change [in CoqDSC.LambdaALEnvValidity]
rel_env_length [in CoqDSC.LambdaALEnvValidity]
rel_env_through_context_evaluation [in CoqDSC.LambdaALEnvValidity]
rel_env_lookup_value [in CoqDSC.LambdaALEnvValidity]
rel_env_lookup_value' [in CoqDSC.LambdaALEnvValidity]
restrict_lookup_2 [in CoqDSC.Environment]
restrict_lookup [in CoqDSC.Environment]
result_in_cache_gen [in CoqDSC.ILambdaALExtensionWithCaches]
reverse_map [in CoqDSC.Misc]
rev_nil [in CoqDSC.Misc]
rev_injective [in CoqDSC.Misc]
S
shape_of_cts_generated_cache [in CoqDSC.ILambdaALCTSProofs]shift0 [in CoqDSC.ILambdaALExtensionWithCaches]
sound_dprimitive [in CoqDSC.LambdaALValidity]
sound_dfixrec [in CoqDSC.LambdaALValidity]
sound_dcurry [in CoqDSC.LambdaALValidity]
sound_dpush [in CoqDSC.LambdaALValidity]
sound_dadd [in CoqDSC.LambdaALValidity]
sound_recompute [in CoqDSC.LambdaALValidity]
sound_eval [in CoqDSC.LambdaALOperationalSemanticsProofs]
split_bind [in CoqDSC.Environment]
split_lookup [in CoqDSC.Environment]
step_indexed_evaluation [in CoqDSC.LambdaALOperationalSemanticsProofs]
step_indexed_dcall_inversion [in CoqDSC.LambdaALOperationalSemanticsProofs]
T
take_drop [in CoqDSC.Misc]tl_app [in CoqDSC.Misc]
tuple_result_in_cache [in CoqDSC.ILambdaALExtensionWithCaches]
U
uncts_values_cts_values [in CoqDSC.ILambdaALCTSProofs]uncts_value_cts_value [in CoqDSC.ILambdaALCTSProofs]
uncts_term_cts_term [in CoqDSC.ILambdaALCTSProofs]
underive_derive [in CoqDSC.LambdaALDerive]
und_d [in CoqDSC.LambdaAL]
unfold_drel_term [in CoqDSC.LambdaALValidity]
unfold_drel_value [in CoqDSC.LambdaALValidity]
unfold_drels [in CoqDSC.LambdaALValidity]
uniq_commute [in CoqDSC.Misc]
V
valid_denvironment_contains_ok_closure [in CoqDSC.LambdaALEnvValidity]valid_denvironment_moves_well [in CoqDSC.LambdaALEnvValidity]
valid_denvironment_lookups_moves_well [in CoqDSC.LambdaALEnvValidity]
valid_denvironment_lookup_moves_well [in CoqDSC.LambdaALEnvValidity]
values_forall2_change [in CoqDSC.LambdaALOperationalSemanticsProofs]
values_of_list_of_list_of_values [in CoqDSC.LambdaALOperationalSemanticsProofs]
values_of_list_list_of_values [in CoqDSC.ILambdaALOperationalSemanticsProofs]
W
weaken [in CoqDSC.Environment]_
_3_7 [in CoqDSC.Overview]_3_6_B_1 [in CoqDSC.Overview]
_3_5 [in CoqDSC.Overview]
_3_4 [in CoqDSC.Overview]
_3_3 [in CoqDSC.Overview]
_3_2 [in CoqDSC.Overview]
_3_1 [in CoqDSC.Overview]
Constructor Index
A
Add [in CoqDSC.Constants]B
BExtendNil [in CoqDSC.ILambdaALExtensionWithCaches]BExtendWithOldDef [in CoqDSC.ILambdaALExtensionWithCaches]
BExtendWithTuple [in CoqDSC.ILambdaALExtensionWithCaches]
boxer [in CoqDSC.LibTactics]
C
Cache [in CoqDSC.ILambdaAL]CacheValue [in CoqDSC.ILambdaALValues]
CDCons [in CoqDSC.LambdaALValues]
CDNil [in CoqDSC.LambdaALValues]
Closure [in CoqDSC.LambdaALValues]
ConsHasNoCache [in CoqDSC.ILambdaALOperationalSemanticsProofs]
Curry [in CoqDSC.Constants]
D
d [in CoqDSC.LambdaAL]dClosure [in CoqDSC.LambdaALValues]
dClosureValid [in CoqDSC.LambdaALValidity]
dDef [in CoqDSC.LambdaAL]
dDefTuple [in CoqDSC.LambdaAL]
Def [in CoqDSC.LambdaAL]
DefTuple [in CoqDSC.LambdaAL]
dIClosure [in CoqDSC.ILambdaALValues]
dIDef [in CoqDSC.ILambdaAL]
dIDefTuple [in CoqDSC.ILambdaAL]
dILiteral [in CoqDSC.ILambdaALValues]
dIPrimitiveNil [in CoqDSC.ILambdaALValues]
dIReplace [in CoqDSC.ILambdaALValues]
dIResult [in CoqDSC.ILambdaAL]
dITuple [in CoqDSC.ILambdaALValues]
dLiteral [in CoqDSC.LambdaALValues]
dLitValid [in CoqDSC.LambdaALValidity]
dPos [in CoqDSC.Constants]
dPrimitiveNil [in CoqDSC.LambdaALValues]
dPrimitiveNilValid [in CoqDSC.LambdaALValidity]
DrelCons [in CoqDSC.LambdaALValidity]
DrelNil [in CoqDSC.LambdaALValidity]
dReplace [in CoqDSC.LambdaALValues]
dReplaceValid [in CoqDSC.LambdaALValidity]
dTuple [in CoqDSC.LambdaALValues]
dTupleValid [in CoqDSC.LambdaALValidity]
dVar [in CoqDSC.LambdaAL]
DVCons [in CoqDSC.LambdaALValues]
DVNil [in CoqDSC.LambdaALValues]
E
ExtendNil [in CoqDSC.ILambdaALExtensionWithCaches]ExtendWithNewDef [in CoqDSC.ILambdaALExtensionWithCaches]
ExtendWithOldDef [in CoqDSC.ILambdaALExtensionWithCaches]
ExtendWithTuple [in CoqDSC.ILambdaALExtensionWithCaches]
F
FixRec [in CoqDSC.Constants]I
IClosure [in CoqDSC.ILambdaALValues]IDef [in CoqDSC.ILambdaAL]
IDefTuple [in CoqDSC.ILambdaAL]
Idx [in CoqDSC.Index]
ILiteral [in CoqDSC.ILambdaALValues]
IPrimitive [in CoqDSC.ILambdaALValues]
IResult [in CoqDSC.ILambdaAL]
ITuple [in CoqDSC.ILambdaALValues]
IVCons [in CoqDSC.ILambdaALValues]
IVNil [in CoqDSC.ILambdaALValues]
L
Literal [in CoqDSC.LambdaALValues]ltac_goal_to_discard_intro [in CoqDSC.LibTactics]
ltac_database_token [in CoqDSC.LibTactics]
ltac_mark [in CoqDSC.LibTactics]
ltac_wilds [in CoqDSC.LibTactics]
ltac_wild [in CoqDSC.LibTactics]
ltac_no_arg [in CoqDSC.LibTactics]
N
Nat [in CoqDSC.Constants]New [in CoqDSC.ILambdaALExtensionWithCaches]
NilHasNoCache [in CoqDSC.ILambdaALOperationalSemanticsProofs]
NoSteps [in CoqDSC.LambdaALOperationalSemantics]
O
Old [in CoqDSC.ILambdaALExtensionWithCaches]P
Primitive [in CoqDSC.LambdaALValues]Push [in CoqDSC.Constants]
S
SCallContext [in CoqDSC.LambdaALOperationalSemanticsProofs]SClosureCall [in CoqDSC.LambdaALOperationalSemantics]
SDCallContext [in CoqDSC.LambdaALOperationalSemanticsProofs]
SDefClosure [in CoqDSC.LambdaALOperationalSemantics]
SDNilContext [in CoqDSC.LambdaALOperationalSemanticsProofs]
SDReplaceCall [in CoqDSC.LambdaALOperationalSemantics]
SDTuple [in CoqDSC.LambdaALOperationalSemantics]
SDTupleContext [in CoqDSC.LambdaALOperationalSemanticsProofs]
SDVar [in CoqDSC.LambdaALOperationalSemantics]
SNilContext [in CoqDSC.LambdaALOperationalSemanticsProofs]
SPrimitiveCall [in CoqDSC.LambdaALOperationalSemantics]
SPrimitiveNil [in CoqDSC.LambdaALOperationalSemantics]
Steps [in CoqDSC.LambdaALOperationalSemantics]
STuple [in CoqDSC.LambdaALOperationalSemantics]
STupleContext [in CoqDSC.LambdaALOperationalSemanticsProofs]
SVar [in CoqDSC.LambdaALOperationalSemantics]
T
TCachedVar [in CoqDSC.ILambdaALOperationalSemantics]TCachedVarUpdate [in CoqDSC.ILambdaALOperationalSemantics]
TCallContext [in CoqDSC.ILambdaALOperationalSemantics]
TClosureCall [in CoqDSC.ILambdaALOperationalSemantics]
TDClosureChange [in CoqDSC.ILambdaALOperationalSemantics]
TDPrimitiveNil [in CoqDSC.ILambdaALOperationalSemantics]
TDReplaceCall [in CoqDSC.ILambdaALOperationalSemantics]
TDResult [in CoqDSC.ILambdaALOperationalSemantics]
TDTuple [in CoqDSC.ILambdaALOperationalSemantics]
TEmptyCache [in CoqDSC.ILambdaALOperationalSemantics]
TEmptyCacheUpdate [in CoqDSC.ILambdaALOperationalSemantics]
TNilContext [in CoqDSC.ILambdaALOperationalSemantics]
TPrimitiveCall [in CoqDSC.ILambdaALOperationalSemantics]
TResult [in CoqDSC.ILambdaALOperationalSemantics]
TTuple [in CoqDSC.ILambdaALOperationalSemantics]
TTupleContext [in CoqDSC.ILambdaALOperationalSemantics]
Tuple [in CoqDSC.LambdaALValues]
V
ValidCons [in CoqDSC.LambdaALEnvValidity]ValidNil [in CoqDSC.LambdaALEnvValidity]
Var [in CoqDSC.LambdaAL]
VCons [in CoqDSC.LambdaALValues]
VNil [in CoqDSC.LambdaALValues]
Axiom Index
F
fun_extensionality [in CoqDSC.LambdaALValidity]I
inj_pair2 [in CoqDSC.LibTactics]P
prop_extensionality [in CoqDSC.LambdaALValidity]Inductive Index
B
base_extended_with_cache [in CoqDSC.ILambdaALExtensionWithCaches]Boxer [in CoqDSC.LibTactics]
C
cache_var [in CoqDSC.ILambdaAL]cache_value [in CoqDSC.ILambdaALValues]
closure_denvironment [in CoqDSC.LambdaALValues]
D
deval [in CoqDSC.ILambdaALOperationalSemantics]dliteral [in CoqDSC.Constants]
drel_value_inductive [in CoqDSC.LambdaALValidity]
dterm [in CoqDSC.ILambdaAL]
dterm [in CoqDSC.LambdaAL]
dvalue [in CoqDSC.LambdaALValues]
dvalue [in CoqDSC.ILambdaALValues]
dvar [in CoqDSC.LambdaAL]
E
eval [in CoqDSC.ILambdaALOperationalSemantics]eval_dcontext [in CoqDSC.LambdaALOperationalSemanticsProofs]
eval_context [in CoqDSC.LambdaALOperationalSemanticsProofs]
eval_cache_update [in CoqDSC.ILambdaALOperationalSemantics]
eval_context [in CoqDSC.ILambdaALOperationalSemantics]
eval_cache [in CoqDSC.ILambdaALOperationalSemantics]
extended_with_cache [in CoqDSC.ILambdaALExtensionWithCaches]
extension [in CoqDSC.ILambdaALExtensionWithCaches]
G
gdeval [in CoqDSC.LambdaALOperationalSemantics]geval [in CoqDSC.LambdaALOperationalSemantics]
H
has_no_cache [in CoqDSC.ILambdaALOperationalSemanticsProofs]I
indexType [in CoqDSC.LambdaALOperationalSemantics]L
ldvalues [in CoqDSC.LambdaALValues]literal [in CoqDSC.Constants]
ltac_goal_to_discard [in CoqDSC.LibTactics]
Ltac_database_token [in CoqDSC.LibTactics]
ltac_Mark [in CoqDSC.LibTactics]
ltac_Wilds [in CoqDSC.LibTactics]
ltac_Wild [in CoqDSC.LibTactics]
ltac_No_arg [in CoqDSC.LibTactics]
P
pre_drel_env [in CoqDSC.LambdaALValidity]primitive [in CoqDSC.Constants]
T
term [in CoqDSC.ILambdaAL]term [in CoqDSC.LambdaAL]
V
valid_denvironment [in CoqDSC.LambdaALEnvValidity]value [in CoqDSC.LambdaALValues]
value [in CoqDSC.ILambdaALValues]
values [in CoqDSC.LambdaALValues]
values [in CoqDSC.ILambdaALValues]
var [in CoqDSC.Index]
Section Index
E
equatesLemma [in CoqDSC.LibTactics]F
FuncEq [in CoqDSC.LibTactics]FUNCTOR [in CoqDSC.LambdaALValidity]
Definition Index
B
bind [in CoqDSC.Environment]binding [in CoqDSC.ILambdaALCTSProofs]
C
cache [in CoqDSC.ILambdaAL]cache_update [in CoqDSC.ILambdaAL]
cache_update_of_term [in CoqDSC.ILambdaALDerive]
cache_of_term [in CoqDSC.ILambdaALDerive]
call [in CoqDSC.ILambdaAL]
call [in CoqDSC.LambdaAL]
closure [in CoqDSC.LambdaALValues]
closure_environment_of_list [in CoqDSC.ILambdaALOperationalSemantics]
closure_denvironment_of_list [in CoqDSC.LambdaALValues]
COIND [in CoqDSC.LibTactics]
compile_binding [in CoqDSC.ILambdaALCTSProofs]
congruence_hypothesis [in CoqDSC.LambdaALFundamentalProperty]
context [in CoqDSC.LambdaAL]
context [in CoqDSC.ILambdaALOperationalSemantics]
correct_dprimitive [in CoqDSC.LambdaALOperationalSemanticsProofs]
correct_dprimitive [in CoqDSC.ILambdaALCTSProofs]
cts_denvironment [in CoqDSC.ILambdaALDerive]
cts_dbinding [in CoqDSC.ILambdaALDerive]
cts_environment [in CoqDSC.ILambdaALDerive]
cts_binding [in CoqDSC.ILambdaALDerive]
cts_dvalues [in CoqDSC.ILambdaALDerive]
cts_closure_denvironment [in CoqDSC.ILambdaALDerive]
cts_dvalue [in CoqDSC.ILambdaALDerive]
cts_dterm [in CoqDSC.ILambdaALDerive]
cts_values [in CoqDSC.ILambdaALDerive]
cts_value [in CoqDSC.ILambdaALDerive]
cts_derive [in CoqDSC.ILambdaALDerive]
cts_derive_term [in CoqDSC.ILambdaALDerive]
cts_term [in CoqDSC.ILambdaALDerive]
cts_term_aux [in CoqDSC.ILambdaALDerive]
D
dcall [in CoqDSC.ILambdaAL]dcall [in CoqDSC.LambdaAL]
dclosure [in CoqDSC.LambdaALValues]
dcontext [in CoqDSC.LambdaAL]
denvironment [in CoqDSC.LambdaALOperationalSemantics]
denvironment [in CoqDSC.ILambdaALOperationalSemantics]
denvironment_of_closure_denvironment [in CoqDSC.LambdaALOperationalSemantics]
denvironment_of_dclosure_denvironment [in CoqDSC.ILambdaALOperationalSemantics]
denvironment_equivalent_modulo_caches_extend [in CoqDSC.ILambdaALExtensionWithCaches]
denvironment_equivalent_modulo_caches [in CoqDSC.ILambdaALExtensionWithCaches]
depth_of_term [in CoqDSC.ILambdaALDerive]
derive [in CoqDSC.LambdaALDerive]
derive_binding [in CoqDSC.ILambdaALCTSProofs]
deval [in CoqDSC.LambdaALOperationalSemantics]
dgraft [in CoqDSC.LambdaAL]
dliteral [in CoqDSC.ILambdaALValues]
dNilpdenv [in CoqDSC.LambdaALDerive]
dNilpldvalues [in CoqDSC.LambdaALDerive]
dNil' [in CoqDSC.LambdaALDerive]
done [in CoqDSC.Crush]
drels [in CoqDSC.LambdaALValidity]
drels_F [in CoqDSC.LambdaALValidity]
drels_type [in CoqDSC.LambdaALValidity]
drel_env [in CoqDSC.LambdaALValidity]
drel_term [in CoqDSC.LambdaALValidity]
drel_value [in CoqDSC.LambdaALValidity]
drel_term_F [in CoqDSC.LambdaALValidity]
drel_value_F [in CoqDSC.LambdaALValidity]
drop [in CoqDSC.Misc]
dttuple [in CoqDSC.LambdaAL]
dtuple [in CoqDSC.ILambdaAL]
dtuple [in CoqDSC.LambdaALValues]
dvar [in CoqDSC.ILambdaAL]
E
environment [in CoqDSC.LambdaALOperationalSemantics]environment [in CoqDSC.ILambdaALOperationalSemantics]
eq' [in CoqDSC.LibTactics]
error [in CoqDSC.ErrorMonad]
eval [in CoqDSC.LambdaALOperationalSemantics]
eval_primitive [in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_fixrec [in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_push [in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_curry [in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_add [in CoqDSC.ILambdaALOperationalSemanticsPrimitives]
eval_dprimitive [in CoqDSC.LambdaALOperationalSemantics]
eval_dfixrec [in CoqDSC.LambdaALOperationalSemantics]
eval_dcurry [in CoqDSC.LambdaALOperationalSemantics]
eval_dpush [in CoqDSC.LambdaALOperationalSemantics]
eval_dadd [in CoqDSC.LambdaALOperationalSemantics]
eval_dprimitive [in CoqDSC.ILambdaALOperationalSemantics]
eval_dfixrec [in CoqDSC.ILambdaALOperationalSemantics]
eval_dcurry [in CoqDSC.ILambdaALOperationalSemantics]
eval_dpush [in CoqDSC.ILambdaALOperationalSemantics]
eval_dadd [in CoqDSC.ILambdaALOperationalSemantics]
eval_primitive [in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_fixrec [in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_curry [in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_push [in CoqDSC.LambdaALOperationalSemanticsPrimitives]
eval_add [in CoqDSC.LambdaALOperationalSemanticsPrimitives]
extended_environment [in CoqDSC.ILambdaALExtensionWithCaches]
G
graft [in CoqDSC.LambdaAL]I
index [in CoqDSC.LambdaALOperationalSemantics]L
ldvalues_of_list [in CoqDSC.LambdaALValues]let_binding [in CoqDSC.LibTactics]
lift [in CoqDSC.Index]
list_of_closure_denvironment [in CoqDSC.ILambdaALOperationalSemantics]
list_of_closure_environment [in CoqDSC.ILambdaALOperationalSemantics]
list_of_closure_denvironment [in CoqDSC.LambdaALValues]
list_of_ldvalues [in CoqDSC.LambdaALValues]
list_of_values [in CoqDSC.LambdaALValues]
list_map2 [in CoqDSC.ErrorMonad]
list_map [in CoqDSC.ErrorMonad]
list_of_values [in CoqDSC.ILambdaALValues]
literal [in CoqDSC.ILambdaALValues]
lookup [in CoqDSC.Environment]
lookups [in CoqDSC.Environment]
lookup_cache [in CoqDSC.ILambdaALOperationalSemantics]
lookup_values [in CoqDSC.ILambdaALOperationalSemantics]
lookup_value [in CoqDSC.ILambdaALOperationalSemantics]
ltac_something [in CoqDSC.LibTactics]
ltac_to_generalize [in CoqDSC.LibTactics]
ltac_tag_subst [in CoqDSC.LibTactics]
ltac_nat_from_int [in CoqDSC.LibTactics]
ltac_database [in CoqDSC.LibTactics]
M
mbind [in CoqDSC.ErrorMonad]modified_environment [in CoqDSC.LambdaALOperationalSemantics]
modified_environment [in CoqDSC.ILambdaALOperationalSemantics]
modified_binding [in CoqDSC.ILambdaALOperationalSemantics]
move [in CoqDSC.LambdaALOperationalSemantics]
move [in CoqDSC.ILambdaALOperationalSemantics]
move_environment [in CoqDSC.LambdaALOperationalSemantics]
move_values [in CoqDSC.LambdaALOperationalSemantics]
move_closure_environment [in CoqDSC.LambdaALOperationalSemantics]
move_literal [in CoqDSC.LambdaALOperationalSemantics]
move_values [in CoqDSC.ILambdaALOperationalSemantics]
move_closure_environment [in CoqDSC.ILambdaALOperationalSemantics]
move_literal [in CoqDSC.ILambdaALOperationalSemantics]
N
neval [in CoqDSC.LambdaALOperationalSemantics]nil_literal [in CoqDSC.LambdaALDerive]
O
original_environment [in CoqDSC.LambdaALOperationalSemantics]original_environment [in CoqDSC.ILambdaALOperationalSemantics]
P
postbind [in CoqDSC.Environment]primitive [in CoqDSC.ILambdaALValues]
R
recompute_primitive [in CoqDSC.LambdaALOperationalSemantics]recompute_primitive [in CoqDSC.ILambdaALOperationalSemantics]
rel_env [in CoqDSC.LambdaALEnvValidity]
rel_value [in CoqDSC.LambdaALEnvValidity]
ret [in CoqDSC.ErrorMonad]
rm [in CoqDSC.LibTactics]
S
shift [in CoqDSC.ILambdaALDerive]split_at [in CoqDSC.Environment]
T
t [in CoqDSC.ErrorMonad]t [in CoqDSC.Environment]
take [in CoqDSC.Misc]
toI [in CoqDSC.LambdaALOperationalSemantics]
ttuple [in CoqDSC.LambdaAL]
tuple [in CoqDSC.ILambdaAL]
tuple [in CoqDSC.LambdaALValues]
U
uncts_values [in CoqDSC.ILambdaALDerive]uncts_value [in CoqDSC.ILambdaALDerive]
uncts_term [in CoqDSC.ILambdaALDerive]
und [in CoqDSC.LambdaAL]
underive [in CoqDSC.LambdaALDerive]
V
valid_closure_changes [in CoqDSC.LambdaALEnvValidity]valid_dprimitive [in CoqDSC.LambdaALValidity]
values_forall2 [in CoqDSC.LambdaALValues]
values_forall2_from [in CoqDSC.LambdaALValues]
values_of_list [in CoqDSC.LambdaALValues]
values_mut [in CoqDSC.LambdaALValues]
values_of_list [in CoqDSC.ILambdaALValues]
value_mutind [in CoqDSC.LambdaALValues]
value_mut [in CoqDSC.LambdaALValues]
| 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 | (751 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 | (62 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 | (17 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 | (27 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (324 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 | (108 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3 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 | (43 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 | (3 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (163 entries) |