Global Index

other

(1951 entries)

Notation Index

other

(146 entries)

Module Index

other

(66 entries)

Variable Index

other

(7 entries)

Library Index

other

(22 entries)

Lemma Index

other

(459 entries)

Constructor Index

other

(670 entries)

Axiom Index

other

(11 entries)

Inductive Index

other

(121 entries)

Section Index

other

(3 entries)

Abbreviation Index

other

(57 entries)

Definition Index

other

(389 entries)

Global Index

A

abs [constructor, in Sub]
abs [constructor, in Norm]
abs [constructor, in RecordSub]
abs_arrow [lemma, in Sub]
abs_arrow [lemma, in RecordSub]
aequiv [definition, in Equiv]
aequiv_example [lemma, in Equiv]
aeval_weakening [lemma, in Equiv]
Aexp [definition, in Hoare]
Aexp_of_aexp [definition, in Hoare]
Aexp_of_nat [definition, in Hoare]
afi_test3 [constructor, in Sub]
afi_test2 [constructor, in Sub]
afi_test1 [constructor, in Sub]
afi_abs [constructor, in Sub]
afi_app2 [constructor, in Sub]
afi_app1 [constructor, in Sub]
afi_var [constructor, in Sub]
afi_test2 [constructor, in Norm]
afi_test1 [constructor, in Norm]
afi_test0 [constructor, in Norm]
afi_snd [constructor, in Norm]
afi_fst [constructor, in Norm]
afi_pair2 [constructor, in Norm]
afi_pair1 [constructor, in Norm]
afi_abs [constructor, in Norm]
afi_app2 [constructor, in Norm]
afi_app1 [constructor, in Norm]
afi_var [constructor, in Norm]
afi_rtail [constructor, in RecordSub]
afi_rhead [constructor, in RecordSub]
afi_proj [constructor, in RecordSub]
afi_abs [constructor, in RecordSub]
afi_app2 [constructor, in RecordSub]
afi_app1 [constructor, in RecordSub]
afi_var [constructor, in RecordSub]
always_loop_hoare [lemma, in Hoare]
ap [definition, in Hoare]
app [constructor, in Sub]
app [constructor, in Norm]
app [constructor, in RecordSub]
appears_free_in [inductive, in Sub]
appears_free_in [inductive, in Norm]
appears_free_in [inductive, in RecordSub]
ap₂ [definition, in Hoare]
Arrow [constructor, in Sub]
Arrow [constructor, in Norm]
Arrow [constructor, in RecordSub]
assert [abbreviation, in Hoare]
Assertion [definition, in Hoare]
assert_of_Prop [definition, in Hoare]
assert_implies [definition, in Hoare]
Assign [constructor, in PE]
assign [definition, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
assn_sub_ex₂' [definition, in Hoare]
assn_sub_ex₁' [definition, in Hoare]
assn_sub_example2'' [definition, in Hoare]
assn_sub_example2' [definition, in Hoare]
assn_sub_example2 [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub [definition, in Hoare]
astep [inductive, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]

B

Base [constructor, in Sub]
Base [constructor, in RecordSub]
bassn [definition, in Hoare]
bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
bexp_eval_false [lemma, in Hoare]
bexp_eval_true [lemma, in Hoare]
Bib [library]
block [inductive, in PE]
body [constructor, in PE]
Bool [constructor, in Sub]
Bool [constructor, in Norm]
Bool [constructor, in Types]
bool_canonical [lemma, in Types]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
bstep [inductive, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq₂ [constructor, in Smallstep]
BS_Eq₁ [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
bvalue [inductive, in Types]
bv_fls [constructor, in Types]
bv_tru [constructor, in Types]

C

D

E

F

fib [definition, in Hoare2]
fib_eqn [lemma, in Hoare2]
find_parity_correct' [lemma, in Hoare2]
find_parity_dec' [definition, in Hoare2]
find_parity_correct [lemma, in Hoare2]
find_parity_dec [definition, in Hoare2]
find_parity [definition, in Hoare2]
FirstTry [module, in Typechecking]
FirstTry.type_check [definition, in Typechecking]
fls [constructor, in Sub]
fls [constructor, in Norm]
fls [constructor, in Types]
fold_constants_com_sound [lemma, in Equiv]
fold_constants_bexp_sound [lemma, in Equiv]
fold_constants_aexp_sound [lemma, in Equiv]
fold_com_ex₁ [definition, in Equiv]
fold_constants_com [definition, in Equiv]
fold_bexp_ex₂ [definition, in Equiv]
fold_bexp_ex₁ [definition, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_aexp_ex₂ [definition, in Equiv]
fold_aexp_ex₁ [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
free_in_context [lemma, in Sub]
free_in_context [lemma, in Norm]
free_in_context [lemma, in RecordSub]
fst [constructor, in Norm]

G

GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
Goto [constructor, in PE]
gt_not_le [axiom, in UseAuto]

H

I

K

keval [definition, in PE]
keval_example [definition, in PE]

L

M

manual_grade_for_products [definition, in Sub]
manual_grade_for_variations [definition, in Sub]
manual_grade_for_pair_permutation [definition, in Sub]
manual_grade_for_smallest_2 [definition, in Sub]
manual_grade_for_smallest_1 [definition, in Sub]
manual_grade_for_small_large_4 [definition, in Sub]
manual_grade_for_small_large_2 [definition, in Sub]
manual_grade_for_small_large_1 [definition, in Sub]
manual_grade_for_proper_subtypes [definition, in Sub]
manual_grade_for_subtype_concepts_tf [definition, in Sub]
manual_grade_for_subtype_instances_tf_2 [definition, in Sub]
manual_grade_for_subtype_order [definition, in Sub]
manual_grade_for_arrow_sub_wrong [definition, in Sub]
manual_grade_for_hoare_repeat [definition, in Hoare]
manual_grade_for_hoare_asgn_wrong [definition, in Hoare]
manual_grade_for_hoare_asgn_examples [definition, in Hoare]
manual_grade_for_combined_properties [definition, in Smallstep]
manual_grade_for_eval__multistep_inf [definition, in Smallstep]
manual_grade_for_equiv_classes [definition, in Equiv]
manual_grade_for_norm [definition, in Norm]
manual_grade_for_norm_fail [definition, in Norm]
manual_grade_for_rcd_types_match_informal [definition, in RecordSub]
manual_grade_for_factorial_dec [definition, in Hoare2]
manual_grade_for_check_defn_of_slow_assignment_dec [definition, in Hoare2]
manual_grade_for_decorations_in_two_loops [definition, in Hoare2]
manual_grade_for_decorations_in_Min_Hoare [definition, in Hoare2]
manual_grade_for_decorations_in_factorial [definition, in Hoare2]
manual_grade_for_decorations_in_slow_assignment [definition, in Hoare2]
manual_grade_for_decorations_in_if_minus_plus_reloaded [definition, in Hoare2]
manual_grade_for_prog_pres_bigstep [definition, in Types]
manual_grade_for_remove_predzro [definition, in Types]
manual_grade_for_variation2 [definition, in Types]
manual_grade_for_variation1 [definition, in Types]
manual_grade_for_subject_expansion [definition, in Types]
manual_grade_for_finish_preservation_informal [definition, in Types]
manual_grade_for_finish_progress_informal [definition, in Types]
mkAexp [abbreviation, in Hoare]
MoreStlc [library]
msubst [definition, in Norm]
msubst_R [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_abs [lemma, in Norm]
msubst_var [lemma, in Norm]
msubst_closed [lemma, in Norm]
multi [inductive, in Smallstep]
multistep [abbreviation, in Norm]
multistep [definition, in Types]
multistep__eval [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_congr_1 [lemma, in Smallstep]
multistep_App2 [lemma, in Norm]
multistep_preserves_R' [lemma, in Norm]
multistep_preserves_R [lemma, in Norm]
multi_trans [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_step [constructor, in Smallstep]
multi_refl [constructor, in Smallstep]
mupdate [definition, in Norm]
mupdate_drop [lemma, in Norm]
mupdate_lookup [lemma, in Norm]
myFact [definition, in UseAuto]

N

NaryExamples [module, in UseTactics]
NaryExamples.demo_branch [lemma, in UseTactics]
NaryExamples.demo_splits [lemma, in UseTactics]
Nat [constructor, in Types]
nat_le_refl [lemma, in UseAuto]
nat_canonical [lemma, in Types]
negation_study_2 [lemma, in UseAuto]
negation_study_1 [lemma, in UseAuto]
nf_same_as_value [lemma, in Smallstep]
nf_is_value [lemma, in Smallstep]
Norm [library]
normalization [lemma, in Norm]
normalize_ex' [lemma, in Smallstep]
normalize_ex [lemma, in Smallstep]
normalizing [definition, in Smallstep]
normal_forms_unique [lemma, in Smallstep]
normal_form_of [definition, in Smallstep]
normal_form [definition, in Smallstep]
nvalue [inductive, in Types]
nv_scc [constructor, in Types]
nv_zro [constructor, in Types]

O

omega_demo_4 [lemma, in UseAuto]
omega_demo_3 [lemma, in UseAuto]
omega_demo_2 [lemma, in UseAuto]
omega_demo_1 [lemma, in UseAuto]
order_matters_2 [lemma, in UseAuto]
order_matters_1 [lemma, in UseAuto]

P

P [axiom, in UseAuto]
P [constructor, in Smallstep]
pair [constructor, in Norm]
parity [definition, in PE]
parity [definition, in Hoare2]
parity_eval [definition, in PE]
parity_body [definition, in PE]
parity_label [inductive, in PE]
parity_correct [lemma, in Hoare2]
parity_lt_2 [lemma, in Hoare2]
parity_ge_2 [lemma, in Hoare2]
PE [library]
peval [inductive, in PE]
pe_program_correct [lemma, in PE]
pe_peval_intro [constructor, in PE]
pe_peval [inductive, in PE]
pe_program [definition, in PE]
pe_block_correct [lemma, in PE]
pe_block_example [definition, in PE]
pe_block [definition, in PE]
pe_com_correct [lemma, in PE]
pe_com_sound [lemma, in PE]
pe_com_complete [lemma, in PE]
pe_ceval_intro [constructor, in PE]
pe_ceval [inductive, in PE]
pe_example3 [definition, in PE]
pe_example2 [definition, in PE]
pe_example1 [definition, in PE]
PE_If [constructor, in PE]
PE_IfFalse [constructor, in PE]
PE_IfTrue [constructor, in PE]
PE_Seq [constructor, in PE]
PE_AssDynamic [constructor, in PE]
PE_AssStatic [constructor, in PE]
PE_Skip [constructor, in PE]
pe_com [inductive, in PE]
pe_compare_update [lemma, in PE]
pe_compare_removes [lemma, in PE]
pe_removes_correct [lemma, in PE]
pe_removes [definition, in PE]
pe_compare_correct [lemma, in PE]
pe_compare [definition, in PE]
pe_unique_correct [lemma, in PE]
pe_unique [definition, in PE]
pe_disagree_domain [lemma, in PE]
pe_disagree_at [definition, in PE]
pe_update_update_add [lemma, in PE]
pe_update_update_remove [lemma, in PE]
pe_add_correct [lemma, in PE]
pe_add [definition, in PE]
pe_remove_correct [lemma, in PE]
pe_remove [definition, in PE]
pe_bexp_correct [lemma, in PE]
pe_bexp [definition, in PE]
pe_aexp_correct [lemma, in PE]
pe_consistent_update [lemma, in PE]
pe_update_consistent [lemma, in PE]
pe_update_correct [lemma, in PE]
pe_update [definition, in PE]
pe_aexp_correct_weak [lemma, in PE]
pe_consistent [definition, in PE]
pe_aexp [definition, in PE]
pe_domain [lemma, in PE]
pe_lookup [definition, in PE]
pe_state [definition, in PE]
post [definition, in Hoare2]
Postscript [library]
post_dec_while [definition, in Hoare2]
post_dec [definition, in Hoare2]
pow2 [definition, in Hoare2]
pow2_le_1 [lemma, in Hoare2]
pow2_plus_1 [lemma, in Hoare2]
prd [constructor, in Types]
Preface [library]
preservation [lemma, in Sub]
preservation [lemma, in Norm]
preservation [lemma, in RecordSub]
preservation [lemma, in Types]
PreservationProgressReferences [module, in UseAuto]
PreservationProgressReferences.nth_eq_last' [lemma, in UseAuto]
PreservationProgressReferences.preservation [lemma, in UseAuto]
PreservationProgressReferences.preservation_ref [lemma, in UseAuto]
PreservationProgressReferences.preservation' [lemma, in UseAuto]
PreservationProgressReferences.progress [lemma, in UseAuto]
PreservationProgressStlc [module, in UseAuto]
PreservationProgressStlc.preservation [lemma, in UseAuto]
PreservationProgressStlc.preservation' [lemma, in UseAuto]
PreservationProgressStlc.progress [lemma, in UseAuto]
PreservationProgressStlc.progress' [lemma, in UseAuto]
preservation' [lemma, in Types]
pre_dec_while [definition, in Hoare2]
pre_dec [definition, in Hoare2]
Prod [constructor, in Norm]
prog [definition, in Smallstep]
program [definition, in PE]
progress [lemma, in Sub]
progress [lemma, in RecordSub]
progress [lemma, in Types]
prog_i [definition, in Equiv]
prog_h [definition, in Equiv]
prog_g [definition, in Equiv]
prog_f [definition, in Equiv]
prog_e [definition, in Equiv]
prog_d [definition, in Equiv]
prog_c [definition, in Equiv]
prog_b [definition, in Equiv]
prog_a [definition, in Equiv]
provable_false_pre [lemma, in HoareAsLogic]
provable_true_post [lemma, in HoareAsLogic]

R

S

T

U

UnfoldsExample [module, in UseTactics]
UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
unit [constructor, in Sub]
Unit [constructor, in Sub]
UseAuto [library]
UseTactics [library]

V

vacuous_substitution [lemma, in Norm]
valid [definition, in HoareAsLogic]
value [inductive, in Sub]
value [inductive, in Smallstep]
value [inductive, in Norm]
value [inductive, in RecordSub]
value [definition, in Types]
value_is_nf [lemma, in Smallstep]
value_halts [lemma, in Norm]
value__normal [lemma, in Norm]
value_is_nf [lemma, in Types]
var [constructor, in Sub]
var [constructor, in Norm]
var [constructor, in RecordSub]
var_not_used_in_aexp [inductive, in Equiv]
vc_dec_while [definition, in Hoare2]
verification_correct_dec [lemma, in Hoare2]
verification_conditions_dec [definition, in Hoare2]
verification_correct [lemma, in Hoare2]
verification_conditions [definition, in Hoare2]
VNUId [constructor, in Equiv]
VNUMinus [constructor, in Equiv]
VNUMult [constructor, in Equiv]
VNUNum [constructor, in Equiv]
VNUPlus [constructor, in Equiv]
v_unit [constructor, in Sub]
v_false [constructor, in Sub]
v_true [constructor, in Sub]
v_abs [constructor, in Sub]
v_const [constructor, in Smallstep]
V_cons [constructor, in Norm]
V_nil [constructor, in Norm]
v_fls [constructor, in Norm]
v_tru [constructor, in Norm]
v_pair [constructor, in Norm]
v_abs [constructor, in Norm]
v_rcons [constructor, in RecordSub]
v_rnil [constructor, in RecordSub]
v_abs [constructor, in RecordSub]

W

well_formed_ty [inductive, in RecordSub]
wfArrow [constructor, in RecordSub]
wfBase [constructor, in RecordSub]
wfRCons [constructor, in RecordSub]
wfRNil [constructor, in RecordSub]
wfTop [constructor, in RecordSub]
wf_rcd_lookup [lemma, in RecordSub]
while_example [definition, in Hoare]
WHILE_true [lemma, in Equiv]
WHILE_true_nonterm [lemma, in Equiv]
WHILE_false [lemma, in Equiv]
working_of_auto_2 [lemma, in UseAuto]
working_of_auto_1 [lemma, in UseAuto]
wp [definition, in HoareAsLogic]
wp_invariant [lemma, in HoareAsLogic]
wp_seq [lemma, in HoareAsLogic]
wp_is_weakest [lemma, in HoareAsLogic]
wp_is_precondition [lemma, in HoareAsLogic]

Z

zprop [definition, in Equiv]
zprop_preserving [lemma, in Equiv]
zro [constructor, in Types]

other

Notation Index

C

_ / _ -->* _ / _ [in Smallstep]
_ / _ --> _ / _ [in Smallstep]
_ ;; _ [in Smallstep]
_ ::= _ [in Smallstep]
PAR _ WITH _ END [in Smallstep]
SKIP [in Smallstep]
TEST _ THEN _ ELSE _ FI [in Smallstep]
WHILE _ DO _ END [in Smallstep]
_ --> _ [in Smallstep]

H

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
HAVOC _ (imp_scope) [in Equiv]
TEST _ THEN _ ELSE _ FI (imp_scope) [in Equiv]
WHILE _ DO _ END (imp_scope) [in Equiv]
_ ;; _ (imp_scope) [in Equiv]
_ ::= _ (imp_scope) [in Equiv]
SKIP (imp_scope) [in Equiv]
_ =[ _ ]=> _ [in Hoare]
_ ;; _ [in Hoare]
_ ::= _ [in Hoare]
_ =[ _ ]=> _ [in Equiv]
HAVOC _ [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
_ ;; _ [in Hoare]
_ ::= _ [in Hoare]
ASSERT _ [in Hoare]
ASSUME _ [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]

I

{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
IF₁ _ THEN _ FI (imp_scope) [in Hoare]
TEST _ THEN _ ELSE _ FI (imp_scope) [in Hoare]
WHILE _ DO _ END (imp_scope) [in Hoare]
_ ::= _ (imp_scope) [in Hoare]
_ ;; _ (imp_scope) [in Hoare]
SKIP (imp_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]

L

_ / _ / _ / _ ==> _ # _ [in PE]
_ / _ ==> _ # _ [in PE]
_ / _ ==> _ / _ / _ [in PE]

R

_ =[ _ ]=> _ [in Hoare]
_ ::= _ [in Hoare]
_ ;; _ [in Hoare]
REPEAT _ UNTIL _ END [in Hoare]
SKIP [in Hoare]
TEST _ THEN _ ELSE _ FI [in Hoare]
WHILE _ DO _ END [in Hoare]
{{ _ }} _ {{ _ }} [in Hoare]

S

_ --> _ [in Smallstep]
_ ⊢ _ ∈ _ [in Records]
_ -->* _ [in Records]
_ --> _ [in Records]
[ _ := _ ] _ [in Records]
_ ⊢ _ ∈ _ [in MoreStlc]
_ -->* _ [in MoreStlc]
_ --> _ [in MoreStlc]
[ _ := _ ] _ [in MoreStlc]
_ / _ -->+ _ / _ [in References]
_ ; _ ⊢ _ ∈ _ [in References]
_ / _ -->* _ / _ [in References]
_ / _ --> _ / _ [in References]
[ _ := _ ] _ [in References]
_ ⊢ _ ∈ _ [in Stlc]
_ -->* _ [in Stlc]
_ --> _ [in Stlc]
[ _ := _ ] _ [in Stlc]

T

_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]

other

Module Index

C

CImp [in Smallstep]
Combined [in Smallstep]

D

DeterministicImp [in UseAuto]

E

EqualityExamples [in UseTactics]
Examples [in Sub]
Examples [in RecordSub]
ExamplesInstantiations [in UseTactics]
ExamplesLets [in UseTactics]
Examples2 [in Sub]
Examples2 [in RecordSub]
ExAssertions [in Hoare]
ExPrettyAssertions [in Hoare]

F

FirstTry [in Typechecking]

G

GenExample [in UseTactics]

H

Himp [in Hoare]
Himp [in Equiv]
Himp2 [in Hoare2]
HoareAssertAssume [in Hoare]

I

If₁ [in Hoare]
IntrovExamples [in UseTactics]
InvertsExamples [in UseTactics]

L

LibTacticsCompatibility [in LibTactics]
Loop [in PE]

N

NaryExamples [in UseTactics]

P

PreservationProgressReferences [in UseAuto]
PreservationProgressStlc [in UseAuto]

R

RepeatExercise [in Hoare]
RingDemo [in UseAuto]

S

T

Temp1 [in Smallstep]
Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp4.Temp5 [in Smallstep]
TypecheckerExtensions [in Typechecking]

U

UnfoldsExample [in UseTactics]

Variable Index

E

equatesLemma.A0 [in LibTactics]
equatesLemma.A1 [in LibTactics]
equatesLemma.A2 [in LibTactics]
equatesLemma.A3 [in LibTactics]
equatesLemma.A4 [in LibTactics]
equatesLemma.A5 [in LibTactics]
equatesLemma.A6 [in LibTactics]

Library Index

B

Bib

E

Equiv

H

Hoare
HoareAsLogic
Hoare2

L

LibTactics

M

MoreStlc

N

Norm

P

PE
Postscript
Preface

R

Records
RecordSub
References

S

Smallstep
Stlc
StlcProp
Sub

T

Typechecking
Types

U

UseAuto
UseTactics

Lemma Index

A

abs_arrow [in Sub]
abs_arrow [in RecordSub]
aequiv_example [in Equiv]
aeval_weakening [in Equiv]
always_loop_hoare [in Hoare]
assign_aequiv [in Equiv]
assign_removes [in PE]

B

bequiv_example [in Equiv]
bexp_eval_false [in Hoare]
bexp_eval_true [in Hoare]
bool_canonical [in Types]

C

canonical_forms_of_Bool [in Sub]
canonical_forms_of_arrow_types [in Sub]
canonical_forms_of_arrow_types [in RecordSub]
CAss_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]
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 Sub]
context_invariance [in Norm]
context_invariance [in RecordSub]
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_dec_correct [in Hoare2]
dpow2_down_correct [in Hoare2]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]

E

EqualityExamples.demo_applys_eq_3 [in UseTactics]
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]
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]
ExamplesInstantiations.substitution_preserves_typing [in UseTactics]
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

fib_eqn [in Hoare2]
find_parity_correct' [in Hoare2]
find_parity_correct [in Hoare2]
fold_constants_com_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_aexp_sound [in Equiv]
free_in_context [in Sub]
free_in_context [in Norm]
free_in_context [in RecordSub]

G

GenExample.substitution_preserves_typing [in UseTactics]

H

I

identity_assignment [in Equiv]
iff_intro_swap [in LibTactics]
iff_trans [in Equiv]
if_minus_plus [in Hoare]
If₁.hoare_if1_good [in Hoare]
If₁.hoare_asgn [in Hoare]
If₁.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

lookup_field_in_value [in RecordSub]
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]
l₁ [in Hoare2]
l₂ [in Hoare2]
l₃ [in Hoare2]
l₃' [in Hoare2]
l₄ [in Hoare2]

M

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]
nat_canonical [in Types]
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

omega_demo_4 [in UseAuto]
omega_demo_3 [in UseAuto]
omega_demo_2 [in UseAuto]
omega_demo_1 [in UseAuto]
order_matters_2 [in UseAuto]
order_matters_1 [in UseAuto]

P

R

rcd_types_match [in RecordSub]
reduce_to_zero_correct''' [in Hoare2]
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

T

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]
value_is_nf [in Types]
verification_correct_dec [in Hoare2]
verification_correct [in Hoare2]

W

wf_rcd_lookup [in RecordSub]
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

abs [in Sub]
abs [in Norm]
abs [in RecordSub]
afi_test3 [in Sub]
afi_test2 [in Sub]
afi_test1 [in Sub]
afi_abs [in Sub]
afi_app2 [in Sub]
afi_app1 [in Sub]
afi_var [in Sub]
afi_test2 [in Norm]
afi_test1 [in Norm]
afi_test0 [in Norm]
afi_snd [in Norm]
afi_fst [in Norm]
afi_pair2 [in Norm]
afi_pair1 [in Norm]
afi_abs [in Norm]
afi_app2 [in Norm]
afi_app1 [in Norm]
afi_var [in Norm]
afi_rtail [in RecordSub]
afi_rhead [in RecordSub]
afi_proj [in RecordSub]
afi_abs [in RecordSub]
afi_app2 [in RecordSub]
afi_app1 [in RecordSub]
afi_var [in RecordSub]
app [in Sub]
app [in Norm]
app [in RecordSub]
Arrow [in Sub]
Arrow [in Norm]
Arrow [in RecordSub]
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

Base [in Sub]
Base [in RecordSub]
body [in PE]
Bool [in Sub]
Bool [in Norm]
Bool [in Types]
boxer [in LibTactics]
BS_AndFalse [in Smallstep]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_AndStep [in Smallstep]
BS_AndTrueStep [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_Eq₂ [in Smallstep]
BS_Eq₁ [in Smallstep]
bv_fls [in Types]
bv_tru [in Types]

C

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]
ev_SS [in Hoare2]
ev_0 [in Hoare2]
E_Plus [in Smallstep]
E_Const [in Smallstep]
E_Some [in PE]
E_None [in PE]

F

fls [in Sub]
fls [in Norm]
fls [in Types]
fst [in Norm]

G

Goto [in PE]

H

I

If [in PE]
If₁.CAss [in Hoare]
If₁.CIf [in Hoare]
If₁.CIf1 [in Hoare]
If₁.CSeq [in Hoare]
If₁.CSkip [in Hoare]
If₁.CWhile [in Hoare]
If₁.E_WhileTrue [in Hoare]
If₁.E_WhileFalse [in Hoare]
If₁.E_IfFalse [in Hoare]
If₁.E_IfTrue [in Hoare]
If₁.E_Seq [in Hoare]
If₁.E_Ass [in Hoare]
If₁.E_Skip [in Hoare]
iszro [in Types]

L

loop [in PE]
Loop.E'Ass [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_AssDynamic [in PE]
Loop.PE_AssStatic [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]

N

Nat [in Types]
nv_scc [in Types]
nv_zro [in Types]

P

P [in Smallstep]
pair [in Norm]
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_AssDynamic [in PE]
PE_AssStatic [in PE]
PE_Skip [in PE]
prd [in Types]
Prod [in Norm]

R

S

T

U

unit [in Sub]
Unit [in Sub]

V

var [in Sub]
var [in Norm]
var [in RecordSub]
VNUId [in Equiv]
VNUMinus [in Equiv]
VNUMult [in Equiv]
VNUNum [in Equiv]
VNUPlus [in Equiv]
v_unit [in Sub]
v_false [in Sub]
v_true [in Sub]
v_abs [in Sub]
v_const [in Smallstep]
V_cons [in Norm]
V_nil [in Norm]
v_fls [in Norm]
v_tru [in Norm]
v_pair [in Norm]
v_abs [in Norm]
v_rcons [in RecordSub]
v_rnil [in RecordSub]
v_abs [in RecordSub]

W

wfArrow [in RecordSub]
wfBase [in RecordSub]
wfRCons [in RecordSub]
wfRNil [in RecordSub]
wfTop [in RecordSub]

Z

zro [in Types]

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

subtype [in UseAuto]
subtype_trans [in UseAuto]
subtype_refl [in UseAuto]

T

typ [in UseAuto]

Inductive Index

A

appears_free_in [in Sub]
appears_free_in [in Norm]
appears_free_in [in RecordSub]
astep [in Smallstep]
aval [in Smallstep]

B

block [in PE]
Boxer [in LibTactics]
bstep [in Smallstep]
bvalue [in Types]

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

ev [in Hoare2]
eval [in Smallstep]

H

has_type [in Sub]
has_type [in Norm]
has_type [in RecordSub]
has_type [in Types]
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

If₁.ceval [in Hoare]
If₁.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]

N

nvalue [in Types]

P

parity_label [in PE]
peval [in PE]
pe_peval [in PE]
pe_ceval [in PE]
pe_com [in PE]

R

record_tm [in RecordSub]
record_ty [in RecordSub]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]

S

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 Sub]
tm [in Smallstep]
tm [in Norm]
tm [in RecordSub]
tm [in Types]
ty [in Sub]
ty [in Norm]
ty [in RecordSub]
ty [in Types]

V

value [in Sub]
value [in Smallstep]
value [in Norm]
value [in RecordSub]
var_not_used_in_aexp [in Equiv]

W

well_formed_ty [in RecordSub]

Section Index

D

DemoAbsurd1 [in UseAuto]

E

equatesLemma [in LibTactics]

H

HintsTransitivity [in UseAuto]

Abbreviation Index

A

assert [in Hoare]

E

Examples.A [in Sub]
Examples.A [in RecordSub]
Examples.B [in Sub]
Examples.B [in RecordSub]
Examples.C [in Sub]
Examples.C [in RecordSub]
Examples.Float [in Sub]
Examples.i [in RecordSub]
Examples.Integer [in Sub]
Examples.j [in RecordSub]
Examples.k [in RecordSub]
Examples.String [in Sub]
Examples.x [in Sub]
Examples.x [in RecordSub]
Examples.y [in Sub]
Examples.y [in RecordSub]
Examples.z [in Sub]
Examples.z [in RecordSub]

M

mkAexp [in Hoare]
multistep [in Norm]

S

Definition Index

A

aequiv [in Equiv]
Aexp [in Hoare]
Aexp_of_aexp [in Hoare]
Aexp_of_nat [in Hoare]
ap [in Hoare]
ap₂ [in Hoare]
Assertion [in Hoare]
assert_of_Prop [in Hoare]
assert_implies [in Hoare]
assign [in PE]
assigned [in PE]
assn_sub_ex₂' [in Hoare]
assn_sub_ex₁' [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 Sub]
context [in Norm]
context [in RecordSub]
ctrans_sound [in Equiv]
c₃ [in Equiv]
c₄ [in Equiv]

D

dec_while_triple_correct [in Hoare2]
dec_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_down [in Hoare2]
drop [in Norm]

E

empty_pe_state [in PE]
env [in Norm]
equiv_classes [in Equiv]
eq' [in LibTactics]
evalF [in Smallstep]
Examples.Employee [in Sub]
Examples.Person [in Sub]
Examples.Student [in Sub]
Examples.subtyping_example_2 [in Sub]
Examples.subtyping_example_1 [in Sub]
Examples.subtyping_example_0 [in Sub]
Examples.subtyping_example_4 [in RecordSub]
Examples.subtyping_example_3 [in RecordSub]
Examples.subtyping_example_2 [in RecordSub]
Examples.subtyping_example_1 [in RecordSub]
Examples.subtyping_example_0 [in RecordSub]
Examples.sub_employee_person [in Sub]
Examples.sub_student_person [in Sub]
Examples.TRcd_kj [in RecordSub]
Examples.TRcd_j [in RecordSub]
Examples2.trcd_kj [in RecordSub]
Examples2.typing_example_2 [in RecordSub]
Examples2.typing_example_1 [in RecordSub]
Examples2.typing_example_0 [in RecordSub]
example_proof [in HoareAsLogic]
ExAssertions.assn1 [in Hoare]
ExAssertions.assn2 [in Hoare]
ExAssertions.assn3 [in Hoare]
ExAssertions.assn4 [in Hoare]
ExPrettyAssertions.assn1 [in Hoare]
ExPrettyAssertions.assn2 [in Hoare]
ExPrettyAssertions.assn3 [in Hoare]
ExPrettyAssertions.assn4 [in Hoare]
ExPrettyAssertions.ex1 [in Hoare]
ExPrettyAssertions.ex2 [in Hoare]
ExPrettyAssertions.ex3 [in Hoare]
extract [in Hoare2]
extract_while_ex [in Hoare2]
extract_dec [in Hoare2]

F

fib [in Hoare2]
find_parity_dec' [in Hoare2]
find_parity_dec [in Hoare2]
find_parity [in Hoare2]
FirstTry.type_check [in Typechecking]
fold_com_ex₁ [in Equiv]
fold_constants_com [in Equiv]
fold_bexp_ex₂ [in Equiv]
fold_bexp_ex₁ [in Equiv]
fold_constants_bexp [in Equiv]
fold_aexp_ex₂ [in Equiv]
fold_aexp_ex₁ [in Equiv]
fold_constants_aexp [in Equiv]

H

halts [in Norm]
has_type_not [in Types]
has_type_1 [in Types]
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_triple [in Hoare]

I

if_example''' [in Hoare]
if_example'' [in Hoare]
if_example [in Hoare]
If₁.hoare_triple [in Hoare]
If₁.if1false_test [in Hoare]
If₁.if1true_test [in Hoare]
If₁.manual_grade_for_hoare_if₁ [in Hoare]
inb [in PE]
InvertsExamples.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

N

normalizing [in Smallstep]
normal_form_of [in Smallstep]
normal_form [in Smallstep]

P

parity [in PE]
parity [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]
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]
reduce_to_zero' [in Hoare2]
relation [in Smallstep]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.hoare_triple [in Hoare]
rm [in LibTactics]

S

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]
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]
tlookup [in RecordSub]
Tlookup [in RecordSub]
TypecheckerExtensions.eqb_ty [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_complete [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_sound [in Typechecking]
TypecheckerExtensions.type_check [in Typechecking]

V

valid [in HoareAsLogic]
value [in Types]
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

other

(1951 entries)

Notation Index

other

(146 entries)

Module Index

other

(66 entries)

Variable Index

other

(7 entries)

Library Index

other

(22 entries)

Lemma Index

other

(459 entries)

Constructor Index

other

(670 entries)

Axiom Index

other

(11 entries)

Inductive Index

other

(121 entries)

Section Index

other

(3 entries)

Abbreviation Index

other

(57 entries)

Definition Index

other

(389 entries)

This page has been generated by coqdoc