applys_eq_init [in LibTactics]
args_eq_7 [in LibTactics]
args_eq_6 [in LibTactics]
args_eq_5 [in LibTactics]
args_eq_4 [in LibTactics]
args_eq_3 [in LibTactics]
args_eq_2 [in LibTactics]
args_eq_1 [in LibTactics]
assign_aequiv [in Equiv]
assign_removes [in PE]
B
bequiv_example [in Equiv]bexp_eval_false [in Hoare]
C
CAsgn_congruence [in Equiv]ceval_extensionality [in PE]
CIf_congruence [in Equiv]
CImp.par_loop_any_X [in Smallstep]
CImp.par_body_n [in Smallstep]
CImp.par_body_n__Sn [in Smallstep]
cmin_minimal [in Equiv]
Combined.combined_strong_progress [in Smallstep]
Combined.combined_step_deterministic [in Smallstep]
compiler_is_correct [in Smallstep]
congruence_demo_3 [in UseAuto]
congruence_demo_4 [in UseAuto]
congruence_demo_2 [in UseAuto]
congruence_demo_1 [in UseAuto]
context_invariance [in Norm]
CSeq_congruence [in Equiv]
CWhile_congruence [in Equiv]
c3_c4_different [in Equiv]
D
dec_while_correct [in Hoare2]demo_false [in UseAuto]
demo_auto_absurd_2 [in UseAuto]
demo_auto_absurd_1 [in UseAuto]
demo_hint_unfold_context_2 [in UseAuto]
demo_hint_unfold_context_1 [in UseAuto]
demo_hint_unfold_goal_2 [in UseAuto]
demo_hint_unfold_goal_1 [in UseAuto]
demo_tryfalse [in UseTactics]
demo_false_arg [in UseTactics]
demo_false [in UseTactics]
demo_clears_all_and_clears_but [in LibTactics]
DeterministicImp.ceval_deterministic'''' [in UseAuto]
DeterministicImp.ceval_deterministic''' [in UseAuto]
DeterministicImp.ceval_deterministic'' [in UseAuto]
DeterministicImp.ceval_deterministic' [in UseAuto]
DeterministicImp.ceval_deterministic [in UseAuto]
dfib_correct [in Hoare2]
div_mod_outer_triple_valid [in Hoare2]
dpow2_down_correct [in Hoare2]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]
E
EqualityExamples.demo_applys_eq_2 [in UseTactics]EqualityExamples.demo_applys_eq_1 [in UseTactics]
EqualityExamples.demo_fequals [in UseTactics]
EqualityExamples.demo_substs [in UseTactics]
EqualityExamples.mult_0_plus'' [in UseTactics]
EqualityExamples.mult_0_plus [in UseTactics]
equality_by_auto [in UseAuto]
equates_6 [in LibTactics]
equates_5 [in LibTactics]
equates_4 [in LibTactics]
equates_3 [in LibTactics]
equates_2 [in LibTactics]
equates_1 [in LibTactics]
equates_0 [in LibTactics]
evalF_eval [in Smallstep]
eval__multistep [in Smallstep]
eval_assign [in PE]
ExamplesLets.demo_lets_underscore [in UseTactics]
ExamplesLets.demo_lets_5 [in UseTactics]
ExamplesLets.demo_lets_4 [in UseTactics]
ExamplesLets.demo_lets_3 [in UseTactics]
ExamplesLets.demo_lets_2 [in UseTactics]
ExamplesLets.demo_lets_1 [in UseTactics]
F
factorial_correct [in Hoare2]false_eqb_string [in Norm]
false_eqb_string [in PE]
fib_eqn [in Hoare2]
fold_constants_com_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_aexp_sound [in Equiv]
free_in_context [in Norm]
G
GenExample.substitution_preserves_typing [in UseTactics]H
Himp.havoc_post [in Hoare]Himp.hoare_havoc [in Hoare]
Himp.hoare_consequence_pre [in Hoare]
Himp.ptwice_cequiv_pcopy [in Equiv]
Himp.pXY_cequiv_pYX [in Equiv]
Himp.p1_p2_equiv [in Equiv]
Himp.p1_may_diverge [in Equiv]
Himp.p2_may_diverge [in Equiv]
Himp.p3_p4_inequiv [in Equiv]
Himp.p5_p6_equiv [in Equiv]
Himp2.hoare_havoc_weakest [in Hoare2]
HoareAssertAssume.assert_implies_assume [in Hoare]
HoareAssertAssume.assert_assume_differ [in Hoare]
HoareAssertAssume.hoare_while [in Hoare]
HoareAssertAssume.hoare_if [in Hoare]
HoareAssertAssume.hoare_skip [in Hoare]
HoareAssertAssume.hoare_seq [in Hoare]
HoareAssertAssume.hoare_consequence_post [in Hoare]
HoareAssertAssume.hoare_consequence_pre [in Hoare]
HoareAssertAssume.hoare_asgn [in Hoare]
hoare_while [in Hoare]
hoare_if [in Hoare]
hoare_consequence_post' [in Hoare]
hoare_consequence_pre'''' [in Hoare]
hoare_consequence_pre''' [in Hoare]
hoare_consequence_pre'' [in Hoare]
hoare_consequence_pre' [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_asgn_fwd_exists [in Hoare]
hoare_asgn_fwd [in Hoare]
hoare_asgn [in Hoare]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_pre_false [in Hoare]
hoare_post_true [in Hoare]
hoare_asgn_weakest [in Hoare2]
hoare_complete [in HoareAsLogic]
hoare_sound [in HoareAsLogic]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]
I
identity_assignment [in Equiv]iff_intro_swap [in LibTactics]
if_minus_plus [in Hoare]
if_minus_plus_correct [in Hoare2]
if_false [in Equiv]
if_true [in Equiv]
if_true_simple [in Equiv]
If1.hoare_if1_good [in Hoare]
If1.hoare_asgn [in Hoare]
If1.hoare_consequence_pre [in Hoare]
inbP [in PE]
induct_height_max2 [in LibTactics]
inequiv_exercise [in Equiv]
instantiation_drop [in Norm]
instantiation_R [in Norm]
instantiation_env_closed [in Norm]
instantiation_domains_match [in Norm]
IntrovExamples.ceval_deterministic' [in UseTactics]
IntrovExamples.ceval_deterministic [in UseTactics]
IntrovExamples.dist_exists_or [in UseTactics]
IntrovExamples.exists_impl [in UseTactics]
invalid_triple [in Hoare]
InvertsExamples.ceval_deterministic' [in UseTactics]
InvertsExamples.ceval_deterministic [in UseTactics]
InvertsExamples.skip_left' [in UseTactics]
InvertsExamples.skip_left [in UseTactics]
is_wp_example [in Hoare2]
L
lia_demo_4 [in UseAuto]lia_demo_3 [in UseAuto]
lia_demo_2 [in UseAuto]
lia_demo_1 [in UseAuto]
loop_unrolling [in Equiv]
Loop.ceval_count_sound [in PE]
Loop.ceval_count_complete [in PE]
Loop.pe_com_correct [in PE]
Loop.pe_com_sound [in PE]
Loop.pe_com_complete [in PE]
Loop.pe_ceval_count_le [in PE]
Loop.pe_compare_nil_update [in PE]
Loop.pe_compare_nil_lookup [in PE]
ltac_something_show [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_database_provide [in LibTactics]
M
minimum_correct [in Hoare2]msubst_R [in Norm]
msubst_preserves_typing [in Norm]
msubst_app [in Norm]
msubst_abs [in Norm]
msubst_var [in Norm]
msubst_closed [in Norm]
multistep__eval [in Smallstep]
multistep_congr_2 [in Smallstep]
multistep_congr_1 [in Smallstep]
multistep_App2 [in Norm]
multistep_preserves_R' [in Norm]
multistep_preserves_R [in Norm]
multi_trans [in Smallstep]
multi_R [in Smallstep]
mupdate_drop [in Norm]
mupdate_lookup [in Norm]
N
NaryExamples.demo_branch [in UseTactics]NaryExamples.demo_splits [in UseTactics]
nat_le_refl [in UseAuto]
negation_study_2 [in UseAuto]
negation_study_1 [in UseAuto]
nf_same_as_value [in Smallstep]
nf_is_value [in Smallstep]
normalization [in Norm]
normalize_ex' [in Smallstep]
normalize_ex [in Smallstep]
normal_forms_unique [in Smallstep]
O
optimizer_sound [in Equiv]optimize_0plus_com_sound [in Equiv]
optimize_0plus_bexp_sound [in Equiv]
optimize_0plus_aexp_sound [in Equiv]
order_matters_2 [in UseAuto]
order_matters_1 [in UseAuto]
P
parity_outer_triple_valid [in Hoare2]parity_lt_2 [in Hoare2]
parity_ge_2 [in Hoare2]
pe_program_correct [in PE]
pe_block_correct [in PE]
pe_com_correct [in PE]
pe_com_sound [in PE]
pe_com_complete [in PE]
pe_compare_update [in PE]
pe_compare_removes [in PE]
pe_removes_correct [in PE]
pe_compare_correct [in PE]
pe_unique_correct [in PE]
pe_disagree_domain [in PE]
pe_update_update_add [in PE]
pe_update_update_remove [in PE]
pe_add_correct [in PE]
pe_remove_correct [in PE]
pe_bexp_correct [in PE]
pe_aexp_correct [in PE]
pe_consistent_update [in PE]
pe_update_consistent [in PE]
pe_update_correct [in PE]
pe_aexp_correct_weak [in PE]
pe_domain [in PE]
positive_difference_correct [in Hoare2]
pow2_le_1 [in Hoare2]
pow2_plus_1 [in Hoare2]
preservation [in Norm]
PreservationProgressReferences.nth_eq_last' [in UseAuto]
PreservationProgressReferences.preservation [in UseAuto]
PreservationProgressReferences.preservation_ref [in UseAuto]
PreservationProgressReferences.preservation' [in UseAuto]
PreservationProgressReferences.progress [in UseAuto]
PreservationProgressStlc.preservation [in UseAuto]
PreservationProgressStlc.preservation' [in UseAuto]
PreservationProgressStlc.progress [in UseAuto]
PreservationProgressStlc.progress' [in UseAuto]
provable_false_pre [in HoareAsLogic]
provable_true_post [in HoareAsLogic]
R
RecordSub.abs_arrow [in RecordSub]RecordSub.canonical_forms_of_arrow_types [in RecordSub]
RecordSub.has_type__wf [in RecordSub]
RecordSub.lookup_field_in_value [in RecordSub]
RecordSub.preservation [in RecordSub]
RecordSub.progress [in RecordSub]
RecordSub.rcd_types_match [in RecordSub]
RecordSub.step_preserves_record_tm [in RecordSub]
RecordSub.substitution_preserves_typing [in RecordSub]
RecordSub.subtype__wf [in RecordSub]
RecordSub.sub_inversion_arrow [in RecordSub]
RecordSub.typing_inversion_abs [in RecordSub]
RecordSub.weakening [in RecordSub]
RecordSub.weakening_empty [in RecordSub]
RecordSub.wf_rcd_lookup [in RecordSub]
reduce_to_zero_correct''' [in Hoare2]
reduce_to_zero_correct' [in Hoare2]
refl_cequiv [in Equiv]
refl_bequiv [in Equiv]
refl_aequiv [in Equiv]
RepeatExercise.ex1_repeat_works [in Hoare]
RingDemo.ring_demo [in UseAuto]
R_typable_empty [in Norm]
R_halts [in Norm]
S
search_depth_5 [in UseAuto]search_depth_4 [in UseAuto]
search_depth_3 [in UseAuto]
search_depth_1 [in UseAuto]
search_depth_0 [in UseAuto]
Semantics.multistep__eval'' [in UseAuto]
Semantics.multistep__eval' [in UseAuto]
Semantics.multistep_eval_ind [in UseAuto]
Semantics.multistep__eval [in UseAuto]
seq_assoc [in Equiv]
SimpleArith2.step_deterministic [in Smallstep]
SimpleArith3.step_deterministic_alt [in Smallstep]
SkipExample.ceval_deterministic [in UseTactics]
SkipExample.demo_admits [in UseTactics]
SkipExample.mult_plus_0 [in UseTactics]
skip_right [in Equiv]
skip_left [in Equiv]
slow_assignment [in Hoare2]
solved_by_jauto [in UseAuto]
solving_by_symmetry [in UseAuto]
solving_exists_hyp [in UseAuto]
solving_exists_goal [in UseAuto]
solving_tauto [in UseAuto]
solving_disj_hyp [in UseAuto]
solving_disj_goal [in UseAuto]
solving_conj_hyp_forall [in UseAuto]
solving_conj_more [in UseAuto]
solving_conj_hyp' [in UseAuto]
solving_conj_hyp [in UseAuto]
solving_conj_goal [in UseAuto]
solving_by_eapply [in UseAuto]
solving_by_apply [in UseAuto]
solving_by_reflexivity [in UseAuto]
SortExamples.ceval_deterministic [in UseTactics]
sqrt_correct [in Hoare2]
stack_step_deterministic [in Smallstep]
StepFunction.complete_stepf [in Typechecking]
StepFunction.complete_valuef [in Typechecking]
StepFunction.sound_stepf [in Typechecking]
StepFunction.sound_valuef [in Typechecking]
StepFunction.value_stepf_nf [in Typechecking]
step__eval [in Smallstep]
step_normalizing [in Smallstep]
step_deterministic [in Smallstep]
step_preserves_R' [in Norm]
step_preserves_R [in Norm]
step_preserves_halting [in Norm]
step_deterministic [in Norm]
STLCArith.preservation [in StlcProp]
STLCArith.progress [in StlcProp]
STLCArith.weakening [in StlcProp]
STLCChecker.type_checking_complete [in Typechecking]
STLCChecker.type_checking_sound [in Typechecking]
STLCExtendedRecords.has_type__wf [in Records]
STLCExtendedRecords.lookup_field_in_value [in Records]
STLCExtendedRecords.preservation [in Records]
STLCExtendedRecords.progress [in Records]
STLCExtendedRecords.step_preserves_record_tm [in Records]
STLCExtendedRecords.substitution_preserves_typing [in Records]
STLCExtendedRecords.typing_example_2 [in Records]
STLCExtendedRecords.weakening [in Records]
STLCExtendedRecords.weakening_empty [in Records]
STLCExtendedRecords.wf_rcd_lookup [in Records]
STLCExtended.preservation [in MoreStlc]
STLCExtended.progress [in MoreStlc]
STLCExtended.substitution_preserves_typing [in MoreStlc]
STLCExtended.weakening [in MoreStlc]
STLCExtended.weakening_empty [in MoreStlc]
STLCProp.canonical_forms_fun [in StlcProp]
STLCProp.canonical_forms_bool [in StlcProp]
STLCProp.context_invariance [in StlcProp]
STLCProp.free_in_context [in StlcProp]
STLCProp.not_subject_expansion [in StlcProp]
STLCProp.preservation [in StlcProp]
STLCProp.progress [in StlcProp]
STLCProp.progress' [in StlcProp]
STLCProp.substitution_preserves_typing_from_typing_ind [in StlcProp]
STLCProp.substitution_preserves_typing [in StlcProp]
STLCProp.typable_empty__closed [in StlcProp]
STLCProp.type_soundness [in StlcProp]
STLCProp.unique_types [in StlcProp]
STLCProp.weakening [in StlcProp]
STLCProp.weakening_empty [in StlcProp]
STLCRef.assign_pres_store_typing [in References]
STLCRef.cyclic_store [in References]
STLCRef.extends_refl [in References]
STLCRef.extends_app [in References]
STLCRef.extends_lookup [in References]
STLCRef.length_extends [in References]
STLCRef.length_replace [in References]
STLCRef.lookup_replace_neq [in References]
STLCRef.lookup_replace_eq [in References]
STLCRef.nth_eq_last [in References]
STLCRef.preservation [in References]
STLCRef.preservation_wrong2 [in References]
STLCRef.preservation_wrong1 [in References]
STLCRef.progress [in References]
STLCRef.RefsAndNontermination.factorial_type [in References]
STLCRef.RefsAndNontermination.loop_fun_step_self [in References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [in References]
STLCRef.RefsAndNontermination.loop_typeable [in References]
STLCRef.replace_nil [in References]
STLCRef.store_well_typed_app [in References]
STLCRef.store_weakening [in References]
STLCRef.store_not_unique [in References]
STLCRef.substitution_preserves_typing [in References]
STLCRef.weakening [in References]
STLCRef.weakening_empty [in References]
STLCSub.abs_arrow [in Sub]
STLCSub.canonical_forms_of_Bool [in Sub]
STLCSub.canonical_forms_of_arrow_types [in Sub]
STLCSub.FormalThoughtExercises.formal_smallest_2 [in Sub]
STLCSub.FormalThoughtExercises.formal_smallest_1 [in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_4 [in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_3 [in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_2 [in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_1 [in Sub]
STLCSub.FormalThoughtExercises.formal_proper_subtypes [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfh [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfg [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tff [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfe [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfd [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfc [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfb [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfa [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2e [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2d [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2b [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2a [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1g [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1f [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1e [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1d [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1c [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1b [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1a [in Sub]
STLCSub.preservation [in Sub]
STLCSub.progress [in Sub]
STLCSub.substitution_preserves_typing [in Sub]
STLCSub.sub_inversion_Top [in Sub]
STLCSub.sub_inversion_Base [in Sub]
STLCSub.sub_inversion_Unit [in Sub]
STLCSub.sub_inversion_arrow [in Sub]
STLCSub.sub_inversion_Bool [in Sub]
STLCSub.typing_inversion_unit [in Sub]
STLCSub.typing_inversion_app [in Sub]
STLCSub.typing_inversion_var [in Sub]
STLCSub.typing_inversion_abs [in Sub]
STLCSub.weakening [in Sub]
STLCSub.weakening_empty [in Sub]
STLCTypes.eqb_ty__eq [in Typechecking]
STLCTypes.eqb_ty_refl [in Typechecking]
STLC.step_example5_with_normalize [in Stlc]
STLC.step_example5 [in Stlc]
STLC.step_example4' [in Stlc]
STLC.step_example3' [in Stlc]
STLC.step_example2' [in Stlc]
STLC.step_example1' [in Stlc]
STLC.step_example4 [in Stlc]
STLC.step_example3 [in Stlc]
STLC.step_example2 [in Stlc]
STLC.step_example1 [in Stlc]
STLC.substi_correct [in Stlc]
strong_progress [in Smallstep]
substitution_preserves_typing [in Norm]
subst_inequiv [in Equiv]
subst_msubst [in Norm]
subst_not_afi [in Norm]
subst_closed [in Norm]
subtract_slowly_outer_triple_valid [in Hoare2]
SubtypingInversion.abs_arrow' [in UseAuto]
SubtypingInversion.abs_arrow [in UseAuto]
swap_exercise [in Hoare]
swap_correct [in Hoare2]
swap_noninterfering_assignments [in Equiv]
swap_if_branches [in Equiv]
swap_subst [in Norm]
sym_cequiv [in Equiv]
sym_bequiv [in Equiv]
sym_aequiv [in Equiv]
T
Temp1.value_not_same_as_normal_form [in Smallstep]Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.step_deterministic [in Smallstep]
Temp4.strong_progress_bool [in Smallstep]
test_multistep_4 [in Smallstep]
test_multistep_3 [in Smallstep]
test_multistep_2 [in Smallstep]
test_multistep_1' [in Smallstep]
test_multistep_1 [in Smallstep]
TM.bool_canonical [in Types]
TM.nat_canonical [in Types]
TM.preservation [in Types]
TM.preservation' [in Types]
TM.progress [in Types]
TM.soundness [in Types]
TM.step_deterministic [in Types]
TM.subject_expansion [in Types]
TM.value_is_nf [in Types]
transitivity_workaround_2 [in UseAuto]
transitivity_workaround_1 [in UseAuto]
transitivity_bad_hint_1 [in UseAuto]
trans_cequiv [in Equiv]
trans_bequiv [in Equiv]
trans_aequiv [in Equiv]
two_loops [in Hoare2]
typable_empty__closed [in Norm]
TypecheckerExtensions.eqb_ty__eq [in Typechecking]
TypecheckerExtensions.eqb_ty_refl [in Typechecking]
TypecheckerExtensions.type_checking_complete [in Typechecking]
TypecheckerExtensions.type_checking_sound [in Typechecking]
U
UnfoldsExample.bexp_eval_true [in UseTactics]V
vacuous_substitution [in Norm]value_is_nf [in Smallstep]
value_halts [in Norm]
value__normal [in Norm]
verification_correct_dec [in Hoare2]
verification_correct [in Hoare2]
W
weakening [in Norm]weakening_empty [in Norm]
while_true [in Equiv]
while_true_nonterm [in Equiv]
while_false [in Equiv]
working_of_auto_2 [in UseAuto]
working_of_auto_1 [in UseAuto]
wp_invariant [in HoareAsLogic]
wp_seq [in HoareAsLogic]
wp_is_weakest [in HoareAsLogic]
wp_is_precondition [in HoareAsLogic]
Z
zprop_preserving [in Equiv]Constructor Index
A
afi_snd [in Norm]afi_fst [in Norm]
afi_pair2 [in Norm]
afi_pair1 [in Norm]
afi_test2 [in Norm]
afi_test1 [in Norm]
afi_test0 [in Norm]
afi_abs [in Norm]
afi_app2 [in Norm]
afi_app1 [in Norm]
afi_var [in Norm]
Assign [in PE]
AS_Mult [in Smallstep]
AS_Mult2 [in Smallstep]
AS_Mult1 [in Smallstep]
AS_Minus [in Smallstep]
AS_Minus2 [in Smallstep]
AS_Minus1 [in Smallstep]
AS_Plus [in Smallstep]
AS_Plus2 [in Smallstep]
AS_Plus1 [in Smallstep]
AS_Id [in Smallstep]
av_num [in Smallstep]
B
body [in PE]boxer [in LibTactics]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_AndFalse [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndStep [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotTrue [in Smallstep]
BS_NotStep [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq2 [in Smallstep]
BS_Eq1 [in Smallstep]
C
C [in Smallstep]CImp.CAsgn [in Smallstep]
CImp.CIf [in Smallstep]
CImp.CPar [in Smallstep]
CImp.CSeq [in Smallstep]
CImp.CSkip [in Smallstep]
CImp.CS_ParDone [in Smallstep]
CImp.CS_Par2 [in Smallstep]
CImp.CS_Par1 [in Smallstep]
CImp.CS_While [in Smallstep]
CImp.CS_IfFalse [in Smallstep]
CImp.CS_IfTrue [in Smallstep]
CImp.CS_IfStep [in Smallstep]
CImp.CS_SeqFinish [in Smallstep]
CImp.CS_SeqStep [in Smallstep]
CImp.CS_Asgn [in Smallstep]
CImp.CS_AsgnStep [in Smallstep]
CImp.CWhile [in Smallstep]
Combined.C [in Smallstep]
Combined.fls [in Smallstep]
Combined.P [in Smallstep]
Combined.ST_If [in Smallstep]
Combined.ST_IfFalse [in Smallstep]
Combined.ST_IfTrue [in Smallstep]
Combined.ST_Plus2 [in Smallstep]
Combined.ST_Plus1 [in Smallstep]
Combined.ST_PlusConstConst [in Smallstep]
Combined.test [in Smallstep]
Combined.tru [in Smallstep]
Combined.v_fls [in Smallstep]
Combined.v_tru [in Smallstep]
Combined.v_const [in Smallstep]
CS_While [in Smallstep]
CS_IfFalse [in Smallstep]
CS_IfTrue [in Smallstep]
CS_IfStep [in Smallstep]
CS_SeqFinish [in Smallstep]
CS_SeqStep [in Smallstep]
CS_Asgn [in Smallstep]
CS_AsgnStep [in Smallstep]
D
DCAsgn [in Hoare2]DCIf [in Hoare2]
DCPost [in Hoare2]
DCPre [in Hoare2]
DCSeq [in Hoare2]
DCSkip [in Hoare2]
DCWhile [in Hoare2]
Decorated [in Hoare2]
done [in PE]
E
entry [in PE]E_Plus [in Smallstep]
E_Const [in Smallstep]
E_Some [in PE]
E_None [in PE]
G
Goto [in PE]H
Himp.CAsgn [in Hoare]Himp.CAsgn [in Equiv]
Himp.CHavoc [in Hoare]
Himp.CHavoc [in Equiv]
Himp.CIf [in Hoare]
Himp.CIf [in Equiv]
Himp.CSeq [in Hoare]
Himp.CSeq [in Equiv]
Himp.CSkip [in Hoare]
Himp.CSkip [in Equiv]
Himp.CWhile [in Hoare]
Himp.CWhile [in Equiv]
Himp.E_Havoc [in Hoare]
Himp.E_WhileTrue [in Hoare]
Himp.E_WhileFalse [in Hoare]
Himp.E_IfFalse [in Hoare]
Himp.E_IfTrue [in Hoare]
Himp.E_Seq [in Hoare]
Himp.E_Asgn [in Hoare]
Himp.E_Skip [in Hoare]
Himp.E_WhileTrue [in Equiv]
Himp.E_WhileFalse [in Equiv]
Himp.E_IfFalse [in Equiv]
Himp.E_IfTrue [in Equiv]
Himp.E_Seq [in Equiv]
Himp.E_Asgn [in Equiv]
Himp.E_Skip [in Equiv]
HoareAssertAssume.CAsgn [in Hoare]
HoareAssertAssume.CAssert [in Hoare]
HoareAssertAssume.CAssume [in Hoare]
HoareAssertAssume.CIf [in Hoare]
HoareAssertAssume.CSeq [in Hoare]
HoareAssertAssume.CSkip [in Hoare]
HoareAssertAssume.CWhile [in Hoare]
HoareAssertAssume.E_Assume [in Hoare]
HoareAssertAssume.E_AssertFalse [in Hoare]
HoareAssertAssume.E_AssertTrue [in Hoare]
HoareAssertAssume.E_WhileTrueError [in Hoare]
HoareAssertAssume.E_WhileTrueNormal [in Hoare]
HoareAssertAssume.E_WhileFalse [in Hoare]
HoareAssertAssume.E_IfFalse [in Hoare]
HoareAssertAssume.E_IfTrue [in Hoare]
HoareAssertAssume.E_SeqError [in Hoare]
HoareAssertAssume.E_SeqNormal [in Hoare]
HoareAssertAssume.E_Asgn [in Hoare]
HoareAssertAssume.E_Skip [in Hoare]
HoareAssertAssume.RError [in Hoare]
HoareAssertAssume.RNormal [in Hoare]
H_Consequence [in HoareAsLogic]
H_While [in HoareAsLogic]
H_If [in HoareAsLogic]
H_Seq [in HoareAsLogic]
H_Asgn [in HoareAsLogic]
H_Skip [in HoareAsLogic]
I
If [in PE]If1.CAsgn [in Hoare]
If1.CIf [in Hoare]
If1.CIf1 [in Hoare]
If1.CSeq [in Hoare]
If1.CSkip [in Hoare]
If1.CWhile [in Hoare]
If1.E_WhileTrue [in Hoare]
If1.E_WhileFalse [in Hoare]
If1.E_IfFalse [in Hoare]
If1.E_IfTrue [in Hoare]
If1.E_Seq [in Hoare]
If1.E_Asgn [in Hoare]
If1.E_Skip [in Hoare]
L
loop [in PE]Loop.E'Asgn [in PE]
Loop.E'IfFalse [in PE]
Loop.E'IfTrue [in PE]
Loop.E'Seq [in PE]
Loop.E'Skip [in PE]
Loop.E'WhileFalse [in PE]
Loop.E'WhileTrue [in PE]
Loop.pe_ceval_count_intro [in PE]
Loop.PE_WhileFixed [in PE]
Loop.PE_WhileFixedLoop [in PE]
Loop.PE_WhileFixedEnd [in PE]
Loop.PE_While [in PE]
Loop.PE_WhileTrue [in PE]
Loop.PE_WhileFalse [in PE]
Loop.PE_If [in PE]
Loop.PE_IfFalse [in PE]
Loop.PE_IfTrue [in PE]
Loop.PE_Seq [in PE]
Loop.PE_AsgnDynamic [in PE]
Loop.PE_AsgnStatic [in PE]
Loop.PE_Skip [in PE]
ltac_goal_to_discard_intro [in LibTactics]
ltac_database_token [in LibTactics]
ltac_mark [in LibTactics]
ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]
M
multi_step [in Smallstep]multi_refl [in Smallstep]
P
P [in Smallstep]pe_peval_intro [in PE]
pe_ceval_intro [in PE]
PE_If [in PE]
PE_IfFalse [in PE]
PE_IfTrue [in PE]
PE_Seq [in PE]
PE_AsgnDynamic [in PE]
PE_AsgnStatic [in PE]
PE_Skip [in PE]
R
RecordSub.rtcons [in RecordSub]RecordSub.RTcons [in RecordSub]
RecordSub.rtnil [in RecordSub]
RecordSub.RTnil [in RecordSub]
RecordSub.ST_Rcd_Tail [in RecordSub]
RecordSub.ST_Rcd_Head [in RecordSub]
RecordSub.ST_ProjRcd [in RecordSub]
RecordSub.ST_Proj1 [in RecordSub]
RecordSub.ST_App2 [in RecordSub]
RecordSub.ST_App1 [in RecordSub]
RecordSub.ST_AppAbs [in RecordSub]
RecordSub.S_RcdPerm [in RecordSub]
RecordSub.S_RcdDepth [in RecordSub]
RecordSub.S_RcdWidth [in RecordSub]
RecordSub.S_Arrow [in RecordSub]
RecordSub.S_Top [in RecordSub]
RecordSub.S_Trans [in RecordSub]
RecordSub.S_Refl [in RecordSub]
RecordSub.tm_rcons [in RecordSub]
RecordSub.tm_rnil [in RecordSub]
RecordSub.tm_rproj [in RecordSub]
RecordSub.tm_abs [in RecordSub]
RecordSub.tm_app [in RecordSub]
RecordSub.tm_var [in RecordSub]
RecordSub.Ty_RCons [in RecordSub]
RecordSub.Ty_RNil [in RecordSub]
RecordSub.Ty_Arrow [in RecordSub]
RecordSub.Ty_Base [in RecordSub]
RecordSub.Ty_Top [in RecordSub]
RecordSub.T_RCons [in RecordSub]
RecordSub.T_RNil [in RecordSub]
RecordSub.T_Sub [in RecordSub]
RecordSub.T_Proj [in RecordSub]
RecordSub.T_App [in RecordSub]
RecordSub.T_Abs [in RecordSub]
RecordSub.T_Var [in RecordSub]
RecordSub.v_rcons [in RecordSub]
RecordSub.v_rnil [in RecordSub]
RecordSub.v_abs [in RecordSub]
RecordSub.wfArrow [in RecordSub]
RecordSub.wfBase [in RecordSub]
RecordSub.wfRCons [in RecordSub]
RecordSub.wfRNil [in RecordSub]
RecordSub.wfTop [in RecordSub]
RepeatExercise.CAsgn [in Hoare]
RepeatExercise.CIf [in Hoare]
RepeatExercise.CRepeat [in Hoare]
RepeatExercise.CSeq [in Hoare]
RepeatExercise.CSkip [in Hoare]
RepeatExercise.CWhile [in Hoare]
RepeatExercise.E_WhileTrue [in Hoare]
RepeatExercise.E_WhileFalse [in Hoare]
RepeatExercise.E_IfFalse [in Hoare]
RepeatExercise.E_IfTrue [in Hoare]
RepeatExercise.E_Seq [in Hoare]
RepeatExercise.E_Asgn [in Hoare]
RepeatExercise.E_Skip [in Hoare]
S
SimpleArith1.ST_Plus2 [in Smallstep]SimpleArith1.ST_Plus1 [in Smallstep]
SimpleArith1.ST_PlusConstConst [in Smallstep]
SS_Mult [in Smallstep]
SS_Minus [in Smallstep]
SS_Plus [in Smallstep]
SS_Load [in Smallstep]
SS_Push [in Smallstep]
STLCArith.tm_if0 [in StlcProp]
STLCArith.tm_mult [in StlcProp]
STLCArith.tm_pred [in StlcProp]
STLCArith.tm_succ [in StlcProp]
STLCArith.tm_const [in StlcProp]
STLCArith.tm_abs [in StlcProp]
STLCArith.tm_app [in StlcProp]
STLCArith.tm_var [in StlcProp]
STLCArith.Ty_Nat [in StlcProp]
STLCArith.Ty_Arrow [in StlcProp]
STLCExtendedRecords.FirstTry.Arrow [in Records]
STLCExtendedRecords.FirstTry.Base [in Records]
STLCExtendedRecords.FirstTry.TRcd [in Records]
STLCExtendedRecords.rtcons [in Records]
STLCExtendedRecords.RTcons [in Records]
STLCExtendedRecords.rtnil [in Records]
STLCExtendedRecords.RTnil [in Records]
STLCExtendedRecords.ST_Rcd_Tail [in Records]
STLCExtendedRecords.ST_Rcd_Head [in Records]
STLCExtendedRecords.ST_ProjRcd [in Records]
STLCExtendedRecords.ST_Proj1 [in Records]
STLCExtendedRecords.ST_App2 [in Records]
STLCExtendedRecords.ST_App1 [in Records]
STLCExtendedRecords.ST_AppAbs [in Records]
STLCExtendedRecords.tm_rcons [in Records]
STLCExtendedRecords.tm_rnil [in Records]
STLCExtendedRecords.tm_rproj [in Records]
STLCExtendedRecords.tm_abs [in Records]
STLCExtendedRecords.tm_app [in Records]
STLCExtendedRecords.tm_var [in Records]
STLCExtendedRecords.Ty_RCons [in Records]
STLCExtendedRecords.Ty_RNil [in Records]
STLCExtendedRecords.Ty_Arrow [in Records]
STLCExtendedRecords.Ty_Base [in Records]
STLCExtendedRecords.T_RCons [in Records]
STLCExtendedRecords.T_RNil [in Records]
STLCExtendedRecords.T_Proj [in Records]
STLCExtendedRecords.T_App [in Records]
STLCExtendedRecords.T_Abs [in Records]
STLCExtendedRecords.T_Var [in Records]
STLCExtendedRecords.v_rcons [in Records]
STLCExtendedRecords.v_rnil [in Records]
STLCExtendedRecords.v_abs [in Records]
STLCExtendedRecords.wfArrow [in Records]
STLCExtendedRecords.wfBase [in Records]
STLCExtendedRecords.wfRCons [in Records]
STLCExtendedRecords.wfRNil [in Records]
STLCExtended.ST_LcaseCons [in MoreStlc]
STLCExtended.ST_LcaseNil [in MoreStlc]
STLCExtended.ST_Lcase1 [in MoreStlc]
STLCExtended.ST_Cons2 [in MoreStlc]
STLCExtended.ST_Cons1 [in MoreStlc]
STLCExtended.ST_CaseInr [in MoreStlc]
STLCExtended.ST_CaseInl [in MoreStlc]
STLCExtended.ST_Case [in MoreStlc]
STLCExtended.ST_Inr [in MoreStlc]
STLCExtended.ST_Inl [in MoreStlc]
STLCExtended.ST_If0_Nonzero [in MoreStlc]
STLCExtended.ST_If0_Zero [in MoreStlc]
STLCExtended.ST_If0 [in MoreStlc]
STLCExtended.ST_Mult2 [in MoreStlc]
STLCExtended.ST_Mult1 [in MoreStlc]
STLCExtended.ST_Mulconsts [in MoreStlc]
STLCExtended.ST_PredNat [in MoreStlc]
STLCExtended.ST_Pred [in MoreStlc]
STLCExtended.ST_SuccNat [in MoreStlc]
STLCExtended.ST_Succ [in MoreStlc]
STLCExtended.ST_App2 [in MoreStlc]
STLCExtended.ST_App1 [in MoreStlc]
STLCExtended.ST_AppAbs [in MoreStlc]
STLCExtended.tm_fix [in MoreStlc]
STLCExtended.tm_let [in MoreStlc]
STLCExtended.tm_snd [in MoreStlc]
STLCExtended.tm_fst [in MoreStlc]
STLCExtended.tm_pair [in MoreStlc]
STLCExtended.tm_unit [in MoreStlc]
STLCExtended.tm_lcase [in MoreStlc]
STLCExtended.tm_cons [in MoreStlc]
STLCExtended.tm_nil [in MoreStlc]
STLCExtended.tm_case [in MoreStlc]
STLCExtended.tm_inr [in MoreStlc]
STLCExtended.tm_inl [in MoreStlc]
STLCExtended.tm_if0 [in MoreStlc]
STLCExtended.tm_mult [in MoreStlc]
STLCExtended.tm_pred [in MoreStlc]
STLCExtended.tm_succ [in MoreStlc]
STLCExtended.tm_const [in MoreStlc]
STLCExtended.tm_abs [in MoreStlc]
STLCExtended.tm_app [in MoreStlc]
STLCExtended.tm_var [in MoreStlc]
STLCExtended.Ty_Prod [in MoreStlc]
STLCExtended.Ty_Unit [in MoreStlc]
STLCExtended.Ty_List [in MoreStlc]
STLCExtended.Ty_Sum [in MoreStlc]
STLCExtended.Ty_Nat [in MoreStlc]
STLCExtended.Ty_Arrow [in MoreStlc]
STLCExtended.T_Unit [in MoreStlc]
STLCExtended.T_Lcase [in MoreStlc]
STLCExtended.T_Cons [in MoreStlc]
STLCExtended.T_Nil [in MoreStlc]
STLCExtended.T_Case [in MoreStlc]
STLCExtended.T_Inr [in MoreStlc]
STLCExtended.T_Inl [in MoreStlc]
STLCExtended.T_If0 [in MoreStlc]
STLCExtended.T_Mult [in MoreStlc]
STLCExtended.T_Pred [in MoreStlc]
STLCExtended.T_Succ [in MoreStlc]
STLCExtended.T_Nat [in MoreStlc]
STLCExtended.T_App [in MoreStlc]
STLCExtended.T_Abs [in MoreStlc]
STLCExtended.T_Var [in MoreStlc]
STLCExtended.v_pair [in MoreStlc]
STLCExtended.v_unit [in MoreStlc]
STLCExtended.v_lcons [in MoreStlc]
STLCExtended.v_lnil [in MoreStlc]
STLCExtended.v_inr [in MoreStlc]
STLCExtended.v_inl [in MoreStlc]
STLCExtended.v_nat [in MoreStlc]
STLCExtended.v_abs [in MoreStlc]
STLCProp.afi_if3 [in StlcProp]
STLCProp.afi_if2 [in StlcProp]
STLCProp.afi_if1 [in StlcProp]
STLCProp.afi_abs [in StlcProp]
STLCProp.afi_app2 [in StlcProp]
STLCProp.afi_app1 [in StlcProp]
STLCProp.afi_var [in StlcProp]
STLCRef.extends_cons [in References]
STLCRef.extends_nil [in References]
STLCRef.RefsAndNontermination.sc_step [in References]
STLCRef.RefsAndNontermination.sc_one [in References]
STLCRef.ST_Assign2 [in References]
STLCRef.ST_Assign1 [in References]
STLCRef.ST_Assign [in References]
STLCRef.ST_Deref [in References]
STLCRef.ST_DerefLoc [in References]
STLCRef.ST_Ref [in References]
STLCRef.ST_RefValue [in References]
STLCRef.ST_If0_Nonzero [in References]
STLCRef.ST_If0_Zero [in References]
STLCRef.ST_If0 [in References]
STLCRef.ST_Mult2 [in References]
STLCRef.ST_Mult1 [in References]
STLCRef.ST_MultNats [in References]
STLCRef.ST_Pred [in References]
STLCRef.ST_PredNat [in References]
STLCRef.ST_Succ [in References]
STLCRef.ST_SuccNat [in References]
STLCRef.ST_App2 [in References]
STLCRef.ST_App1 [in References]
STLCRef.ST_AppAbs [in References]
STLCRef.tm_loc [in References]
STLCRef.tm_assign [in References]
STLCRef.tm_deref [in References]
STLCRef.tm_ref [in References]
STLCRef.tm_unit [in References]
STLCRef.tm_if0 [in References]
STLCRef.tm_mult [in References]
STLCRef.tm_pred [in References]
STLCRef.tm_succ [in References]
STLCRef.tm_const [in References]
STLCRef.tm_abs [in References]
STLCRef.tm_app [in References]
STLCRef.tm_var [in References]
STLCRef.Ty_Ref [in References]
STLCRef.Ty_Arrow [in References]
STLCRef.Ty_Unit [in References]
STLCRef.Ty_Nat [in References]
STLCRef.T_Assign [in References]
STLCRef.T_Deref [in References]
STLCRef.T_Ref [in References]
STLCRef.T_Loc [in References]
STLCRef.T_Unit [in References]
STLCRef.T_If0 [in References]
STLCRef.T_Mult [in References]
STLCRef.T_Pred [in References]
STLCRef.T_Succ [in References]
STLCRef.T_Nat [in References]
STLCRef.T_App [in References]
STLCRef.T_Abs [in References]
STLCRef.T_Var [in References]
STLCRef.v_loc [in References]
STLCRef.v_unit [in References]
STLCRef.v_nat [in References]
STLCRef.v_abs [in References]
STLCSub.ST_If [in Sub]
STLCSub.ST_IfFalse [in Sub]
STLCSub.ST_IfTrue [in Sub]
STLCSub.ST_App2 [in Sub]
STLCSub.ST_App1 [in Sub]
STLCSub.ST_AppAbs [in Sub]
STLCSub.S_Arrow [in Sub]
STLCSub.S_Top [in Sub]
STLCSub.S_Trans [in Sub]
STLCSub.S_Refl [in Sub]
STLCSub.tm_snd [in Sub]
STLCSub.tm_fst [in Sub]
STLCSub.tm_pair [in Sub]
STLCSub.tm_unit [in Sub]
STLCSub.tm_if [in Sub]
STLCSub.tm_false [in Sub]
STLCSub.tm_true [in Sub]
STLCSub.tm_abs [in Sub]
STLCSub.tm_app [in Sub]
STLCSub.tm_var [in Sub]
STLCSub.Ty_Prod [in Sub]
STLCSub.Ty_Unit [in Sub]
STLCSub.Ty_Arrow [in Sub]
STLCSub.Ty_Base [in Sub]
STLCSub.Ty_Bool [in Sub]
STLCSub.Ty_Top [in Sub]
STLCSub.T_Sub [in Sub]
STLCSub.T_Unit [in Sub]
STLCSub.T_If [in Sub]
STLCSub.T_False [in Sub]
STLCSub.T_True [in Sub]
STLCSub.T_App [in Sub]
STLCSub.T_Abs [in Sub]
STLCSub.T_Var [in Sub]
STLCSub.v_unit [in Sub]
STLCSub.v_false [in Sub]
STLCSub.v_true [in Sub]
STLCSub.v_abs [in Sub]
STLC.ST_If [in Stlc]
STLC.ST_IfFalse [in Stlc]
STLC.ST_IfTrue [in Stlc]
STLC.ST_App2 [in Stlc]
STLC.ST_App1 [in Stlc]
STLC.ST_AppAbs [in Stlc]
STLC.s_var1 [in Stlc]
STLC.tm_if [in Stlc]
STLC.tm_false [in Stlc]
STLC.tm_true [in Stlc]
STLC.tm_abs [in Stlc]
STLC.tm_app [in Stlc]
STLC.tm_var [in Stlc]
STLC.Ty_Arrow [in Stlc]
STLC.Ty_Bool [in Stlc]
STLC.T_If [in Stlc]
STLC.T_False [in Stlc]
STLC.T_True [in Stlc]
STLC.T_App [in Stlc]
STLC.T_Abs [in Stlc]
STLC.T_Var [in Stlc]
STLC.v_false [in Stlc]
STLC.v_true [in Stlc]
STLC.v_abs [in Stlc]
ST_Plus2 [in Smallstep]
ST_Plus1 [in Smallstep]
ST_PlusConstConst [in Smallstep]
ST_SndPair [in Norm]
ST_Snd1 [in Norm]
ST_FstPair [in Norm]
ST_Fst1 [in Norm]
ST_Pair2 [in Norm]
ST_Pair1 [in Norm]
ST_If [in Norm]
ST_IfFalse [in Norm]
ST_IfTrue [in Norm]
ST_App2 [in Norm]
ST_App1 [in Norm]
ST_AppAbs [in Norm]
T
Temp1.ST_Plus2 [in Smallstep]Temp1.ST_Plus1 [in Smallstep]
Temp1.ST_PlusConstConst [in Smallstep]
Temp1.v_funny [in Smallstep]
Temp1.v_const [in Smallstep]
Temp2.ST_Plus2 [in Smallstep]
Temp2.ST_Plus1 [in Smallstep]
Temp2.ST_PlusConstConst [in Smallstep]
Temp2.ST_Funny [in Smallstep]
Temp2.v_const [in Smallstep]
Temp3.ST_Plus1 [in Smallstep]
Temp3.ST_PlusConstConst [in Smallstep]
Temp3.v_const [in Smallstep]
Temp4.fls [in Smallstep]
Temp4.ST_If [in Smallstep]
Temp4.ST_IfFalse [in Smallstep]
Temp4.ST_IfTrue [in Smallstep]
Temp4.Temp5.ST_If [in Smallstep]
Temp4.Temp5.ST_IfFalse [in Smallstep]
Temp4.Temp5.ST_IfTrue [in Smallstep]
Temp4.test [in Smallstep]
Temp4.tru [in Smallstep]
Temp4.v_fls [in Smallstep]
Temp4.v_tru [in Smallstep]
tm_snd [in Norm]
tm_fst [in Norm]
tm_pair [in Norm]
tm_if [in Norm]
tm_false [in Norm]
tm_true [in Norm]
tm_abs [in Norm]
tm_app [in Norm]
tm_var [in Norm]
TM.Bool [in Types]
TM.bv_false [in Types]
TM.bv_True [in Types]
TM.fls [in Types]
TM.iszro [in Types]
TM.ite [in Types]
TM.Nat [in Types]
TM.nv_succ [in Types]
TM.nv_0 [in Types]
TM.prd [in Types]
TM.scc [in Types]
TM.ST_Iszero [in Types]
TM.ST_IszeroSucc [in Types]
TM.ST_Iszero0 [in Types]
TM.ST_Pred [in Types]
TM.ST_PredSucc [in Types]
TM.ST_Pred0 [in Types]
TM.ST_Succ [in Types]
TM.ST_If [in Types]
TM.ST_IfFalse [in Types]
TM.ST_IfTrue [in Types]
TM.tru [in Types]
TM.T_Iszero [in Types]
TM.T_Pred [in Types]
TM.T_Succ [in Types]
TM.T_0 [in Types]
TM.T_If [in Types]
TM.T_False [in Types]
TM.T_True [in Types]
TM.zro [in Types]
Ty_Prod [in Norm]
Ty_Arrow [in Norm]
Ty_Bool [in Norm]
T_Snd [in Norm]
T_Fst [in Norm]
T_Pair [in Norm]
T_If [in Norm]
T_False [in Norm]
T_True [in Norm]
T_App [in Norm]
T_Abs [in Norm]
T_Var [in Norm]
V
VNUId [in Equiv]VNUMinus [in Equiv]
VNUMult [in Equiv]
VNUNum [in Equiv]
VNUPlus [in Equiv]
v_const [in Smallstep]
V_cons [in Norm]
V_nil [in Norm]
v_pair [in Norm]
v_false [in Norm]
v_true [in Norm]
v_abs [in Norm]
Axiom Index
E
EqualityExamples.big_expression_using [in UseTactics]ExamplesLets.typing_inversion_var [in UseTactics]
G
gt_not_le [in UseAuto]I
inj_pair2 [in LibTactics]L
le_gt_false [in UseAuto]le_not_gt [in UseAuto]
P
P [in UseAuto]S
skip_axiom [in LibTactics]subtype [in UseAuto]
subtype_trans [in UseAuto]
subtype_refl [in UseAuto]
T
typ [in UseAuto]Inductive Index
A
appears_free_in [in Norm]astep [in Smallstep]
aval [in Smallstep]
B
block [in PE]Boxer [in LibTactics]
bstep [in Smallstep]
C
CImp.com [in Smallstep]CImp.cstep [in Smallstep]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
cstep [in Smallstep]
D
dcom [in Hoare2]decorated [in Hoare2]
derivable [in HoareAsLogic]
E
eval [in Smallstep]H
has_type [in Norm]Himp.ceval [in Hoare]
Himp.ceval [in Equiv]
Himp.com [in Hoare]
Himp.com [in Equiv]
HoareAssertAssume.ceval [in Hoare]
HoareAssertAssume.com [in Hoare]
HoareAssertAssume.result [in Hoare]
I
If1.ceval [in Hoare]If1.com [in Hoare]
instantiation [in Norm]
L
Loop.ceval_count [in PE]Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
ltac_goal_to_discard [in LibTactics]
Ltac_database_token [in LibTactics]
ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]
M
multi [in Smallstep]P
parity_label [in PE]peval [in PE]
pe_peval [in PE]
pe_ceval [in PE]
pe_com [in PE]
R
RecordSub.has_type [in RecordSub]RecordSub.record_tm [in RecordSub]
RecordSub.record_ty [in RecordSub]
RecordSub.step [in RecordSub]
RecordSub.subtype [in RecordSub]
RecordSub.tm [in RecordSub]
RecordSub.ty [in RecordSub]
RecordSub.value [in RecordSub]
RecordSub.well_formed_ty [in RecordSub]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
S
SimpleArith1.step [in Smallstep]stack_step [in Smallstep]
step [in Smallstep]
step [in Norm]
STLCArith.has_type [in StlcProp]
STLCArith.step [in StlcProp]
STLCArith.tm [in StlcProp]
STLCArith.ty [in StlcProp]
STLCArith.value [in StlcProp]
STLCExtendedRecords.FirstTry.ty [in Records]
STLCExtendedRecords.has_type [in Records]
STLCExtendedRecords.record_tm [in Records]
STLCExtendedRecords.record_ty [in Records]
STLCExtendedRecords.step [in Records]
STLCExtendedRecords.tm [in Records]
STLCExtendedRecords.ty [in Records]
STLCExtendedRecords.value [in Records]
STLCExtendedRecords.well_formed_ty [in Records]
STLCExtended.has_type [in MoreStlc]
STLCExtended.step [in MoreStlc]
STLCExtended.tm [in MoreStlc]
STLCExtended.ty [in MoreStlc]
STLCExtended.value [in MoreStlc]
STLCProp.appears_free_in [in StlcProp]
STLCRef.extends [in References]
STLCRef.has_type [in References]
STLCRef.RefsAndNontermination.step_closure [in References]
STLCRef.step [in References]
STLCRef.tm [in References]
STLCRef.ty [in References]
STLCRef.value [in References]
STLCSub.has_type [in Sub]
STLCSub.step [in Sub]
STLCSub.subtype [in Sub]
STLCSub.tm [in Sub]
STLCSub.ty [in Sub]
STLCSub.value [in Sub]
STLC.has_type [in Stlc]
STLC.step [in Stlc]
STLC.substi [in Stlc]
STLC.tm [in Stlc]
STLC.ty [in Stlc]
STLC.value [in Stlc]
T
Temp1.step [in Smallstep]Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Smallstep]
tm [in Norm]
TM.bvalue [in Types]
TM.has_type [in Types]
TM.nvalue [in Types]
TM.step [in Types]
TM.tm [in Types]
TM.ty [in Types]
ty [in Norm]
V
value [in Smallstep]value [in Norm]
var_not_used_in_aexp [in Equiv]
Section Index
D
DemoAbsurd1 [in UseAuto]E
equatesLemma [in LibTactics]F
FuncEq [in LibTactics]H
HintsTransitivity [in UseAuto]Abbreviation Index
A
assert [in Hoare]M
mkAexp [in Hoare]multistep [in Norm]
R
RecordSub.Examples.A [in RecordSub]RecordSub.Examples.B [in RecordSub]
RecordSub.Examples.C [in RecordSub]
RecordSub.Examples.i [in RecordSub]
RecordSub.Examples.j [in RecordSub]
RecordSub.Examples.k [in RecordSub]
RecordSub.Examples.x [in RecordSub]
RecordSub.Examples.y [in RecordSub]
RecordSub.Examples.z [in RecordSub]
S
step_normal_form [in Norm]STLCArith.multistep [in StlcProp]
STLCExtendedRecords.A [in Records]
STLCExtendedRecords.a [in Records]
STLCExtendedRecords.B [in Records]
STLCExtendedRecords.f [in Records]
STLCExtendedRecords.g [in Records]
STLCExtendedRecords.i1 [in Records]
STLCExtendedRecords.i2 [in Records]
STLCExtendedRecords.k [in Records]
STLCExtendedRecords.l [in Records]
STLCExtendedRecords.multistep [in Records]
STLCExtended.Examples.a [in MoreStlc]
STLCExtended.Examples.eo [in MoreStlc]
STLCExtended.Examples.eq [in MoreStlc]
STLCExtended.Examples.even [in MoreStlc]
STLCExtended.Examples.evenodd [in MoreStlc]
STLCExtended.Examples.f [in MoreStlc]
STLCExtended.Examples.g [in MoreStlc]
STLCExtended.Examples.i1 [in MoreStlc]
STLCExtended.Examples.i2 [in MoreStlc]
STLCExtended.Examples.k [in MoreStlc]
STLCExtended.Examples.l [in MoreStlc]
STLCExtended.Examples.m [in MoreStlc]
STLCExtended.Examples.n [in MoreStlc]
STLCExtended.Examples.odd [in MoreStlc]
STLCExtended.Examples.processSum [in MoreStlc]
STLCExtended.Examples.x [in MoreStlc]
STLCExtended.Examples.y [in MoreStlc]
STLCExtended.multistep [in MoreStlc]
STLCSub.Examples.A [in Sub]
STLCSub.Examples.B [in Sub]
STLCSub.Examples.C [in Sub]
STLCSub.Examples.Float [in Sub]
STLCSub.Examples.Integer [in Sub]
STLCSub.Examples.String [in Sub]
STLCSub.Examples.x [in Sub]
STLCSub.Examples.y [in Sub]
STLCSub.Examples.z [in Sub]
STLCSub.FormalThoughtExercises.a [in Sub]
STLCSub.FormalThoughtExercises.p [in Sub]
STLC.idB [in Stlc]
STLC.idBB [in Stlc]
STLC.idBBBB [in Stlc]
STLC.k [in Stlc]
STLC.multistep [in Stlc]
STLC.notB [in Stlc]
T
TM.step_normal_form [in Types]Definition Index
A
aequiv [in Equiv]Aexp [in Hoare]
Aexp_of_aexp [in Hoare]
Aexp_of_nat [in Hoare]
ap [in Hoare]
ap2 [in Hoare]
Assertion [in Hoare]
assert_of_Prop [in Hoare]
assert_implies [in Hoare]
assign [in PE]
assigned [in PE]
assn_sub_ex2' [in Hoare]
assn_sub_ex1' [in Hoare]
assn_sub_example2'' [in Hoare]
assn_sub_example2' [in Hoare]
assn_sub_example2 [in Hoare]
assn_sub_example [in Hoare]
assn_sub [in Hoare]
atrans_sound [in Equiv]
B
bassn [in Hoare]bequiv [in Equiv]
btrans_sound [in Equiv]
C
capprox [in Equiv]cequiv [in Equiv]
CImp.cmultistep [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop [in Smallstep]
closed [in Norm]
closed_env [in Norm]
cmin [in Equiv]
COIND [in LibTactics]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
context [in Norm]
ctrans_sound [in Equiv]
c3 [in Equiv]
c4 [in Equiv]
D
dec_while_triple_correct [in Hoare2]dec_while [in Hoare2]
dec0 [in Hoare2]
dec1 [in Hoare2]
deterministic [in Smallstep]
dfib [in Hoare2]
div_mod_dec [in Hoare2]
dpow2_dec [in Hoare2]
drop [in Norm]
E
empty_pe_state [in PE]env [in Norm]
equiv_classes [in Equiv]
eq' [in LibTactics]
evalF [in Smallstep]
ExamplePrettyAssertions.assn1 [in Hoare]
ExamplePrettyAssertions.assn2 [in Hoare]
ExamplePrettyAssertions.assn3 [in Hoare]
ExamplePrettyAssertions.assn4 [in Hoare]
ExamplePrettyAssertions.ex1 [in Hoare]
ExamplePrettyAssertions.ex2 [in Hoare]
ExamplePrettyAssertions.ex3 [in Hoare]
ExAssertions.assn1 [in Hoare]
ExAssertions.assn2 [in Hoare]
ExAssertions.assn3 [in Hoare]
ExAssertions.assn4 [in Hoare]
extract [in Hoare2]
extract_while_ex [in Hoare2]
extract_dec [in Hoare2]
F
factorial_dec [in Hoare2]fib [in Hoare2]
FILL_IN_HERE [in Smallstep]
FILL_IN_HERE [in Hoare2]
FirstTry.type_check [in Typechecking]
fold_com_ex1 [in Equiv]
fold_constants_com [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_constants_bexp [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_aexp_ex1 [in Equiv]
fold_constants_aexp [in Equiv]
H
halts [in Norm]Himp.cequiv [in Equiv]
Himp.havoc_pre [in Hoare]
Himp.havoc_example2 [in Equiv]
Himp.havoc_example1 [in Equiv]
Himp.hoare_triple [in Hoare]
Himp.manual_grade_for_Check_rule_for_HAVOC [in Equiv]
Himp.pcopy [in Equiv]
Himp.ptwice [in Equiv]
Himp.pXY [in Equiv]
Himp.pYX [in Equiv]
Himp.p1 [in Equiv]
Himp.p2 [in Equiv]
Himp.p3 [in Equiv]
Himp.p4 [in Equiv]
Himp.p5 [in Equiv]
Himp.p6 [in Equiv]
HoareAssertAssume.assert_assume_example [in Hoare]
HoareAssertAssume.hoare_triple [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example1''' [in Hoare]
hoare_asgn_example1'' [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example1 [in Hoare]
hoare_asgn_examples2 [in Hoare]
hoare_asgn_examples1 [in Hoare]
hoare_triple [in Hoare]
I
if_example''' [in Hoare]if_example'' [in Hoare]
if_example [in Hoare]
if_minus_plus_dec [in Hoare2]
If1.hoare_triple [in Hoare]
If1.if1false_test [in Hoare]
If1.if1true_test [in Hoare]
If1.manual_grade_for_hoare_if1 [in Hoare]
inb [in PE]
InvertsExamples1.typing_nonexample_1 [in UseTactics]
is_wp [in Hoare2]
K
keval [in PE]keval_example [in PE]
L
lookup [in Norm]Loop.pe_loop_example4 [in PE]
Loop.pe_loop_example3 [in PE]
Loop.pe_loop_example2 [in PE]
Loop.pe_loop_example1 [in PE]
Loop.square_loop [in PE]
ltac_something [in LibTactics]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_int_to_nat [in LibTactics]
ltac_database [in LibTactics]
M
manual_grade_for_eval__multistep_inf [in Smallstep]manual_grade_for_hoare_repeat [in Hoare]
manual_grade_for_hoare_asgn_wrong [in Hoare]
manual_grade_for_not_congr [in Equiv]
manual_grade_for_equiv_classes [in Equiv]
manual_grade_for_norm [in Norm]
manual_grade_for_norm_fail [in Norm]
manual_grade_for_pair_permutation [in Sub]
manual_grade_for_smallest_2 [in Sub]
manual_grade_for_smallest_1 [in Sub]
manual_grade_for_small_large_4 [in Sub]
manual_grade_for_small_large_2 [in Sub]
manual_grade_for_small_large_1 [in Sub]
manual_grade_for_proper_subtypes [in Sub]
manual_grade_for_subtype_concepts_tf [in Sub]
manual_grade_for_subtype_instances_tf_2 [in Sub]
manual_grade_for_subtype_order [in Sub]
manual_grade_for_arrow_sub_wrong [in Sub]
minimum_dec [in Hoare2]
msubst [in Norm]
mupdate [in Norm]
myFact [in UseAuto]
N
normalizing [in Smallstep]normal_form_of [in Smallstep]
normal_form [in Smallstep]
O
optimizer [in Equiv]optimize_0plus_com [in Equiv]
optimize_0plus_bexp [in Equiv]
optimize_0plus_aexp [in Equiv]
outer_triple_valid [in Hoare2]
P
parity [in Hoare2]parity [in PE]
parity_dec [in Hoare2]
parity_eval [in PE]
parity_body [in PE]
pe_program [in PE]
pe_block_example [in PE]
pe_block [in PE]
pe_example3 [in PE]
pe_example2 [in PE]
pe_example1 [in PE]
pe_removes [in PE]
pe_compare [in PE]
pe_unique [in PE]
pe_disagree_at [in PE]
pe_add [in PE]
pe_remove [in PE]
pe_bexp [in PE]
pe_update [in PE]
pe_consistent [in PE]
pe_aexp [in PE]
pe_lookup [in PE]
pe_state [in PE]
positive_difference_dec [in Hoare2]
post [in Hoare2]
post_dec_while [in Hoare2]
post_dec [in Hoare2]
pow2 [in Hoare2]
pre_dec_while [in Hoare2]
pre_dec [in Hoare2]
prog [in Smallstep]
program [in PE]
prog_i [in Equiv]
prog_h [in Equiv]
prog_g [in Equiv]
prog_f [in Equiv]
prog_e [in Equiv]
prog_d [in Equiv]
prog_c [in Equiv]
prog_b [in Equiv]
prog_a [in Equiv]
R
R [in Norm]RecordSub.context [in RecordSub]
RecordSub.Examples.subtyping_example_4 [in RecordSub]
RecordSub.Examples.subtyping_example_3 [in RecordSub]
RecordSub.Examples.subtyping_example_2 [in RecordSub]
RecordSub.Examples.subtyping_example_1 [in RecordSub]
RecordSub.Examples.subtyping_example_0 [in RecordSub]
RecordSub.Examples.TRcd_kj [in RecordSub]
RecordSub.Examples.TRcd_j [in RecordSub]
RecordSub.Examples2.trcd_kj [in RecordSub]
RecordSub.Examples2.typing_example_2 [in RecordSub]
RecordSub.Examples2.typing_example_1 [in RecordSub]
RecordSub.Examples2.typing_example_0 [in RecordSub]
RecordSub.manual_grade_for_rcd_types_match_informal [in RecordSub]
RecordSub.subst [in RecordSub]
RecordSub.tlookup [in RecordSub]
RecordSub.Tlookup [in RecordSub]
reduce_to_zero' [in Hoare2]
refines [in Equiv]
relation [in Smallstep]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.hoare_triple [in Hoare]
rm [in LibTactics]
S
sample_proof [in HoareAsLogic]SimpleArith1.test_step_2 [in Smallstep]
SimpleArith1.test_step_1 [in Smallstep]
slow_assignment_dec [in Hoare2]
sqrt_dec [in Hoare2]
stack [in Smallstep]
stack_multistep [in Smallstep]
StepFunction.assert [in Typechecking]
StepFunction.manual_grade_for_stepf_defn [in Typechecking]
StepFunction.manual_grade_for_valuef_defn [in Typechecking]
StepFunction.stepf [in Typechecking]
StepFunction.valuef [in Typechecking]
step_example1''' [in Smallstep]
step_example1'' [in Smallstep]
step_example1' [in Smallstep]
step_example1 [in Smallstep]
step_normal_form [in Smallstep]
STLCArith.context [in StlcProp]
STLCArith.Nat_typing_example [in StlcProp]
STLCArith.Nat_step_example [in StlcProp]
STLCArith.subst [in StlcProp]
STLCChecker.type_check [in Typechecking]
STLCExtendedRecords.context [in Records]
STLCExtendedRecords.FirstTry.alist [in Records]
STLCExtendedRecords.subst [in Records]
STLCExtendedRecords.Tlookup [in Records]
STLCExtendedRecords.tlookup [in Records]
STLCExtendedRecords.typing_nonexample_2 [in Records]
STLCExtendedRecords.typing_nonexample [in Records]
STLCExtendedRecords.weird_type [in Records]
STLCExtended.context [in MoreStlc]
STLCExtended.Examples.FixTest1.fact [in MoreStlc]
STLCExtended.Examples.FixTest1.reduces [in MoreStlc]
STLCExtended.Examples.FixTest1.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest2.map [in MoreStlc]
STLCExtended.Examples.FixTest2.reduces [in MoreStlc]
STLCExtended.Examples.FixTest2.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest3.equal [in MoreStlc]
STLCExtended.Examples.FixTest3.reduces [in MoreStlc]
STLCExtended.Examples.FixTest3.reduces2 [in MoreStlc]
STLCExtended.Examples.FixTest3.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest4.eotest [in MoreStlc]
STLCExtended.Examples.FixTest4.reduces [in MoreStlc]
STLCExtended.Examples.FixTest4.typechecks [in MoreStlc]
STLCExtended.Examples.LetTest.reduces [in MoreStlc]
STLCExtended.Examples.LetTest.tm_test [in MoreStlc]
STLCExtended.Examples.LetTest.typechecks [in MoreStlc]
STLCExtended.Examples.ListTest.reduces [in MoreStlc]
STLCExtended.Examples.ListTest.tm_test [in MoreStlc]
STLCExtended.Examples.ListTest.typechecks [in MoreStlc]
STLCExtended.Examples.Numtest.reduces [in MoreStlc]
STLCExtended.Examples.Numtest.tm_test [in MoreStlc]
STLCExtended.Examples.Numtest.typechecks [in MoreStlc]
STLCExtended.Examples.ProdTest.reduces [in MoreStlc]
STLCExtended.Examples.ProdTest.tm_test [in MoreStlc]
STLCExtended.Examples.ProdTest.typechecks [in MoreStlc]
STLCExtended.Examples.Sumtest1.reduces [in MoreStlc]
STLCExtended.Examples.Sumtest1.tm_test [in MoreStlc]
STLCExtended.Examples.Sumtest1.typechecks [in MoreStlc]
STLCExtended.Examples.Sumtest2.reduces [in MoreStlc]
STLCExtended.Examples.Sumtest2.tm_test [in MoreStlc]
STLCExtended.Examples.Sumtest2.typechecks [in MoreStlc]
STLCExtended.subst [in MoreStlc]
STLCExtended.x [in MoreStlc]
STLCExtended.y [in MoreStlc]
STLCExtended.z [in MoreStlc]
STLCProp.closed [in StlcProp]
STLCProp.manual_grade_for_stlc_variation3 [in StlcProp]
STLCProp.manual_grade_for_stlc_variation2 [in StlcProp]
STLCProp.manual_grade_for_stlc_variation1 [in StlcProp]
STLCProp.manual_grade_for_progress_preservation_statement [in StlcProp]
STLCProp.manual_grade_for_afi [in StlcProp]
STLCProp.manual_grade_for_subject_expansion_stlc [in StlcProp]
STLCProp.stuck [in StlcProp]
STLCRef.context [in References]
STLCRef.ExampleVariables.r [in References]
STLCRef.ExampleVariables.s [in References]
STLCRef.ExampleVariables.x [in References]
STLCRef.ExampleVariables.y [in References]
STLCRef.manual_grade_for_preservation_informal [in References]
STLCRef.manual_grade_for_type_safety_violation [in References]
STLCRef.manual_grade_for_compact_update [in References]
STLCRef.multistep [in References]
STLCRef.preservation_theorem [in References]
STLCRef.RefsAndNontermination.factorial [in References]
STLCRef.RefsAndNontermination.loop [in References]
STLCRef.RefsAndNontermination.loop_fun [in References]
STLCRef.RefsAndNontermination.multistep1 [in References]
STLCRef.replace [in References]
STLCRef.store [in References]
STLCRef.store_well_typed [in References]
STLCRef.store_Tlookup [in References]
STLCRef.store_ty [in References]
STLCRef.store_lookup [in References]
STLCRef.subst [in References]
STLCRef.tseq [in References]
STLCRef.x [in References]
STLCRef.y [in References]
STLCRef.z [in References]
STLCSub.context [in Sub]
STLCSub.Examples.Employee [in Sub]
STLCSub.Examples.Person [in Sub]
STLCSub.Examples.Student [in Sub]
STLCSub.Examples.subtyping_example_2 [in Sub]
STLCSub.Examples.subtyping_example_1 [in Sub]
STLCSub.Examples.subtyping_example_0 [in Sub]
STLCSub.Examples.sub_employee_person [in Sub]
STLCSub.Examples.sub_student_person [in Sub]
STLCSub.FormalThoughtExercises.smallest [in Sub]
STLCSub.FormalThoughtExercises.smallest_largest [in Sub]
STLCSub.FormalThoughtExercises.TF [in Sub]
STLCSub.manual_grade_for_products_preservation [in Sub]
STLCSub.manual_grade_for_products_progress [in Sub]
STLCSub.manual_grade_for_products_subtype_has_type [in Sub]
STLCSub.manual_grade_for_products_value_step [in Sub]
STLCSub.manual_grade_for_variations [in Sub]
STLCSub.subst [in Sub]
STLCTypes.eqb_ty [in Typechecking]
STLC.context [in Stlc]
STLC.subst [in Stlc]
STLC.typing_nonexample_3 [in Stlc]
STLC.typing_nonexample_1 [in Stlc]
STLC.typing_example_3 [in Stlc]
STLC.typing_example_2_full [in Stlc]
STLC.typing_example_2 [in Stlc]
STLC.typing_example_1' [in Stlc]
STLC.typing_example_1 [in Stlc]
STLC.x [in Stlc]
STLC.y [in Stlc]
STLC.z [in Stlc]
subst [in Norm]
subst_equiv_property [in Equiv]
subst_aexp_ex [in Equiv]
subst_aexp [in Equiv]
subtract_slowly_dec [in Hoare2]
swap_program [in Hoare]
swap_dec [in Hoare2]
T
T [in Hoare2]tass [in Norm]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop1 [in Smallstep]
Temp4.manual_grade_for_smallstep_bools [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
Temp4.Temp5.manual_grade_for_properties_of_altered_step [in Smallstep]
test_optimize_0plus [in Equiv]
test_pe_bexp2 [in PE]
test_pe_bexp1 [in PE]
test_pe_update [in PE]
test_pe_aexp1 [in PE]
text_pe_aexp2 [in PE]
TM.has_type_not [in Types]
TM.has_type_1 [in Types]
TM.manual_grade_for_prog_pres_bigstep [in Types]
TM.manual_grade_for_remove_pred0 [in Types]
TM.manual_grade_for_variation2 [in Types]
TM.manual_grade_for_variation1 [in Types]
TM.manual_grade_for_finish_preservation_informal [in Types]
TM.manual_grade_for_finish_progress_informal [in Types]
TM.multistep [in Types]
TM.some_term_is_stuck [in Types]
TM.stuck [in Types]
TM.succ_hastype_nat__hastype_nat [in Types]
TM.value [in Types]
two_loops_dec [in Hoare2]
TypecheckerExtensions.eqb_ty [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_check_defn [in Typechecking]
TypecheckerExtensions.type_check [in Typechecking]
V
valid [in HoareAsLogic]vc_dec_while [in Hoare2]
verification_conditions_dec [in Hoare2]
verification_conditions [in Hoare2]
W
while_example [in Hoare]wp [in HoareAsLogic]
Z
zprop [in Equiv]| 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 | (5472 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 | (309 entries) |
| Binder 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 | (3342 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 | (70 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 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 | (22 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 | (504 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 | (615 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 | (12 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 | (118 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 | (4 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 | (60 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 | (401 entries) |
This page has been generated by coqdoc


in first
```
Some properties of each element
- `.innerHTML`: the actual HTML content (not necessarily just text!)
- `.`, e.g. `.src`, any attribute of this element
- ...alternatively: `.setAttribute(attr, val)`
- `.style.`, e.g. `document.body.style.margin = "5px"`
- `.on`, e.g. `.onclick` hooks for JS
---
# Attaching JS to Elements
- https://developer.mozilla.org/en-US/docs/Web/Events
- _Inline_, e.g.
```html
Click me!
```
```javascript
function action(e) { e.innerHTML = "I was clicked..."; }
```
- Via JavaScript, single or multiple handlers:
```javascript
document.getElementById("myBtn").onclick = function(e) { ... }
```
```javascript
document.getElementById("myBtn").addEventListener("click", function(e) { ...});
```
- If set via JS, `this` is automatically given as first argument.
---
# Navigating the DOM
https://developer.mozilla.org/en-US/docs/Mozilla/Tech/XUL/Tutorial/Document_Object_Model#Navigating_the_DOM
- DOM is a tree structure, so you can navigate it
- Root is `document.documentElement`
- Linkage is: `firstChild`, `lastChild`, `childNodes`, `parentNode`, `nextSibling`, `previousSibling`
Example: Iterate over the children of the root node:
```javascript
var childNodes = document.documentElement.childNodes;
for (var i = 0; i < childNodes.length; i++) {
var child = childNodes[i];
// do something with child
}
```
---
# Node Types
https://developer.mozilla.org/en-US/docs/Web/API/Node/nodeType
Nodes (elements) can be of different typ, for example:
- `Node.ELEMENT_NODE`: a regular node
- `Node.TEXT_NODE`: the actual text content of an element (or attribute)
- `Node.DOCUMENT_NODE`: a document node, e.g. `document` (or inside an iframe)
---
# Iterating over Elements
```html
Collect.
```
```javascript
window.collect = function () {
var f = document.forms["login"];
var text = "";
for (var e of f) {
text += e.value;
}
document.getElementById("text").innerHTML = text;
}
```
---
# Modifying the DOM
`document.createElement(tagname)` creates (and returns) a new element.
Use `.insertBefore()` and `.appendChild()` to add the new element to the DOM.
Block elements (`p`, `div`, ...) need a _text_ node to display content.
Use `.removeChild()` to remove a certain element from the DOM.
```html
This is a paragraph.
This is another paragraph.
```
```javascript
var para = document.createElement("p");
var node = document.createTextNode("This is new.");
para.appendChild(node);
var element = document.getElementById("div1");
var child = document.getElementById("p1");
element.insertBefore(para, child);
```
---
# Browser Object Model (BOM)
- `window` object represents the browser window
- Contains all global objects, functions and variables (will be added automatically)
- Example methods: `window.open()` or `window.close()`
- `window.location` manages what page is loaded; to navigate away, you can set `window.location.href = ...`
- `window.history` manages the history of the current window; use `window.history.back()` to navigate one step back.

You can access/modify cookies via `document.cookie`. (They're text-based).
Cookies are in a sense _historic_ (security exploits, disabled by browsers, etc.)
If you plan on "remembering" users and their sessions, use [localstorage](https://developer.mozilla.org/en-US/docs/Web/API/Window/localStorage) or [sessionstorage](https://developer.mozilla.org/en-US/docs/Web/API/Window/sessionStorage).
```javascript
sessionStorage.setItem('key', 'value'); // same for localStorage
sessionStorage.getItem('key');
sessionStorage.removeItem('key');
sessionStorage.clear();
```
Content protected by browser (vs. plain text files on disk).
---
# Timeouts and "Multi-Threading"
JavaScript is inherently single threaded (unless you use [web workers](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers))
Never ever consider an active wait:
```javascript
while (!ready())
;
```
![Never Ever](/assets/never.gif)
---
# Timeouts and "Multi-Threading"
JavaScript runs the [_event loop_](https://developer.mozilla.org/en-US/docs/Web/JavaScript/EventLoop).
Use `on<....>` events with callbacks to react to (active) user input.
Use [_timers_](https://developer.mozilla.org/en-US/Add-ons/Code_snippets/Timers) to schedule (repetetive) tasks.
```javascript
var timeoutID = setTimeout(function[, delay, param1, param2, ...]);
var intervalID = scope.setInterval(func, delay[, param1, param2, ...]);
```
```javascript
var t1 = setTimeout(function() { alert('Hello world!'); }, 1000);
var t2 = setInterval(function() { alert('Hello, again!'); }, 1000);
clearTimeout(t1);
clearInterval(t2);
```
---
# AJAX
_Asynchronous JavaScript and XML (nowadays: JSON)_
- Use JS to dynamically retrieve data and manipulate the DOM
- Mid-90ies: early appearance in IE5, Mozilla, Safari
- Mid-2000s: wide-spread popularity (OWA, Gmail, Maps, Kayak)
- `XMLHttpRequest` standardized in 2006 (first draft)
- Today: state-of-the-art (webmailers, )
- Drawback: not all crawlers execute JS, thus harder to index
---
.right[[DanielSHaischt, via Wikimedia Commons](https://commons.wikimedia.org/wiki/File%3AAjax-vergleich.svg) ]
---
# XMLHttpRequest
Retrieve data from a (remote) URL; use the `onload` event handler to install a callback for once the response comes in.
```javascript
var xhr = new XMLHttpRequest();
xhr.open('GET', '//openmensa.org/api/v2/canteens/229/days/20171109/meals');
xhr.onload = function() {
if (xhr.status === 200) {
var meals = processMenu(JSON.parse(xhr.responseText));
renderMenu(meals);
} else {
console.log('Request failed. Returned status of ' + xhr.status);
}
};
xhr.send();
```
More on requests next week!
---
# Fetch: Modern and Elegant
`XMLHttpRequest` is a bit clumsy.
Use the modern [`fetch` function](https://developer.mozilla.org/en-US/docs/Web/API/Fetch_API) (ES6).
```javascript
fetch('//openmensa.org/api/v2/canteens/229/days/20171109/meals')
.then(function(response) {
response.text().then(function(text) {
document.getElementById('resp').innerHTML = text;
});
});
```
---
# jQuery
http://jquery.com/
Simplifies JavaScript for DOM and AJAX interaction.
Syntax `$(selector).action()`:
- `$` for jQuery
- _selector_ to query (or find) HTML elements (can be a result list!)
- _action_ to perform on the element(s)
Examples:
- `$(this).hide()`: hides current element
- `$('p').hide()`: hides all `p` elements
- `$('.test').hide()`: hides all elements with class `.test`
- `$('#test').hide()`: hides the element with id `test`
---
# jQuery: DOM Traversal and Manipulation
Get the ` element with the class 'continue' and change its HTML to 'Next Step...'
```javascript
$('button.continue').html('Next Step...');
```
Other frequently used functions:
- `.css('attribute', 'value')`: set certain CSS properties
- `.attr('id', 'value')`: set certain element attriutes (id, etc.)
- `.append()`, `.remove()`, etc. to modify DOM
---
# jQuery: Event Handling
Show the `#banner-message` element that is hidden with `display:none` in its CSS when any button in `#button-container` is clicked.
```javascript
var hiddenBox = $('#banner-message');
$('#button-container button').on('click', function (event) {
hiddenBox.show();
});
```
---
# jQuery: Ajax
```html
```
```javascript
$.ajax({
url: '//api.icndb.com/jokes/random',
data: {
firstName: 'Hans',
lastName: 'Dampf'
},
success: function (data) {
$('blockquote').text(data.value.joke);
}
});
```
```javascript
$.ajax({
url: '//api.icndb.com/jokes/random'
})
.done(function (data) {
$('blockquote').text(data.value.joke);
});
```
---
# Summary
The DOM and BOM allow you to dynamically interact with the current window and the page that's currently rendered.
JavaScript allows you to modify the DOM as long as the page is open.
jQuery makes traversing and manipulating the DOM ridiculously easy.
jQuery selectors make it easy to apply manipulations to lists of elements; think almost like a database query!
Use `$.ajax` (or if `XMLHttpRequest`, if no jQuery) to dynamically load data and alter your page.
**Outlook**: Even with jQuery, rendering dynamic content is pretty cumbersome -- we'll talk about toolkits in a few weeks!


Login Form
Chat app
Log In
Don't have an account? Register here.
Already logged in and want to logout?


The previous example created a server that dealt with response errors by aborting response generation, potentially avoiding pointless work. However, it did this silently for any error. In this example, we'll modify the previous example so that it logs each failed response.
This example will use the Twisted API for logging errors. As was
mentioned in the first example
covering Deferreds, errbacks are passed an error. In the previous
example, the _responseFailed
errback accepted this error
as a parameter but ignored it. The only way this example will differ
is that this _responseFailed
will use that error
parameter to log a message.
This example will require all of the imports required by the previous example plus one new import:
1
from twisted.python.log import err
The only other part of the previous example which changes is
the _responseFailed
callback, which will now log the
error passed to it:
1 2 3 4
... def _responseFailed(self, failure, call): call.cancel() err(failure, "Async response demo interrupted response")
We're passing two arguments to err
here. The first is the error which is being
passed in to the callback. This is always an object of type Failure
, a class which represents an
exception and (sometimes, but not always) a traceback. err
will
format this nicely for the log. The second argument is a descriptive string that
tells someone reading the log what the source of the error was.
Here's the full example with the two above modifications:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20
from twisted.web.resource import Resource from twisted.web.server import NOT_DONE_YET from twisted.internet import reactor from twisted.python.log import err class DelayedResource(Resource): def _delayedRender(self, request): request.write("Sorry to keep you waiting.") request.finish() def _responseFailed(self, failure, call): call.cancel() err(failure, "Async response demo interrupted response") def render_GET(self, request): call = reactor.callLater(5, self._delayedRender, request) request.notifyFinish().addErrback(self._responseFailed, call) return NOT_DONE_YET resource = DelayedResource()
Run this server as in the previous example and interrupt a request. Unlike the previous example, where the server gave no indication that this had happened, you'll see a message in the log output with this version.


Tony Fisher invented this puzzle in the mid-80s. It's a fun varient of the classic Rubik's Cube. Four of the six cut planes of the Rubik's Cube are simply rotated 45 degrees on an axis perpendicular to a face of the cube.
Start with the layer method, using the white or yellow face as the bottom layer. Solve the first two layers. The third layer is addressed next.
Note, of course, that you must take special care to orient the mid-layer centers (which look like corners), which is one obvious thing that differentiates this from the Rubik's Cube.
At this point we see the only significant reason for this puzzle being slightly harder and more interesting than a Rubik's Cube in that an odd number of edge peices may be flipped. (Remember that edge peices look like corner peices, and vice-versa. What I mean here are peices of the top layer equivilent to edge peices of the Rubik's Cube.)
We must have an even number of edge peices flipped in order to get zero of them flipped as per the usual steps involved in the layer method. The answer to this riddle is simply that one of the edge peices in the middle layer (which looks like a center) needs to be flipped. Since these edge peices look solved in either orientation, you're free to flip any such edge, and then continue with the solve. Doing so, you'll get an even number of mis-oriented edge peices in the top layer, (because edges must be flipped in pairs), and then you can finish the solve.
I go about this by simply bringing up any middle edge peice into the top layer, and then re-slotting it back to where it came from, but in the opposite orientation.


Bitmap display in font view.
Anti-Aliased (Greymap) display in font view.
At screen pixel sizes the rasterizer has trouble rendering some of the finer details, but with anti-alias turned on the results are much better. In the "H" below, the one on the left (bitmap) does not show the double horizontal bar of the H very well, while it is well rendered in the one on the right. The results are more extreme in the example above.
| ![](img/H-bm.png | ) |


Package algorithms.graphs
Class DegeneracyOrderingMatulaBeck
- java.lang.Object
-
- algorithms.graphs.DegeneracyOrderingMatulaBeck
-
public class DegeneracyOrderingMatulaBeck extends java.lang.Object
In graph theory, a k-degenerate graph is an undirected graph in which every subgraph has a vertex of degree at most k: that is, some vertex in the subgraph touches k or fewer of the subgraph's edges. The degeneracy of a graph is the smallest value of k for which it is k-degenerate. The degeneracy of a graph is a measure of how sparse it is, and is within a constant factor of other sparsity measures such as the arboricity of a graph.https://en.wikipedia.org/wiki/Degeneracy_(graph_theory)#Relation_to_other_graph_parameters
Degeneracy is also known as the k-core number, width, and linkage, and is essentially the same as the coloring number or Szekeres-Wilf number (named after Szekeres and Wilf (1968)). k-degenerate graphs have also been called k-inductive graphs. The degeneracy of a graph may be computed in linear time by an algorithm that repeatedly removes minimum-degree vertices. The connected components that are left after all vertices of degree less than k have been removed are called the k-cores of the graph and the degeneracy of a graph is the largest value k such that it has a k-core. As Matula and Beck (1983) describe, it is possible to find a vertex ordering of a finite graph G that optimizes the coloring number of the ordering, in linear time, by using a bucket queue to repeatedly find and remove the vertex of smallest degree.the runtime is O( (|V| + |E|) * log_2(w)) where w is maxDegree which is essentially O((|V| + |E|))
NOTE: for an undirected graph that is a simple undirected graph not a multigraph, the maximum possible number of edges |E|_max = C(|V|, 2) and the max possible degree of a vertex = |V|-1, and in that case |V| will not be less than a number whose maximum is |V|-1. This code does not at this time handle multigraphs, but the ability to store the structure needed for it is present. When the multigraph datastructure is used, the runtime complexity is O( (|V| + |E|) * log_2(|V|))- Author:
- nichole
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description (package private) static interface
DegeneracyOrderingMatulaBeck.IBucketQueue
(package private) static class
DegeneracyOrderingMatulaBeck.SBucketQueue
(package private) static class
DegeneracyOrderingMatulaBeck.TBucketQueue
-
Constructor Summary
Constructors Constructor Description DegeneracyOrderingMatulaBeck()
-
Method Summary
All Methods Static Methods Concrete Methods Modifier and Type Method Description protected static int
calculateMaxDegree(gnu.trove.map.TIntObjectMap<gnu.trove.set.TIntSet> adjMap)
static int
findDegeneracyOrder(gnu.trove.map.TIntObjectMap<gnu.trove.set.TIntSet> adjMap, int[] out)
following https://en.wikipedia.org/wiki/Degeneracy_(graph_theory)#Relation_to_other_graph_parameters
-
-
-
Method Detail
-
findDegeneracyOrder
public static int findDegeneracyOrder(gnu.trove.map.TIntObjectMap<gnu.trove.set.TIntSet> adjMap, int[] out)
following https://en.wikipedia.org/wiki/Degeneracy_(graph_theory)#Relation_to_other_graph_parametersthe runtime is O( (|V| + |E|) * log_2(w)) where w is maxDegree which is essentially O((|V| + |E|))
- Parameters:
adjMap
- an undirected graph as an adjacency map with key=vertex index, value = set of indexes of vertexes for the neighbors of the key. note: the method expects that the adjacency map has a key for every vertex listed in the values.out
- output array of size |V|- Returns:
- the degeneracy of the graph.
-
calculateMaxDegree
protected static int calculateMaxDegree(gnu.trove.map.TIntObjectMap<gnu.trove.set.TIntSet> adjMap)
- Parameters:
adjMap
-- Returns:
-
-


Harry Styles announces new album and release date
Harry Styles has revealed the name and release date of his new album.
The One Direction heartthrob, 25, posted a message on Twitter saying: “FINE LINE. THE ALBUM. DEC 13.”
The eagerly awaited offering comes two years after the singer’s self-titled debut solo album.
Fans had been speculating that news was coming after Styles posted a message on Twitter asking: “Do you know who you are?”, with a link to a web page of the same name.
The page now asks fans to enter their names and then gives the message: “You are a fine line. TPWK. Love, H.”
Styles’s announcement sparked excitement among fans.
“AND THE LORD JUST ANSWERED MY PRAYERS,” one posted online, while another called it “a moment in history”.


Associate Board
Joining We All Code's Associate Board is an exciting opportunity for early- to mid-career professionals who want to contribute their time, talent, and treasure to We All Code's mission, while building professional networks and enhancing leadership skills.
Overview
The Associate Board provides an excellent opportunity for interested volunteers at an early stage in their careers to contribute to We All Code's mission on many levels (devoting time, treasure, talent) while building professional networks and enhancing leadership skills.
The work of the Associate Board will focus on the following guiding principles:
- Elevate the presence of We All Code across Chicago and enhance visibility for our programs;
- Raise funds and engage new potential donors to support the development of future leaders; and
- Create opportunities outside of the organization for engagement with young students.
Benefits of an Associate Board Membership
- Friend-raising and networking experience
- Leadership development experience and mentoring with the Board of Directors
- Mentoring opportunities
- Name recognition on Board invitations (when appropriate)
- Recognition in the organization's Annual Report
- Opportunities to enjoy special privileges such as behind-the-scenes tours and previews of new programs and initiatives
Membership Requirements
- A passion for building future leaders and a commitment to developing students of courage, confidence and character.
- Personally donate $250 (give) and work to bring in additional $500 (get) through personal/professional networks throughout the year.
- Be an enthusiastic advocate for the mission of We All Code, especially among Chicago's young professional community.
- Attend at least 75% of scheduled meetings, though attendance at all meetings is strongly encouraged.
- Join an Associate Board committee.
- Support fundraising events. This would include at least two of the following:
- Secure monetary or in-kind donations.
- Purchase at least one ticket and attend the event(s)
- Make a personal financial donation towards the event if unable to attend
- Purchase raffle tickets, silent auction items, etc. (if applicable)
- Engage personal and professional networks and/or companies to support the organization at-large and Associate Board-specific events.
- Commit to building students of courage, confidence and character, who make the world a better place and be passionate about developing future leaders.
The Associate Board currently consists of approximately 15 members. We aspire to grow while keeping membership limited. Our target members are professionals, entrepreneurs, and civic leaders in the first 5-10 years of their careers. Membership on the Associate Board is open to anyone who is passionate about We All Code's mission and interested in supporting the work we do.
Fundraising Goal
Each year, the Associate Board works with its liaison(s) from the Board of Directors to establish a fundraising goal for the fall event in addition to the Associate Board give/get requirements.
Associate Board Committees
Outreach - The Associate Board Outreach Committee works to increase the reach of We All Code, build a network/pipeline, and ensure that multiple dimensions of We All Code are represented.
Fundraising - The Associate Board Fundraising Committee uses creativity and connections, with a We All Code focus, to lead the annual fall event. This Committee focuses on leading the full Associate Board through the process of securing sponsorships, selling tickets, securing silent auction items, and creating an event that is engaging and mission-oriented.
Volunteer - The Associate Board Volunteer Committee works to create opportunities that engage the Associate Board members with the mission of the organization in a hands-on, meaningful way that also creates social interaction with each other.
Questions?
Please contact us at<EMAIL_ADDRESS>for any questions or more information.
Apply to join the Associate Board
Don't miss this unique opportunity to give back to the Chicago community!


---
layout: post
title: balthasar neumann choir sketch
date: '2017-12-28T11:30:09+01:00'
categories:
- Sketches
- Sketchbooks
picture_url: https://film-Storyboards.tumblr.com/post/169041825351/balthasar-neumann-choir-sketch
---
Balthasar Neumann Choir & ensemble — from sketchbook.


MultiChoice - Multiple Choice generator
It's a script in VBScript used to generate exam documents based on multiple choice and free text questions
Download: MultiChoice_20090625a.rar
Instructions:
- Edit document templates at "Templates" folder. Unused test documents are prefixed with "~" char
- Clear output folder from old documents
- Navigate to Data folder
- Edit "OldQuestions.doc" to add any questions used in previous tests that you don't want to reuse (copy-paste the question text - text formatting isn't important)
- Edit multiple choice questions spreadsheet at "Data" folder. See existing sample there (mark unused questions with a * at the 1st column and mark correct answers with bold font)
- Edit Generate.vbs with Notepad
- to select how many questions to pick from spreadsheet's tab A, tab B and tab C
- to select how many shuffled versions of the multiple choice document to generate [one for each student group to avoid them copying from each other])
- to edit the length of the text that is used for spreadsheet questions to compare with old questions (from OldQuestions.doc) to see if it will be ignored
- to select whether a filled-in with answers document will also be generated
- to select whether comments from spreadsheet cells are shown at the generated answers document
- Drag-drop a questions spreadsheet (.xls file) onto the Generate.vbs script (need to have installed Windows Script Host [WSH] - it is preinstalled at recent Windows versions)
This will process all templates (apart the ones prefixed with ~) from "Templates" folder and will pick questions from the spreadsheet tabs to fill them in, ignoring any old questions. Results will be placed in "Output" folder. If you edit the script to generate a filled-in with answers document it will also generate one for each questions document generated.
Requirements: you must have Microsoft Word, Microsoft Excel and WSH (Windows Scripting Host) installed. If you don't have WSH, you can download WSH from Microsoft
(C)opyright 2009 - Zoomicon / George Birbilis
Free to use / give due credit


Abstract. This document demonstrates DocOnce with English text [1].
First heading: we're calculating a bit
Problem 1: Add two numbers
Project 2: Multiply two numbers
Even more advanced mathematics
Second heading: We look at video and picture
References
Today's first training is \( 0+0 \). It does not give much training...
Calculate \( 1+2 \).
3.
Simply count with fingers: one finger, two fingers, count to three fingers alltogether.
Filename: add
.
Calulate \( 3\cdot 4 \).
The exercise can be be calculated with aid of a calculator.
Filename: multiply
.
Actually, \( 3\cdot 4 = 4\cdot 3 \).
We look at the world's most famous equation.
YouTube film.


If pos is 4 and currentSize is 7, trace this code that removes an item:
int[] values = {10, 20, 30, 40, 50, 60, 70}; for (int i = pos + 1; i < currentSize; i++) { values[i - 1] = values[i]; }
What is the array after the code executes?
There are no hints for this question


With a relational interpreter you can run normal scheme functions "backwards" by grounding the output and leaving the inputs fresh. The interpreter will then produce the inputs for the given output.
By setting a programs input to also be it's output, you create a program which returns itself, known as a quine.
We can also create twines, which are two programs that produce the other. We make each program the output of each other and make sure they are different with a disequality constraint (otherwise we would just get two quines).
Now go make some more!


| Home | Libraries | People | FAQ | More |
This tutorial progresses through the basic usage of the library, demonstrating how to use a monotonic allocator with STL containers, how to use monotonic storage directly without an allocator, how to use regions and access tags, and finally demonstrates the use of the supplied container library with stack-based local storage.
The following is a very quick introduction to Boost.Monotonic:
#include <boost/monotonic/allocator.hpp> using namespace boost; int main() { { std::list<int, monotonic::allocator<int> > list; for (size_t n = 0; n < 1000; ++n) list.push_back(n); } monotonic::static_storage<>::release(); return 0; }
Here we have created a std::list
using a monotonic allocator. While we add new elements to the list in the
for-loop, allocation is coming from storage in the default region with default
access. The first 32k of allocation will come from the BSS segment embedded
in the application image (the amount of such storage is configurable), then
once that local storage is exhausted, later allocation requests will be serviced
from the heap. Since de-allocation does nothing in a monotonic allocator,
we must manually release the resources once we are finished, as shown above.
While this example is trivial, if you were to benchmark it against using
a default std::allocator
you will find that monotonic
allocation is much faster. In those tables, all factors are normalised. So a number less than one means this system is slower, and a number greater than one means this system is faster. The metric used for normalisation is in the data.
This is one of the main reasons for using this library; to provide efficient storage and allocation for temporary containers.
We shall now move on to some more interesting examples, including how to use multiple containers that share the same strorage, using regions, using local stack-based storage, and dealing with threading issues.
In this example, we create a map of ints to vectors of ints, with each container using a monotonic allocator:
int main() { { typedef std::vector<int, monotonic::allocator<int> > Vector; typedef std::map<int, Vector, std::less<int>, monotonic::allocator<Vector> > Map; Map map; for (size_t n = 0; n < 10000; ++n) { map[rand()%100].push_back(n); } } monotonic::static_storage<>::release(); return 0; };
Again, storage will only ever increase, so we must release it after we have finished using it.
Benchmarking the performance of this against other allocation schemes[2] show that monotonic allocation is extremely fast and efficient.
The key point here is that you can use a monotonic::allocator
anywhere that you would otherwise use a std::allocator
or any other STL-compliant custom allocator. Monotonic allocators of the
same type are effectively stateless, and may be default-constructed, used,
and discarded as needed.
We will deal with stateful monotonic allocators that can use local stack-based storage in a later section.
While it can be useful to have one storage area for all allocations, at times
will will want to segment our memory usage into different regions.
This is done by passing a user-supplied region tag type
to the type signature of a monotonic::allocator
,
as shown here:
struct my_region_A { }; struct my_region_B { }; int main() { { std::list<int, monotonic::allocator<int, my_region_A> > A_list; A_list.push_back(1); { std::list<int, monotonic::allocator<int, my_region_B> > B_list; B_list.push_back(2); } monotonic::static_storage<my_region_B>::release(); A_list.push_back(3); } monotonic::static_storage<my_region_A>::release(); return 0; }
Here, we have defined two storage regions, designated with the type-tags
my_region_A
and my_region_B
. These are passed as the second
type argument to a monotonic::allocator
in order to segment out the storage used. These regions are independant of
each other; releasing storage for B_list
does not effect the storage for A_list
.
Using segmented storage systems helps with logical seperation of resource usage amoung different sub-systems within an application. It also helps with ensuring privacy when using local storage, as demonstrated below:
class System { struct region {}; typedef std::vector<Object, monotonic::allocator<Object, region> > Objects; public: void update() { { Objects objects; GatherRelevant(objects); Process(objects); Update(objects); } // reset storage, ready for next update monotonic::static_storage<region>::reset(); } };
We have used a private region-tag region
to guarantee that storage used by local containers such as Objects
is not shared with any other system.
Note that this is a typical use-case for monotonic allocation, as it uses a locally defined container which is populated, used and discarded regularly.
While monotonic allocators use monotonic storage, we can also use this storage
directly and wherever we want efficient resource management. Using a monotonic::stack<>
gives you a first-class C++ stack which you can use at will, pass as an argument
or return as a result
[3]
.
The general usage pattern is:
monotonic::stack<Size> stack; { T0 &t0 = stack.push<T0>(..args..); T1 &t1 = stack.push<T1>(..args..); .... Tn &tn = stack.push<Tn>(..args..); stack.pop(); stack.pop(); ... }
Objects are created in-place using emplace semantics.
You just provide the type and construction arguments - your object will be
either on the stack or the heap and you needn't worry either way. Objects
are not copied, which means you can safely use types
that do not have default constructors or assignment overloads with stack<>
.
All objects pushed onto the stack<>
are destroyed when the stack leaves
scope - there is no need to pop them all explicitly. New objects can be added
between push
and pop
.
You can set the amount of C++ machine stack to use by saying stack<num_bytes>
.The
default inline size of a stack<>
object is defined as boost::monotonic::DefaltSizes::InlineSize
.
We can use a stack<>
as a platform-independant alloca(size)
by pushing an array of bytes, by using stack.push<char [N]>
or stack.push<boost::array<char, N> >
or more generally stack.push_array<Ty, N>
.
When we call stack.pop()
,
the last value added to the stack is destroyed and the stack pointer is set
to the end of the previous object on the stack. Objects are added using correct
machine alignment. Calling pop
on an empty stack throws an empty_stack
exception.
| Note | |
|---|---|
It is best practise to open a new statement block before using a |
We can also iterate over the stack, get the stack size, and clear the stack:
typedef monotonic::stack<> Stack; Stack stack; { ... add objects to the stack ... array<char, 1000> &bytes = stack.push_array<char, 1000>(); // number of elements on the stack size_t size = stack.size(); // number of bytes used size_t used_bytes = stack.bytes_used(); // iterate over heterogenous elements Stack::const_iterator elem = stack.begin(), end = stack.end(); for (; elem != end; ++elem) { cout << elem->get_type().name() << endl; if (elem->is_type<int>()) { int num = elem->get<int>(); cout << num << endl; } } // stacks are first-class objects and can be copied, passed // as arguments and returned as results Stack copy = stack; }
monotonic::stack<>
is just like your very own C++ stack which you can share between objects
and functions and even across process boundaries, independantly of the underlying
machine-based stack. They can be copied and compared and iterated over.
| Warning | |
|---|---|
Copying |
Unlike the C++ stack, storage for a stack<>
will use the heap when its local
inline stack-based buffer is exhuasted. This makes it ideal for local buffers
that will generally be small enough to fit onto the stack, but with the fallback
safety of transparently using the heap to service later requests for the
cases where that inline buffer is not large enough. This is especially useful
in recursive functions, which can be readily re-written to use a monotonic::stack<>
and thus be divorced from the limitations of the C++ stack.
| Note | |
|---|---|
When a |
You can use monotonic::enter
to localise usage of a stack:
template <class Stack> void UseStack(Stack &stack) { monotonic::enter local(stack); }
This ensures that the stack leaves in the same state that it entered, by
pop
ping until the stack is
balanced. If the stack is smaller when local
leaves scope than when it entered scope, it will throw boost::monotonic::uneven_stack
.


{% load static %}
c/s
3pm-6pm
Monday to Friday
contact
070-7781-1005
<EMAIL_ADDRESS>AYoung Kim
2014-GyeonggiAnyang-00221
1233774586
About
Terms & Conditions
Privacy Policy
@ayoungcompany.All Right
Reserved.


NCAA Men's Basketball Tourney Predictor
A website that utilizes past results between seeds to create a random bracket based on probability.


Since we use the URL hash to preserve Back button behavior, using page anchors to jump down to a position on the page isn't supported by using the traditional anchor link (#foo). This feature is slated for 1.4, but until then, you can use the silentScroll
method to scroll to a particular Y position without triggering scroll event listeners. You can pass in a yPos
argument to scroll to that Y location.
Here is an example of how to scroll to a position:
//scroll to Y 300px
$.mobile.silentScroll(300);
All Questions & Answers


/dev/blog
Bez Hermoso, Software Engineer @ Square
As the day gets busier, a tmux
session could really need some little re-organization. To tidy things a bit, you can move a pane from one crowded window to another using join-pane
.
It requires two steps:
- break the pane out via
break-pane
. This is bound to<prefix> !
by default. - Execute this in the
tmux
command-line::join-pane -t <int>
, where<int>
is the index of the window you want to move it into. You can optionally specify-h
or-v
to explicitly telltmux
to attach the current pane as a horizontal-split or a vertical-split on the target window, respectively.
For more info, consult
man tmux
.


{{> head}}
Strand is a growing library of common UI widgets built as web components. Strand components are cohesive in look and feel and designed to be interoperable. We've built Strand atop Google's Polymer project.
Strand is for developers who want to quickly mock up an application, or who want to get an 'out-of-the-box' user interface up and running with minimal effort.
Web components are the future of web application development. Web components offer logic and styling encapsulation, which removes boilerplate from your application. Each Strand component is designed with intent to separate component behavior from the underlying data as much as possible.
Polymer provides essential sugar as well as 2 way binding to increase developer velocity and reduce boilerplate.


--- layout: post title: How to enable php gmp on Mac OS X without macports categories: - Mac - PHP tags: - gmp - mac - PHP published: false comments: true ---
If you are using macports, you can easily install the package of "php-gmp".
But if you are a user of homebrew like me, you may need these tips.
First, you have to install gmp via homebrew, but it will give you gmp 5.0.1, which doesn't work with PHP 5.3
So you have to modify your Formula, go to /usr/local/Library/Formula/gmp.rb and modify:
url 'ftp://ftp.gnu.org/gnu/gmp/gmp-5.0.1.tar.bz2'
sha1 '6340edc7ceb95f9015a758c7c0d196eb0f441d49'
to
url 'ftp://ftp.gmplib.org/pub/gmp-4.3.2/gmp-4.3.2.tar.bz2'
sha1 'c011e8feaf1bb89158bd55eaabd7ef8fdd101a2c'
Now, you can run
brew install gmp
to install gmp.
Next step, download the php source code from php.net, we will need to build a php_gmp.so module from it.


Oil Technical Analysis: WTI challenges weekly highs near $58.00 a barrel
by Flavio Tosti- After ranging throughout the week, crude oil is accelerating towards the 58.00 handle.
- The level to beat for bulls is the 58.00 resistance.
Crude oil daily chart
The crude oil West Texas Intermediate (WTI) is currently holding above $57.00 a barrel and the 200-day simple moving average (DMA). The market has been trading sideways throughout the first half of November.
Crude oil four-hour chart
WTI is trading above the main SMAs, keeping the bullish bias intact while above the 56.00 support level. Buyers are likely looking for a daily breakout above the 58.00 level to potentially drive WTI towards the 59.00 and 60.00 price levels.
Crude oil 30-minute chart
The market is challenging the weekly highs and the 58.00 figure while currently above the main SMAs. Support is seen at the 57.50 level followed by 57.00 and the 56.40 levels.
Additional key levels
WTI
| Overview | |
|---|---|
| Today last price | 57.94 |
| Today Daily Change | 0.95 |
| Today Daily Change % | 1.67 |
| Today daily open | 56.99 |
| Trends | |
|---|---|
| Daily SMA20 | 56.03 |
| Daily SMA50 | 55.76 |
| Daily SMA100 | 55.99 |
| Daily SMA200 | 57.52 |
| Levels | |
|---|---|
| Previous Daily High | 57.87 |
| Previous Daily Low | 56.72 |
| Previous Weekly High | 57.93 |
| Previous Weekly Low | 55.84 |
| Previous Monthly High | 56.97 |
| Previous Monthly Low | 51.19 |
| Daily Fibonacci 38.2% | 57.16 |
| Daily Fibonacci 61.8% | 57.43 |
| Daily Pivot Point S1 | 56.52 |
| Daily Pivot Point S2 | 56.04 |
| Daily Pivot Point S3 | 55.37 |
| Daily Pivot Point R1 | 57.67 |
| Daily Pivot Point R2 | 58.34 |
| Daily Pivot Point R3 | 58.82 |


All Classes and Interfaces
Class
Description
Skeleton implementation of a named axis.
An AbstractController is a skeleton implementation of a controller that
contains a fixed number of axes, controllers, and rumblers.
An axis is a single button, slider, or dial, which has a single range.
Identifiers for different Axes.
KeyIDs for standard PC (LATIN-1) keyboards
POV enum for different positions.
A Controller represents a physical device, such as a keyboard, mouse,
or joystick, or a logical grouping of related controls, such as a button
pad or mouse ball.
Common controller port types.
Types of controller objects.
A ControllerEnvironment represents a collection of controllers that are
physically or logically linked.
An event that is fired when the state of a controller changes
A listener for changes in the state of controllers
Combines the list of seperate keyboards and mice found with the raw plugin,
with the game controllers found with direct input.
DirectInput implementation of controller environment
A FIFO queue for input events.
A Keyboard is a type of controller consisting of a single controller,
they keypad, which contains several axes (the keys).
Environment plugin for linux
A Mouse is a type of controller consisting of two child controllers,
a ball and a button pad.
OSX HIDManager implementation
This is a marker interface used to mark plugins in a Jar file
for retrieval by the Plugins class.
This class is used internally by the Plugin system.
This is the application interface to the Plugin system.
DirectInput implementation of controller environment
A Rumbler is a controller's mechanism for delivering feedback
to the user through the device.
Generic Desktop Usages
The version and build number of this implementation.
The version and build number of this implementation.