Volume 2: Programming Language Foundations

• Table of Contents
• Index
• Roadmap

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

:

_

(1933 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

:

_

(132 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

_

(66 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

_

(7 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

_

(22 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

_

(686 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

_

(457 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

_

(11 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

_

(123 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

_

(3 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

_

(55 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

_

(371 entries)

---

Global Index

A

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

B

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

C

C [constructor, in PLF.Smallstep]
canonical_forms_of_arrow_types [lemma, in PLF.RecordSub]
canonical_forms_of_arrow_types [lemma, in PLF.Sub]
canonical_forms_of_Bool [lemma, in PLF.Sub]
capprox [definition, in PLF.Equiv]
CAss_congruence [lemma, in PLF.Equiv]
cequiv [definition, in PLF.Equiv]
ceval_extensionality [lemma, in PLF.PE]
CIf_congruence [lemma, in PLF.Equiv]
CImp [module, in PLF.Smallstep]
CImp.CAss [constructor, in PLF.Smallstep]
CImp.CIf [constructor, in PLF.Smallstep]
CImp.cmultistep [definition, in PLF.Smallstep]
CImp.com [inductive, in PLF.Smallstep]
CImp.CPar [constructor, in PLF.Smallstep]
CImp.CSeq [constructor, in PLF.Smallstep]
CImp.CSkip [constructor, in PLF.Smallstep]
CImp.cstep [inductive, in PLF.Smallstep]
CImp.CS_Ass [constructor, in PLF.Smallstep]
CImp.CS_AssStep [constructor, in PLF.Smallstep]
CImp.CS_IfFalse [constructor, in PLF.Smallstep]
CImp.CS_IfStep [constructor, in PLF.Smallstep]
CImp.CS_IfTrue [constructor, in PLF.Smallstep]
CImp.CS_ParDone [constructor, in PLF.Smallstep]
CImp.CS_Par1 [constructor, in PLF.Smallstep]
CImp.CS_Par2 [constructor, in PLF.Smallstep]
CImp.CS_SeqFinish [constructor, in PLF.Smallstep]
CImp.CS_SeqStep [constructor, in PLF.Smallstep]
CImp.CS_While [constructor, in PLF.Smallstep]
CImp.CWhile [constructor, in PLF.Smallstep]
CImp.par_body_n [lemma, in PLF.Smallstep]
CImp.par_body_n__Sn [lemma, in PLF.Smallstep]
CImp.par_loop [definition, in PLF.Smallstep]
CImp.par_loop_any_X [lemma, in PLF.Smallstep]
CImp.par_loop_example_0 [definition, in PLF.Smallstep]
CImp.par_loop_example_2 [definition, in PLF.Smallstep]
-->'_x_'/'_x">CImp.::x_'/'_x_'-->'_x_'/'_x [notation, in PLF.Smallstep]
-->*'_x_'/'_x">CImp.::x_'/'_x_'-->*'_x_'/'_x [notation, in PLF.Smallstep]
CImp.::x_'::='_x [notation, in PLF.Smallstep]
CImp.::x_';;'_x [notation, in PLF.Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [notation, in PLF.Smallstep]
CImp.::'SKIP' [notation, in PLF.Smallstep]
CImp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [notation, in PLF.Smallstep]
closed [definition, in PLF.Norm]
closed_env [definition, in PLF.Norm]
cmin [definition, in PLF.Equiv]
cmin_minimal [lemma, in PLF.Equiv]
COIND [definition, in PLF.LibTactics]
Combined [module, in PLF.Smallstep]
Combined.C [constructor, in PLF.Smallstep]
Combined.fls [constructor, in PLF.Smallstep]
Combined.P [constructor, in PLF.Smallstep]
Combined.step [inductive, in PLF.Smallstep]
Combined.ST_If [constructor, in PLF.Smallstep]
Combined.ST_IfFalse [constructor, in PLF.Smallstep]
Combined.ST_IfTrue [constructor, in PLF.Smallstep]
Combined.ST_PlusConstConst [constructor, in PLF.Smallstep]
Combined.ST_Plus1 [constructor, in PLF.Smallstep]
Combined.ST_Plus2 [constructor, in PLF.Smallstep]
Combined.test [constructor, in PLF.Smallstep]
Combined.tm [inductive, in PLF.Smallstep]
Combined.tru [constructor, in PLF.Smallstep]
Combined.value [inductive, in PLF.Smallstep]
Combined.v_const [constructor, in PLF.Smallstep]
Combined.v_fls [constructor, in PLF.Smallstep]
Combined.v_tru [constructor, in PLF.Smallstep]
-->'_x">Combined.::x_'-->'_x [notation, in PLF.Smallstep]
compiler_is_correct [lemma, in PLF.Smallstep]
compiler_is_correct_statement [definition, in PLF.Smallstep]
congruence_demo_1 [lemma, in PLF.UseAuto]
congruence_demo_2 [lemma, in PLF.UseAuto]
congruence_demo_3 [lemma, in PLF.UseAuto]
congruence_demo_4 [lemma, in PLF.UseAuto]
congruence_example [definition, in PLF.Equiv]
context [definition, in PLF.Norm]
context [definition, in PLF.RecordSub]
context [definition, in PLF.Sub]
context_invariance [lemma, in PLF.Norm]
context_invariance [lemma, in PLF.RecordSub]
context_invariance [lemma, in PLF.Sub]
CSeq_congruence [lemma, in PLF.Equiv]
cstep [inductive, in PLF.Smallstep]
CS_Ass [constructor, in PLF.Smallstep]
CS_AssStep [constructor, in PLF.Smallstep]
CS_IfFalse [constructor, in PLF.Smallstep]
CS_IfStep [constructor, in PLF.Smallstep]
CS_IfTrue [constructor, in PLF.Smallstep]
CS_SeqFinish [constructor, in PLF.Smallstep]
CS_SeqStep [constructor, in PLF.Smallstep]
CS_While [constructor, in PLF.Smallstep]
ctrans_sound [definition, in PLF.Equiv]
CWhile_congruence [lemma, in PLF.Equiv]
c₃ [definition, in PLF.Equiv]
c3_c4_different [lemma, in PLF.Equiv]
c₄ [definition, in PLF.Equiv]

D

DCAsgn [constructor, in PLF.Hoare2]
DCIf [constructor, in PLF.Hoare2]
dcom [inductive, in PLF.Hoare2]
DCPost [constructor, in PLF.Hoare2]
DCPre [constructor, in PLF.Hoare2]
DCSeq [constructor, in PLF.Hoare2]
DCSkip [constructor, in PLF.Hoare2]
DCWhile [constructor, in PLF.Hoare2]
Decorated [constructor, in PLF.Hoare2]
decorated [inductive, in PLF.Hoare2]
dec0 [definition, in PLF.Hoare2]
dec1 [definition, in PLF.Hoare2]
dec_correct [definition, in PLF.Hoare2]
dec_while [definition, in PLF.Hoare2]
dec_while_correct [lemma, in PLF.Hoare2]
DemoAbsurd1 [section, in PLF.UseAuto]
demo_auto_absurd_1 [lemma, in PLF.UseAuto]
demo_auto_absurd_2 [lemma, in PLF.UseAuto]
demo_clears_all_and_clears_but [lemma, in PLF.LibTactics]
demo_false [lemma, in PLF.UseTactics]
demo_false [lemma, in PLF.UseAuto]
demo_false_arg [lemma, in PLF.UseTactics]
demo_hint_unfold_context_1 [lemma, in PLF.UseAuto]
demo_hint_unfold_context_2 [lemma, in PLF.UseAuto]
demo_hint_unfold_goal_1 [lemma, in PLF.UseAuto]
demo_hint_unfold_goal_2 [lemma, in PLF.UseAuto]
demo_tryfalse [lemma, in PLF.UseTactics]
deterministic [definition, in PLF.Smallstep]
DeterministicImp [module, in PLF.UseAuto]
DeterministicImp.ceval_deterministic [lemma, in PLF.UseAuto]
DeterministicImp.ceval_deterministic' [lemma, in PLF.UseAuto]
DeterministicImp.ceval_deterministic'' [lemma, in PLF.UseAuto]
DeterministicImp.ceval_deterministic''' [lemma, in PLF.UseAuto]
DeterministicImp.ceval_deterministic'''' [lemma, in PLF.UseAuto]
dfib [definition, in PLF.Hoare2]
dfib_correct [lemma, in PLF.Hoare2]
div_mod_dec [definition, in PLF.Hoare2]
div_mod_dec_correct [lemma, in PLF.Hoare2]
done [constructor, in PLF.PE]
dpow2_down [definition, in PLF.Hoare2]
dpow2_down_correct [lemma, in PLF.Hoare2]
drop [definition, in PLF.Norm]
duplicate_subst [lemma, in PLF.Norm]
dup_lemma [lemma, in PLF.LibTactics]

E

empty_pe_state [definition, in PLF.PE]
entry [constructor, in PLF.PE]
env [definition, in PLF.Norm]
EqualityExamples [module, in PLF.UseTactics]
EqualityExamples.big_expression_using [axiom, in PLF.UseTactics]
EqualityExamples.demo_applys_eq_1 [lemma, in PLF.UseTactics]
EqualityExamples.demo_applys_eq_2 [lemma, in PLF.UseTactics]
EqualityExamples.demo_applys_eq_3 [lemma, in PLF.UseTactics]
EqualityExamples.demo_fequals [lemma, in PLF.UseTactics]
EqualityExamples.demo_substs [lemma, in PLF.UseTactics]
EqualityExamples.mult_0_plus [lemma, in PLF.UseTactics]
EqualityExamples.mult_0_plus' [lemma, in PLF.UseTactics]
EqualityExamples.mult_0_plus'' [lemma, in PLF.UseTactics]
equality_by_auto [lemma, in PLF.UseAuto]
equatesLemma [section, in PLF.LibTactics]
equatesLemma.A0 [variable, in PLF.LibTactics]
equatesLemma.A1 [variable, in PLF.LibTactics]
equatesLemma.A2 [variable, in PLF.LibTactics]
equatesLemma.A3 [variable, in PLF.LibTactics]
equatesLemma.A4 [variable, in PLF.LibTactics]
equatesLemma.A5 [variable, in PLF.LibTactics]
equatesLemma.A6 [variable, in PLF.LibTactics]
equates_0 [lemma, in PLF.LibTactics]
equates_1 [lemma, in PLF.LibTactics]
equates_2 [lemma, in PLF.LibTactics]
equates_3 [lemma, in PLF.LibTactics]
equates_4 [lemma, in PLF.LibTactics]
equates_5 [lemma, in PLF.LibTactics]
equates_6 [lemma, in PLF.LibTactics]
Equiv [library]
equiv_classes [definition, in PLF.Equiv]
eq' [definition, in PLF.LibTactics]
ev [inductive, in PLF.Hoare2]
eval [inductive, in PLF.Smallstep]
evalF [definition, in PLF.Smallstep]
evalF_eval [lemma, in PLF.Smallstep]
eval_assign [lemma, in PLF.PE]
eval__multistep [lemma, in PLF.Smallstep]
ev_SS [constructor, in PLF.Hoare2]
ev_0 [constructor, in PLF.Hoare2]
Examples [module, in PLF.RecordSub]
Examples [module, in PLF.Sub]
ExamplesInstantiations [module, in PLF.UseTactics]
ExamplesInstantiations.substitution_preserves_typing [lemma, in PLF.UseTactics]
ExamplesLets [module, in PLF.UseTactics]
ExamplesLets.demo_lets_underscore [lemma, in PLF.UseTactics]
ExamplesLets.demo_lets_1 [lemma, in PLF.UseTactics]
ExamplesLets.demo_lets_2 [lemma, in PLF.UseTactics]
ExamplesLets.demo_lets_3 [lemma, in PLF.UseTactics]
ExamplesLets.demo_lets_4 [lemma, in PLF.UseTactics]
ExamplesLets.demo_lets_5 [lemma, in PLF.UseTactics]
ExamplesLets.typing_inversion_var [axiom, in PLF.UseTactics]
Examples.A [abbreviation, in PLF.RecordSub]
Examples.A [abbreviation, in PLF.Sub]
Examples.B [abbreviation, in PLF.Sub]
Examples.B [abbreviation, in PLF.RecordSub]
Examples.C [abbreviation, in PLF.Sub]
Examples.C [abbreviation, in PLF.RecordSub]
Examples.Employee [definition, in PLF.Sub]
Examples.Float [abbreviation, in PLF.Sub]
Examples.i [abbreviation, in PLF.RecordSub]
Examples.Integer [abbreviation, in PLF.Sub]
Examples.j [abbreviation, in PLF.RecordSub]
Examples.k [abbreviation, in PLF.RecordSub]
Examples.Person [definition, in PLF.Sub]
Examples.String [abbreviation, in PLF.Sub]
Examples.Student [definition, in PLF.Sub]
Examples.subtyping_example_0 [definition, in PLF.RecordSub]
Examples.subtyping_example_0 [definition, in PLF.Sub]
Examples.subtyping_example_1 [definition, in PLF.Sub]
Examples.subtyping_example_1 [definition, in PLF.RecordSub]
Examples.subtyping_example_2 [definition, in PLF.RecordSub]
Examples.subtyping_example_2 [definition, in PLF.Sub]
Examples.subtyping_example_3 [definition, in PLF.RecordSub]
Examples.subtyping_example_4 [definition, in PLF.RecordSub]
Examples.sub_employee_person [definition, in PLF.Sub]
Examples.sub_student_person [definition, in PLF.Sub]
Examples.TRcd_j [definition, in PLF.RecordSub]
Examples.TRcd_kj [definition, in PLF.RecordSub]
Examples.x [abbreviation, in PLF.RecordSub]
Examples.x [abbreviation, in PLF.Sub]
Examples.y [abbreviation, in PLF.RecordSub]
Examples.y [abbreviation, in PLF.Sub]
Examples.z [abbreviation, in PLF.RecordSub]
Examples.z [abbreviation, in PLF.Sub]
Examples2 [module, in PLF.RecordSub]
Examples2 [module, in PLF.Sub]
Examples2.trcd_kj [definition, in PLF.RecordSub]
Examples2.typing_example_0 [definition, in PLF.RecordSub]
Examples2.typing_example_1 [definition, in PLF.RecordSub]
Examples2.typing_example_2 [definition, in PLF.RecordSub]
ExAssertions [module, in PLF.Hoare]
ExAssertions.as1 [definition, in PLF.Hoare]
ExAssertions.as2 [definition, in PLF.Hoare]
ExAssertions.as3 [definition, in PLF.Hoare]
ExAssertions.as4 [definition, in PLF.Hoare]
ExAssertions.as5 [definition, in PLF.Hoare]
ExAssertions.as6 [definition, in PLF.Hoare]
extract [definition, in PLF.Hoare2]
extract_dec [definition, in PLF.Hoare2]
E_Const [constructor, in PLF.Smallstep]
E_None [constructor, in PLF.PE]
E_Plus [constructor, in PLF.Smallstep]
E_Some [constructor, in PLF.PE]

F

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

G

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

H

halts [definition, in PLF.Norm]
has_type [inductive, in PLF.Sub]
has_type [inductive, in PLF.RecordSub]
has_type [inductive, in PLF.Types]
has_type [inductive, in PLF.Norm]
has_type_not [definition, in PLF.Types]
has_type_1 [definition, in PLF.Types]
has_type__wf [lemma, in PLF.RecordSub]
Himp [module, in PLF.Hoare]
Himp [module, in PLF.Equiv]
Himp.CAsgn [constructor, in PLF.Hoare]
Himp.CAss [constructor, in PLF.Equiv]
Himp.cequiv [definition, in PLF.Equiv]
Himp.ceval [inductive, in PLF.Hoare]
Himp.ceval [inductive, in PLF.Equiv]
Himp.CHavoc [constructor, in PLF.Equiv]
Himp.CHavoc [constructor, in PLF.Hoare]
Himp.CIf [constructor, in PLF.Equiv]
Himp.CIf [constructor, in PLF.Hoare]
Himp.com [inductive, in PLF.Hoare]
Himp.com [inductive, in PLF.Equiv]
Himp.CSeq [constructor, in PLF.Equiv]
Himp.CSeq [constructor, in PLF.Hoare]
Himp.CSkip [constructor, in PLF.Equiv]
Himp.CSkip [constructor, in PLF.Hoare]
Himp.CWhile [constructor, in PLF.Hoare]
Himp.CWhile [constructor, in PLF.Equiv]
Himp.E_Ass [constructor, in PLF.Equiv]
Himp.E_Ass [constructor, in PLF.Hoare]
Himp.E_Havoc [constructor, in PLF.Hoare]
Himp.E_IfFalse [constructor, in PLF.Equiv]
Himp.E_IfFalse [constructor, in PLF.Hoare]
Himp.E_IfTrue [constructor, in PLF.Hoare]
Himp.E_IfTrue [constructor, in PLF.Equiv]
Himp.E_Seq [constructor, in PLF.Hoare]
Himp.E_Seq [constructor, in PLF.Equiv]
Himp.E_Skip [constructor, in PLF.Equiv]
Himp.E_Skip [constructor, in PLF.Hoare]
Himp.E_WhileFalse [constructor, in PLF.Hoare]
Himp.E_WhileFalse [constructor, in PLF.Equiv]
Himp.E_WhileTrue [constructor, in PLF.Equiv]
Himp.E_WhileTrue [constructor, in PLF.Hoare]
Himp.havoc_example1 [definition, in PLF.Equiv]
Himp.havoc_example2 [definition, in PLF.Equiv]
Himp.havoc_pre [definition, in PLF.Hoare]
Himp.hoare_havoc [lemma, in PLF.Hoare]
Himp.hoare_triple [definition, in PLF.Hoare]
Himp.manual_grade_for_Check_rule_for_HAVOC [definition, in PLF.Equiv]
Himp.pcopy [definition, in PLF.Equiv]
Himp.ptwice [definition, in PLF.Equiv]
Himp.ptwice_cequiv_pcopy [lemma, in PLF.Equiv]
Himp.pXY [definition, in PLF.Equiv]
Himp.pXY_cequiv_pYX [lemma, in PLF.Equiv]
Himp.pYX [definition, in PLF.Equiv]
Himp.p1 [definition, in PLF.Equiv]
Himp.p1_may_diverge [lemma, in PLF.Equiv]
Himp.p1_p2_equiv [lemma, in PLF.Equiv]
Himp.p2 [definition, in PLF.Equiv]
Himp.p2_may_diverge [lemma, in PLF.Equiv]
Himp.p3 [definition, in PLF.Equiv]
Himp.p3_p4_inequiv [lemma, in PLF.Equiv]
Himp.p4 [definition, in PLF.Equiv]
Himp.p5 [definition, in PLF.Equiv]
Himp.p5_p6_equiv [lemma, in PLF.Equiv]
Himp.p6 [definition, in PLF.Equiv]
Himp.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in PLF.Hoare]
Himp.:imp_scope:x_'::='_x [notation, in PLF.Equiv]
Himp.:imp_scope:x_';;'_x [notation, in PLF.Equiv]
Himp.:imp_scope:'HAVOC'_x [notation, in PLF.Equiv]
Himp.:imp_scope:'SKIP' [notation, in PLF.Equiv]
Himp.:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Equiv]
Himp.:imp_scope:'WHILE'_x_'DO'_x_'END' [notation, in PLF.Equiv]
Himp.::x_'::='_x [notation, in PLF.Hoare]
Himp.::x_';;'_x [notation, in PLF.Hoare]
Himp.::x_'=['_x_']=>'_x [notation, in PLF.Equiv]
Himp.::x_'=['_x_']=>'_x [notation, in PLF.Hoare]
Himp.::'HAVOC'_x [notation, in PLF.Hoare]
Himp.::'SKIP' [notation, in PLF.Hoare]
Himp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Hoare]
Himp.::'WHILE'_x_'DO'_x_'END' [notation, in PLF.Hoare]
Himp2 [module, in PLF.Hoare2]
Himp2.hoare_havoc_weakest [lemma, in PLF.Hoare2]
HintsTransitivity [section, in PLF.UseAuto]
Hoare [library]
HoareAsLogic [library]
HoareAssertAssume [module, in PLF.Hoare]
HoareAssertAssume.assert_assume_differ [lemma, in PLF.Hoare]
HoareAssertAssume.assert_assume_example [definition, in PLF.Hoare]
HoareAssertAssume.assert_implies_assume [lemma, in PLF.Hoare]
HoareAssertAssume.CAss [constructor, in PLF.Hoare]
HoareAssertAssume.CAssert [constructor, in PLF.Hoare]
HoareAssertAssume.CAssume [constructor, in PLF.Hoare]
HoareAssertAssume.ceval [inductive, in PLF.Hoare]
HoareAssertAssume.CIf [constructor, in PLF.Hoare]
HoareAssertAssume.com [inductive, in PLF.Hoare]
HoareAssertAssume.CSeq [constructor, in PLF.Hoare]
HoareAssertAssume.CSkip [constructor, in PLF.Hoare]
HoareAssertAssume.CWhile [constructor, in PLF.Hoare]
HoareAssertAssume.E_Ass [constructor, in PLF.Hoare]
HoareAssertAssume.E_AssertFalse [constructor, in PLF.Hoare]
HoareAssertAssume.E_AssertTrue [constructor, in PLF.Hoare]
HoareAssertAssume.E_Assume [constructor, in PLF.Hoare]
HoareAssertAssume.E_IfFalse [constructor, in PLF.Hoare]
HoareAssertAssume.E_IfTrue [constructor, in PLF.Hoare]
HoareAssertAssume.E_SeqError [constructor, in PLF.Hoare]
HoareAssertAssume.E_SeqNormal [constructor, in PLF.Hoare]
HoareAssertAssume.E_Skip [constructor, in PLF.Hoare]
HoareAssertAssume.E_WhileFalse [constructor, in PLF.Hoare]
HoareAssertAssume.E_WhileTrueError [constructor, in PLF.Hoare]
HoareAssertAssume.E_WhileTrueNormal [constructor, in PLF.Hoare]
HoareAssertAssume.hoare_asgn [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_consequence_post [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_consequence_pre [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_if [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_seq [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_skip [lemma, in PLF.Hoare]
HoareAssertAssume.hoare_triple [definition, in PLF.Hoare]
HoareAssertAssume.hoare_while [lemma, in PLF.Hoare]
HoareAssertAssume.RError [constructor, in PLF.Hoare]
HoareAssertAssume.result [inductive, in PLF.Hoare]
HoareAssertAssume.RNormal [constructor, in PLF.Hoare]
HoareAssertAssume.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in PLF.Hoare]
HoareAssertAssume.::x_'::='_x [notation, in PLF.Hoare]
HoareAssertAssume.::x_';;'_x [notation, in PLF.Hoare]
HoareAssertAssume.::x_'=['_x_']=>'_x [notation, in PLF.Hoare]
HoareAssertAssume.::'ASSERT'_x [notation, in PLF.Hoare]
HoareAssertAssume.::'ASSUME'_x [notation, in PLF.Hoare]
HoareAssertAssume.::'SKIP' [notation, in PLF.Hoare]
HoareAssertAssume.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Hoare]
HoareAssertAssume.::'WHILE'_x_'DO'_x_'END' [notation, in PLF.Hoare]
Hoare2 [library]
hoare_asgn [lemma, in PLF.Hoare]
hoare_asgn_example1 [definition, in PLF.Hoare]
hoare_asgn_example1' [definition, in PLF.Hoare]
hoare_asgn_example3 [definition, in PLF.Hoare]
hoare_asgn_example4 [definition, in PLF.Hoare]
hoare_asgn_fwd [lemma, in PLF.Hoare]
hoare_asgn_fwd_exists [lemma, in PLF.Hoare]
hoare_asgn_weakest [lemma, in PLF.Hoare2]
hoare_consequence [lemma, in PLF.Hoare]
hoare_consequence_post [lemma, in PLF.Hoare]
hoare_consequence_pre [lemma, in PLF.Hoare]
hoare_if [lemma, in PLF.Hoare]
hoare_post_true [lemma, in PLF.Hoare]
hoare_pre_false [lemma, in PLF.Hoare]
hoare_proof [inductive, in PLF.HoareAsLogic]
hoare_proof_complete [lemma, in PLF.HoareAsLogic]
hoare_proof_sound [lemma, in PLF.HoareAsLogic]
hoare_seq [lemma, in PLF.Hoare]
hoare_skip [lemma, in PLF.Hoare]
hoare_triple [definition, in PLF.Hoare]
hoare_while [lemma, in PLF.Hoare]
H_Asgn [constructor, in PLF.HoareAsLogic]
H_Consequence [constructor, in PLF.HoareAsLogic]
H_Consequence_post [lemma, in PLF.HoareAsLogic]
H_Consequence_pre [lemma, in PLF.HoareAsLogic]
H_If [constructor, in PLF.HoareAsLogic]
H_Post_True_deriv [lemma, in PLF.HoareAsLogic]
H_Pre_False_deriv [lemma, in PLF.HoareAsLogic]
H_Seq [constructor, in PLF.HoareAsLogic]
H_Skip [constructor, in PLF.HoareAsLogic]
H_While [constructor, in PLF.HoareAsLogic]

I

identity_assignment [lemma, in PLF.Equiv]
If [constructor, in PLF.PE]
iff_intro_swap [lemma, in PLF.LibTactics]
iff_trans [lemma, in PLF.Equiv]
If₁ [module, in PLF.Hoare]
If₁.CAss [constructor, in PLF.Hoare]
If₁.ceval [inductive, in PLF.Hoare]
If₁.CIf [constructor, in PLF.Hoare]
If₁.CIf1 [constructor, in PLF.Hoare]
If₁.com [inductive, in PLF.Hoare]
If₁.CSeq [constructor, in PLF.Hoare]
If₁.CSkip [constructor, in PLF.Hoare]
If₁.CWhile [constructor, in PLF.Hoare]
If₁.E_Ass [constructor, in PLF.Hoare]
If₁.E_IfFalse [constructor, in PLF.Hoare]
If₁.E_IfTrue [constructor, in PLF.Hoare]
If₁.E_Seq [constructor, in PLF.Hoare]
If₁.E_Skip [constructor, in PLF.Hoare]
If₁.E_WhileFalse [constructor, in PLF.Hoare]
If₁.E_WhileTrue [constructor, in PLF.Hoare]
If₁.hoare_if1_good [lemma, in PLF.Hoare]
If₁.hoare_triple [definition, in PLF.Hoare]
If₁.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in PLF.Hoare]
If₁.:imp_scope:x_'::='_x [notation, in PLF.Hoare]
If₁.:imp_scope:x_';;'_x [notation, in PLF.Hoare]
If₁.:imp_scope:'IF₁'_x_'THEN'_x_'FI' [notation, in PLF.Hoare]
If₁.:imp_scope:'SKIP' [notation, in PLF.Hoare]
If₁.:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Hoare]
If₁.:imp_scope:'WHILE'_x_'DO'_x_'END' [notation, in PLF.Hoare]
If₁.::x_'=['_x_']=>'_x [notation, in PLF.Hoare]
if_example [definition, in PLF.Hoare]
if_minus_correct [lemma, in PLF.Hoare2]
if_minus_dec [definition, in PLF.Hoare2]
if_minus_plus [lemma, in PLF.Hoare]
if_minus_plus_com [definition, in PLF.Hoare2]
if_minus_plus_correct [lemma, in PLF.Hoare2]
if_minus_plus_dec [definition, in PLF.Hoare2]
inb [definition, in PLF.PE]
inbP [lemma, in PLF.PE]
induct_height_max2 [lemma, in PLF.LibTactics]
inequiv_exercise [lemma, in PLF.Equiv]
inj_pair2 [axiom, in PLF.LibTactics]
instantiation [inductive, in PLF.Norm]
instantiation_domains_match [lemma, in PLF.Norm]
instantiation_drop [lemma, in PLF.Norm]
instantiation_env_closed [lemma, in PLF.Norm]
instantiation_R [lemma, in PLF.Norm]
IntrovExamples [module, in PLF.UseTactics]
IntrovExamples.ceval_deterministic [lemma, in PLF.UseTactics]
IntrovExamples.ceval_deterministic' [lemma, in PLF.UseTactics]
IntrovExamples.dist_exists_or [lemma, in PLF.UseTactics]
IntrovExamples.exists_impl [lemma, in PLF.UseTactics]
InvertsExamples [module, in PLF.UseTactics]
InvertsExamples.ceval_deterministic [lemma, in PLF.UseTactics]
InvertsExamples.ceval_deterministic' [lemma, in PLF.UseTactics]
InvertsExamples.skip_left [lemma, in PLF.UseTactics]
InvertsExamples.skip_left' [lemma, in PLF.UseTactics]
InvertsExamples.typing_nonexample_1 [definition, in PLF.UseTactics]
iszro [constructor, in PLF.Types]
is_wp [definition, in PLF.Hoare2]
is_wp_example [lemma, in PLF.Hoare2]

K

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

L

le_gt_false [axiom, in PLF.UseAuto]
le_not_gt [axiom, in PLF.UseAuto]
LibTactics [library]
LibTacticsCompatibility [module, in PLF.LibTactics]
lookup [definition, in PLF.Norm]
lookup_field_in_value [lemma, in PLF.RecordSub]
Loop [module, in PLF.PE]
loop [constructor, in PLF.PE]
Loop.ceval_count [inductive, in PLF.PE]
Loop.ceval_count_complete [lemma, in PLF.PE]
Loop.ceval_count_sound [lemma, in PLF.PE]
Loop.E'Ass [constructor, in PLF.PE]
Loop.E'IfFalse [constructor, in PLF.PE]
Loop.E'IfTrue [constructor, in PLF.PE]
Loop.E'Seq [constructor, in PLF.PE]
Loop.E'Skip [constructor, in PLF.PE]
Loop.E'WhileFalse [constructor, in PLF.PE]
Loop.E'WhileTrue [constructor, in PLF.PE]
Loop.PE_AssDynamic [constructor, in PLF.PE]
Loop.PE_AssStatic [constructor, in PLF.PE]
Loop.pe_ceval_count [inductive, in PLF.PE]
Loop.pe_ceval_count_intro [constructor, in PLF.PE]
Loop.pe_ceval_count_le [lemma, in PLF.PE]
Loop.pe_com [inductive, in PLF.PE]
Loop.pe_compare_nil_lookup [lemma, in PLF.PE]
Loop.pe_compare_nil_update [lemma, in PLF.PE]
Loop.pe_com_complete [lemma, in PLF.PE]
Loop.pe_com_correct [lemma, in PLF.PE]
Loop.pe_com_sound [lemma, in PLF.PE]
Loop.PE_If [constructor, in PLF.PE]
Loop.PE_IfFalse [constructor, in PLF.PE]
Loop.PE_IfTrue [constructor, in PLF.PE]
Loop.pe_loop_example1 [definition, in PLF.PE]
Loop.pe_loop_example2 [definition, in PLF.PE]
Loop.pe_loop_example3 [definition, in PLF.PE]
Loop.pe_loop_example4 [definition, in PLF.PE]
Loop.PE_Seq [constructor, in PLF.PE]
Loop.PE_Skip [constructor, in PLF.PE]
Loop.PE_While [constructor, in PLF.PE]
Loop.PE_WhileFalse [constructor, in PLF.PE]
Loop.PE_WhileFixed [constructor, in PLF.PE]
Loop.PE_WhileFixedEnd [constructor, in PLF.PE]
Loop.PE_WhileFixedLoop [constructor, in PLF.PE]
Loop.PE_WhileTrue [constructor, in PLF.PE]
Loop.square_loop [definition, in PLF.PE]
Loop.::x_'/'_x_'/'_x_'/'_x_'\\'_x_'#'_x [notation, in PLF.PE]
Loop.::x_'/'_x_'\\'_x_'#'_x [notation, in PLF.PE]
Loop.::x_'/'_x_'\\'_x_'/'_x_'/'_x [notation, in PLF.PE]
loop_unrolling [lemma, in PLF.Equiv]
ltac_database [definition, in PLF.LibTactics]
ltac_database_provide [lemma, in PLF.LibTactics]
ltac_database_token [constructor, in PLF.LibTactics]
Ltac_database_token [inductive, in PLF.LibTactics]
ltac_goal_to_discard [inductive, in PLF.LibTactics]
ltac_goal_to_discard_intro [constructor, in PLF.LibTactics]
ltac_int_to_nat [definition, in PLF.LibTactics]
ltac_Mark [inductive, in PLF.LibTactics]
ltac_mark [constructor, in PLF.LibTactics]
ltac_No_arg [inductive, in PLF.LibTactics]
ltac_no_arg [constructor, in PLF.LibTactics]
ltac_something [definition, in PLF.LibTactics]
ltac_something_eq [lemma, in PLF.LibTactics]
ltac_something_hide [lemma, in PLF.LibTactics]
ltac_something_show [lemma, in PLF.LibTactics]
ltac_tag_subst [definition, in PLF.LibTactics]
ltac_to_generalize [definition, in PLF.LibTactics]
ltac_Wild [inductive, in PLF.LibTactics]
ltac_wild [constructor, in PLF.LibTactics]
ltac_wilds [constructor, in PLF.LibTactics]
ltac_Wilds [inductive, in PLF.LibTactics]
l₁ [lemma, in PLF.Hoare2]
l₂ [lemma, in PLF.Hoare2]
l₃ [lemma, in PLF.Hoare2]
l₃' [lemma, in PLF.Hoare2]
l₄ [lemma, in PLF.Hoare2]

M

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

N

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

O

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

P

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

R

R [definition, in PLF.Norm]
rcd_types_match [lemma, in PLF.RecordSub]
rcons [constructor, in PLF.RecordSub]
RCons [constructor, in PLF.RecordSub]
real_fact [definition, in PLF.Hoare2]
Records [library]
RecordSub [library]
record_tm [inductive, in PLF.RecordSub]
record_ty [inductive, in PLF.RecordSub]
reduce_to_zero' [definition, in PLF.Hoare2]
reduce_to_zero_correct' [lemma, in PLF.Hoare2]
References [library]
refl_aequiv [lemma, in PLF.Equiv]
refl_bequiv [lemma, in PLF.Equiv]
refl_cequiv [lemma, in PLF.Equiv]
relation [definition, in PLF.Smallstep]
RepeatExercise [module, in PLF.Hoare]
RepeatExercise.CAsgn [constructor, in PLF.Hoare]
RepeatExercise.ceval [inductive, in PLF.Hoare]
RepeatExercise.CIf [constructor, in PLF.Hoare]
RepeatExercise.com [inductive, in PLF.Hoare]
RepeatExercise.CRepeat [constructor, in PLF.Hoare]
RepeatExercise.CSeq [constructor, in PLF.Hoare]
RepeatExercise.CSkip [constructor, in PLF.Hoare]
RepeatExercise.CWhile [constructor, in PLF.Hoare]
RepeatExercise.ex1_repeat [definition, in PLF.Hoare]
RepeatExercise.ex1_repeat_works [lemma, in PLF.Hoare]
RepeatExercise.E_Ass [constructor, in PLF.Hoare]
RepeatExercise.E_IfFalse [constructor, in PLF.Hoare]
RepeatExercise.E_IfTrue [constructor, in PLF.Hoare]
RepeatExercise.E_Seq [constructor, in PLF.Hoare]
RepeatExercise.E_Skip [constructor, in PLF.Hoare]
RepeatExercise.E_WhileFalse [constructor, in PLF.Hoare]
RepeatExercise.E_WhileTrue [constructor, in PLF.Hoare]
RepeatExercise.hoare_triple [definition, in PLF.Hoare]
RepeatExercise.::x_'::='_x [notation, in PLF.Hoare]
RepeatExercise.::x_';;'_x [notation, in PLF.Hoare]
RepeatExercise.::x_'=['_x_']=>'_x [notation, in PLF.Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [notation, in PLF.Hoare]
RepeatExercise.::'SKIP' [notation, in PLF.Hoare]
RepeatExercise.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [notation, in PLF.Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [notation, in PLF.Hoare]
RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in PLF.Hoare]
RingDemo [module, in PLF.UseAuto]
RingDemo.ring_demo [lemma, in PLF.UseAuto]
rm [definition, in PLF.LibTactics]
RNil [constructor, in PLF.RecordSub]
rnil [constructor, in PLF.RecordSub]
rproj [constructor, in PLF.RecordSub]
rtcons [constructor, in PLF.RecordSub]
RTcons [constructor, in PLF.RecordSub]
rtnil [constructor, in PLF.RecordSub]
RTnil [constructor, in PLF.RecordSub]
R_halts [lemma, in PLF.Norm]
R_typable_empty [lemma, in PLF.Norm]

S

sample_proof [definition, in PLF.HoareAsLogic]
scc [constructor, in PLF.Types]
scc_hastype_nat__hastype_nat [definition, in PLF.Types]
search_depth_0 [lemma, in PLF.UseAuto]
search_depth_1 [lemma, in PLF.UseAuto]
search_depth_3 [lemma, in PLF.UseAuto]
search_depth_4 [lemma, in PLF.UseAuto]
search_depth_5 [lemma, in PLF.UseAuto]
Semantics [module, in PLF.UseAuto]
Semantics.multistep_eval_ind [lemma, in PLF.UseAuto]
Semantics.multistep__eval [lemma, in PLF.UseAuto]
Semantics.multistep__eval' [lemma, in PLF.UseAuto]
Semantics.multistep__eval'' [lemma, in PLF.UseAuto]
seq_assoc [lemma, in PLF.Equiv]
silly1 [lemma, in PLF.Hoare]
silly2 [lemma, in PLF.Hoare]
silly2_eassumption [lemma, in PLF.Hoare]
silly2_fixed [lemma, in PLF.Hoare]
SimpleArith1 [module, in PLF.Smallstep]
SimpleArith1.step [inductive, in PLF.Smallstep]
SimpleArith1.ST_PlusConstConst [constructor, in PLF.Smallstep]
SimpleArith1.ST_Plus1 [constructor, in PLF.Smallstep]
SimpleArith1.ST_Plus2 [constructor, in PLF.Smallstep]
SimpleArith1.test_step_1 [definition, in PLF.Smallstep]
SimpleArith1.test_step_2 [definition, in PLF.Smallstep]
-->'_x">SimpleArith1.::x_'-->'_x [notation, in PLF.Smallstep]
SimpleArith2 [module, in PLF.Smallstep]
SimpleArith2.step_deterministic [lemma, in PLF.Smallstep]
SimpleArith3 [module, in PLF.Smallstep]
SimpleArith3.step_deterministic_alt [lemma, in PLF.Smallstep]
SkipExample [module, in PLF.UseTactics]
SkipExample.ceval_deterministic [lemma, in PLF.UseTactics]
SkipExample.demo_admits [lemma, in PLF.UseTactics]
SkipExample.mult_plus_0 [lemma, in PLF.UseTactics]
skip_left [lemma, in PLF.Equiv]
skip_right [lemma, in PLF.Equiv]
slow_assignment_dec [definition, in PLF.Hoare2]
slow_assignment_dec_correct [lemma, in PLF.Hoare2]
Smallstep [library]
snd [constructor, in PLF.Norm]
solved_by_jauto [lemma, in PLF.UseAuto]
solving_by_apply [lemma, in PLF.UseAuto]
solving_by_eapply [lemma, in PLF.UseAuto]
solving_by_reflexivity [lemma, in PLF.UseAuto]
solving_conj_goal [lemma, in PLF.UseAuto]
solving_conj_hyp [lemma, in PLF.UseAuto]
solving_conj_hyp' [lemma, in PLF.UseAuto]
solving_conj_hyp_forall [lemma, in PLF.UseAuto]
solving_conj_more [lemma, in PLF.UseAuto]
solving_disj_goal [lemma, in PLF.UseAuto]
solving_disj_hyp [lemma, in PLF.UseAuto]
solving_exists_goal [lemma, in PLF.UseAuto]
solving_exists_hyp [lemma, in PLF.UseAuto]
solving_tauto [lemma, in PLF.UseAuto]
some_term_is_stuck [definition, in PLF.Types]
SortExamples [module, in PLF.UseTactics]
SortExamples.ceval_deterministic [lemma, in PLF.UseTactics]
soundness [lemma, in PLF.Types]
sqrt_correct [lemma, in PLF.Hoare2]
sqrt_dec [definition, in PLF.Hoare2]
square_dec [definition, in PLF.Hoare2]
square_dec' [definition, in PLF.Hoare2]
square_dec'_correct [lemma, in PLF.Hoare2]
square_dec_correct [lemma, in PLF.Hoare2]
square_simpler_dec [definition, in PLF.Hoare2]
square_simpler_dec_correct [lemma, in PLF.Hoare2]
SS_Load [constructor, in PLF.Smallstep]
SS_Minus [constructor, in PLF.Smallstep]
SS_Mult [constructor, in PLF.Smallstep]
SS_Plus [constructor, in PLF.Smallstep]
SS_Push [constructor, in PLF.Smallstep]
stack [definition, in PLF.Smallstep]
stack_multistep [definition, in PLF.Smallstep]
stack_step [inductive, in PLF.Smallstep]
stack_step_deterministic [lemma, in PLF.Smallstep]
step [inductive, in PLF.Sub]
step [inductive, in PLF.Types]
step [inductive, in PLF.RecordSub]
step [inductive, in PLF.Smallstep]
step [inductive, in PLF.Norm]
StepFunction [module, in PLF.Typechecking]
StepFunction.complete_stepf [lemma, in PLF.Typechecking]
StepFunction.sound_stepf [lemma, in PLF.Typechecking]
StepFunction.stepf [definition, in PLF.Typechecking]
step_deterministic [lemma, in PLF.Norm]
step_deterministic [lemma, in PLF.Smallstep]
step_deterministic [lemma, in PLF.Types]
step_example1 [definition, in PLF.Smallstep]
step_example1' [definition, in PLF.Smallstep]
step_example1'' [definition, in PLF.Smallstep]
step_example1''' [definition, in PLF.Smallstep]
step_normalizing [lemma, in PLF.Smallstep]
step_normal_form [definition, in PLF.Smallstep]
step_normal_form [abbreviation, in PLF.Types]
step_normal_form [abbreviation, in PLF.Norm]
step_preserves_halting [lemma, in PLF.Norm]
step_preserves_R [lemma, in PLF.Norm]
step_preserves_record_tm [lemma, in PLF.RecordSub]
step_preserves_R' [lemma, in PLF.Norm]
step__eval [lemma, in PLF.Smallstep]
STLC [module, in PLF.Stlc]
Stlc [library]
STLCArith [module, in PLF.StlcProp]
STLCArith.abs [constructor, in PLF.StlcProp]
STLCArith.app [constructor, in PLF.StlcProp]
STLCArith.Arrow [constructor, in PLF.StlcProp]
STLCArith.const [constructor, in PLF.StlcProp]
STLCArith.manual_grade_for_stlc_arith [definition, in PLF.StlcProp]
STLCArith.mlt [constructor, in PLF.StlcProp]
STLCArith.Nat [constructor, in PLF.StlcProp]
STLCArith.prd [constructor, in PLF.StlcProp]
STLCArith.scc [constructor, in PLF.StlcProp]
STLCArith.test0 [constructor, in PLF.StlcProp]
STLCArith.tm [inductive, in PLF.StlcProp]
STLCArith.ty [inductive, in PLF.StlcProp]
STLCArith.var [constructor, in PLF.StlcProp]
STLCChecker [module, in PLF.Typechecking]
STLCChecker.type_check [definition, in PLF.Typechecking]
STLCChecker.type_checking_complete [lemma, in PLF.Typechecking]
STLCChecker.type_checking_sound [lemma, in PLF.Typechecking]
STLCExtended [module, in PLF.MoreStlc]
STLCExtendedRecords [module, in PLF.Records]
STLCExtendedRecords.A [abbreviation, in PLF.Records]
STLCExtendedRecords.a [abbreviation, in PLF.Records]
STLCExtendedRecords.abs [constructor, in PLF.Records]
STLCExtendedRecords.afi_abs [constructor, in PLF.Records]
STLCExtendedRecords.afi_app1 [constructor, in PLF.Records]
STLCExtendedRecords.afi_app2 [constructor, in PLF.Records]
STLCExtendedRecords.afi_proj [constructor, in PLF.Records]
STLCExtendedRecords.afi_rhead [constructor, in PLF.Records]
STLCExtendedRecords.afi_rtail [constructor, in PLF.Records]
STLCExtendedRecords.afi_var [constructor, in PLF.Records]
STLCExtendedRecords.app [constructor, in PLF.Records]
STLCExtendedRecords.appears_free_in [inductive, in PLF.Records]
STLCExtendedRecords.Arrow [constructor, in PLF.Records]
STLCExtendedRecords.B [abbreviation, in PLF.Records]
STLCExtendedRecords.Base [constructor, in PLF.Records]
STLCExtendedRecords.context [definition, in PLF.Records]
STLCExtendedRecords.context_invariance [lemma, in PLF.Records]
STLCExtendedRecords.f [abbreviation, in PLF.Records]
STLCExtendedRecords.FirstTry [module, in PLF.Records]
STLCExtendedRecords.FirstTry.alist [definition, in PLF.Records]
STLCExtendedRecords.FirstTry.Arrow [constructor, in PLF.Records]
STLCExtendedRecords.FirstTry.Base [constructor, in PLF.Records]
STLCExtendedRecords.FirstTry.TRcd [constructor, in PLF.Records]
STLCExtendedRecords.FirstTry.ty [inductive, in PLF.Records]
STLCExtendedRecords.free_in_context [lemma, in PLF.Records]
STLCExtendedRecords.g [abbreviation, in PLF.Records]
STLCExtendedRecords.has_type [inductive, in PLF.Records]
STLCExtendedRecords.has_type__wf [lemma, in PLF.Records]
STLCExtendedRecords.i1 [abbreviation, in PLF.Records]
STLCExtendedRecords.i2 [abbreviation, in PLF.Records]
STLCExtendedRecords.k [abbreviation, in PLF.Records]
STLCExtendedRecords.l [abbreviation, in PLF.Records]
STLCExtendedRecords.lookup_field_in_value [lemma, in PLF.Records]
STLCExtendedRecords.multistep [abbreviation, in PLF.Records]
STLCExtendedRecords.preservation [lemma, in PLF.Records]
STLCExtendedRecords.progress [lemma, in PLF.Records]
STLCExtendedRecords.RCons [constructor, in PLF.Records]
STLCExtendedRecords.rcons [constructor, in PLF.Records]
STLCExtendedRecords.record_tm [inductive, in PLF.Records]
STLCExtendedRecords.record_ty [inductive, in PLF.Records]
STLCExtendedRecords.RNil [constructor, in PLF.Records]
STLCExtendedRecords.rproj [constructor, in PLF.Records]
STLCExtendedRecords.rtcons [constructor, in PLF.Records]
STLCExtendedRecords.RTcons [constructor, in PLF.Records]
STLCExtendedRecords.rtnil [constructor, in PLF.Records]
STLCExtendedRecords.RTnil [constructor, in PLF.Records]
STLCExtendedRecords.step [inductive, in PLF.Records]
STLCExtendedRecords.step_preserves_record_tm [lemma, in PLF.Records]
STLCExtendedRecords.ST_AppAbs [constructor, in PLF.Records]
STLCExtendedRecords.ST_App1 [constructor, in PLF.Records]
STLCExtendedRecords.ST_App2 [constructor, in PLF.Records]
STLCExtendedRecords.ST_ProjRcd [constructor, in PLF.Records]
STLCExtendedRecords.ST_Proj1 [constructor, in PLF.Records]
STLCExtendedRecords.ST_Rcd_Head [constructor, in PLF.Records]
STLCExtendedRecords.ST_Rcd_Tail [constructor, in PLF.Records]
STLCExtendedRecords.subst [definition, in PLF.Records]
STLCExtendedRecords.substitution_preserves_typing [lemma, in PLF.Records]
STLCExtendedRecords.Tlookup [definition, in PLF.Records]
STLCExtendedRecords.tlookup [definition, in PLF.Records]
STLCExtendedRecords.tm [inductive, in PLF.Records]
STLCExtendedRecords.trnil [constructor, in PLF.Records]
STLCExtendedRecords.ty [inductive, in PLF.Records]
STLCExtendedRecords.typing_example_2 [lemma, in PLF.Records]
STLCExtendedRecords.typing_nonexample [definition, in PLF.Records]
STLCExtendedRecords.typing_nonexample_2 [definition, in PLF.Records]
STLCExtendedRecords.T_Abs [constructor, in PLF.Records]
STLCExtendedRecords.T_App [constructor, in PLF.Records]
STLCExtendedRecords.T_Proj [constructor, in PLF.Records]
STLCExtendedRecords.T_RCons [constructor, in PLF.Records]
STLCExtendedRecords.T_RNil [constructor, in PLF.Records]
STLCExtendedRecords.T_Var [constructor, in PLF.Records]
STLCExtendedRecords.value [inductive, in PLF.Records]
STLCExtendedRecords.var [constructor, in PLF.Records]
STLCExtendedRecords.v_abs [constructor, in PLF.Records]
STLCExtendedRecords.v_rcons [constructor, in PLF.Records]
STLCExtendedRecords.v_rnil [constructor, in PLF.Records]
STLCExtendedRecords.weird_type [definition, in PLF.Records]
STLCExtendedRecords.well_formed_ty [inductive, in PLF.Records]
STLCExtendedRecords.wfArrow [constructor, in PLF.Records]
STLCExtendedRecords.wfBase [constructor, in PLF.Records]
STLCExtendedRecords.wfRCons [constructor, in PLF.Records]
STLCExtendedRecords.wfRNil [constructor, in PLF.Records]
STLCExtendedRecords.wf_rcd_lookup [lemma, in PLF.Records]
-->'_x">STLCExtendedRecords.::x_'-->'_x [notation, in PLF.Records]
-->*'_x">STLCExtendedRecords.::x_'-->*'_x [notation, in PLF.Records]
STLCExtendedRecords.::x_'⊢'_x_'∈'_x [notation, in PLF.Records]
STLCExtendedRecords.::'['_x_':='_x_']'_x [notation, in PLF.Records]
STLCExtended.abs [constructor, in PLF.MoreStlc]
STLCExtended.afi_abs [constructor, in PLF.MoreStlc]
STLCExtended.afi_app1 [constructor, in PLF.MoreStlc]
STLCExtended.afi_app2 [constructor, in PLF.MoreStlc]
STLCExtended.afi_case0 [constructor, in PLF.MoreStlc]
STLCExtended.afi_case1 [constructor, in PLF.MoreStlc]
STLCExtended.afi_case2 [constructor, in PLF.MoreStlc]
STLCExtended.afi_cons1 [constructor, in PLF.MoreStlc]
STLCExtended.afi_cons2 [constructor, in PLF.MoreStlc]
STLCExtended.afi_inl [constructor, in PLF.MoreStlc]
STLCExtended.afi_inr [constructor, in PLF.MoreStlc]
STLCExtended.afi_lcase1 [constructor, in PLF.MoreStlc]
STLCExtended.afi_lcase2 [constructor, in PLF.MoreStlc]
STLCExtended.afi_lcase3 [constructor, in PLF.MoreStlc]
STLCExtended.afi_mult1 [constructor, in PLF.MoreStlc]
STLCExtended.afi_mult2 [constructor, in PLF.MoreStlc]
STLCExtended.afi_pred [constructor, in PLF.MoreStlc]
STLCExtended.afi_succ [constructor, in PLF.MoreStlc]
STLCExtended.afi_test01 [constructor, in PLF.MoreStlc]
STLCExtended.afi_test02 [constructor, in PLF.MoreStlc]
STLCExtended.afi_test03 [constructor, in PLF.MoreStlc]
STLCExtended.afi_var [constructor, in PLF.MoreStlc]
STLCExtended.app [constructor, in PLF.MoreStlc]
STLCExtended.appears_free_in [inductive, in PLF.MoreStlc]
STLCExtended.Arrow [constructor, in PLF.MoreStlc]
STLCExtended.const [constructor, in PLF.MoreStlc]
STLCExtended.context [definition, in PLF.MoreStlc]
STLCExtended.context_invariance [lemma, in PLF.MoreStlc]
STLCExtended.Examples [module, in PLF.MoreStlc]
STLCExtended.Examples.a [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.eo [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.eq [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.even [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.evenodd [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.f [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.FixTest1 [module, in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.fact [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest2 [module, in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.map [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest3 [module, in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.equal [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.reduces2 [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest4 [module, in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.eotest [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.g [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.i1 [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.i2 [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.k [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.l [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.LetTest [module, in PLF.MoreStlc]
STLCExtended.Examples.LetTest.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.LetTest.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.LetTest.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.ListTest [module, in PLF.MoreStlc]
STLCExtended.Examples.ListTest.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.ListTest.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.ListTest.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.m [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.n [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.Numtest [module, in PLF.MoreStlc]
STLCExtended.Examples.Numtest.numtest_reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.Numtest.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.Numtest.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.odd [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.processSum [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.Prodtest [module, in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1 [module, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2 [module, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.reduces [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.test [definition, in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.typechecks [definition, in PLF.MoreStlc]
STLCExtended.Examples.x [abbreviation, in PLF.MoreStlc]
STLCExtended.Examples.y [abbreviation, in PLF.MoreStlc]
STLCExtended.free_in_context [lemma, in PLF.MoreStlc]
STLCExtended.fst [constructor, in PLF.MoreStlc]
STLCExtended.has_type [inductive, in PLF.MoreStlc]
STLCExtended.List [constructor, in PLF.MoreStlc]
STLCExtended.manual_grade_for_context_invariance [definition, in PLF.MoreStlc]
STLCExtended.manual_grade_for_extensions_definition [definition, in PLF.MoreStlc]
STLCExtended.manual_grade_for_preservation [definition, in PLF.MoreStlc]
STLCExtended.manual_grade_for_progress [definition, in PLF.MoreStlc]
STLCExtended.manual_grade_for_substitution_preserves_typing [definition, in PLF.MoreStlc]
STLCExtended.mlt [constructor, in PLF.MoreStlc]
STLCExtended.multistep [abbreviation, in PLF.MoreStlc]
STLCExtended.Nat [constructor, in PLF.MoreStlc]
STLCExtended.pair [constructor, in PLF.MoreStlc]
STLCExtended.prd [constructor, in PLF.MoreStlc]
STLCExtended.preservation [lemma, in PLF.MoreStlc]
STLCExtended.Prod [constructor, in PLF.MoreStlc]
STLCExtended.progress [lemma, in PLF.MoreStlc]
STLCExtended.scc [constructor, in PLF.MoreStlc]
STLCExtended.snd [constructor, in PLF.MoreStlc]
STLCExtended.step [inductive, in PLF.MoreStlc]
STLCExtended.ST_AppAbs [constructor, in PLF.MoreStlc]
STLCExtended.ST_App1 [constructor, in PLF.MoreStlc]
STLCExtended.ST_App2 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Case [constructor, in PLF.MoreStlc]
STLCExtended.ST_CaseInl [constructor, in PLF.MoreStlc]
STLCExtended.ST_CaseInr [constructor, in PLF.MoreStlc]
STLCExtended.ST_Cons1 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Cons2 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Inl [constructor, in PLF.MoreStlc]
STLCExtended.ST_Inr [constructor, in PLF.MoreStlc]
STLCExtended.ST_LcaseCons [constructor, in PLF.MoreStlc]
STLCExtended.ST_LcaseNil [constructor, in PLF.MoreStlc]
STLCExtended.ST_Lcase1 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Mulconsts [constructor, in PLF.MoreStlc]
STLCExtended.ST_Mult1 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Mult2 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Pred [constructor, in PLF.MoreStlc]
STLCExtended.ST_PredNat [constructor, in PLF.MoreStlc]
STLCExtended.ST_SuccNat [constructor, in PLF.MoreStlc]
STLCExtended.ST_Succ1 [constructor, in PLF.MoreStlc]
STLCExtended.ST_Test0Nonzero [constructor, in PLF.MoreStlc]
STLCExtended.ST_Test0Zero [constructor, in PLF.MoreStlc]
STLCExtended.ST_Test01 [constructor, in PLF.MoreStlc]
STLCExtended.subst [definition, in PLF.MoreStlc]
STLCExtended.substitution_preserves_typing [lemma, in PLF.MoreStlc]
STLCExtended.Sum [constructor, in PLF.MoreStlc]
STLCExtended.tcase [constructor, in PLF.MoreStlc]
STLCExtended.tcons [constructor, in PLF.MoreStlc]
STLCExtended.test0 [constructor, in PLF.MoreStlc]
STLCExtended.tfix [constructor, in PLF.MoreStlc]
STLCExtended.tinl [constructor, in PLF.MoreStlc]
STLCExtended.tinr [constructor, in PLF.MoreStlc]
STLCExtended.tlcase [constructor, in PLF.MoreStlc]
STLCExtended.tlet [constructor, in PLF.MoreStlc]
STLCExtended.tm [inductive, in PLF.MoreStlc]
STLCExtended.tnil [constructor, in PLF.MoreStlc]
STLCExtended.ty [inductive, in PLF.MoreStlc]
STLCExtended.T_Abs [constructor, in PLF.MoreStlc]
STLCExtended.T_App [constructor, in PLF.MoreStlc]
STLCExtended.T_Case [constructor, in PLF.MoreStlc]
STLCExtended.T_Cons [constructor, in PLF.MoreStlc]
STLCExtended.T_Inl [constructor, in PLF.MoreStlc]
STLCExtended.T_Inr [constructor, in PLF.MoreStlc]
STLCExtended.T_Lcase [constructor, in PLF.MoreStlc]
STLCExtended.T_Mult [constructor, in PLF.MoreStlc]
STLCExtended.T_Nat [constructor, in PLF.MoreStlc]
STLCExtended.T_Nil [constructor, in PLF.MoreStlc]
STLCExtended.T_Pred [constructor, in PLF.MoreStlc]
STLCExtended.T_Succ [constructor, in PLF.MoreStlc]
STLCExtended.T_Test0 [constructor, in PLF.MoreStlc]
STLCExtended.T_Unit [constructor, in PLF.MoreStlc]
STLCExtended.T_Var [constructor, in PLF.MoreStlc]
STLCExtended.Unit [constructor, in PLF.MoreStlc]
STLCExtended.unit [constructor, in PLF.MoreStlc]
STLCExtended.value [inductive, in PLF.MoreStlc]
STLCExtended.var [constructor, in PLF.MoreStlc]
STLCExtended.v_abs [constructor, in PLF.MoreStlc]
STLCExtended.v_inl [constructor, in PLF.MoreStlc]
STLCExtended.v_inr [constructor, in PLF.MoreStlc]
STLCExtended.v_lcons [constructor, in PLF.MoreStlc]
STLCExtended.v_lnil [constructor, in PLF.MoreStlc]
STLCExtended.v_nat [constructor, in PLF.MoreStlc]
STLCExtended.v_pair [constructor, in PLF.MoreStlc]
STLCExtended.v_unit [constructor, in PLF.MoreStlc]
-->'_x">STLCExtended.::x_'-->'_x [notation, in PLF.MoreStlc]
-->*'_x">STLCExtended.::x_'-->*'_x [notation, in PLF.MoreStlc]
STLCExtended.::x_'⊢'_x_'∈'_x [notation, in PLF.MoreStlc]
STLCExtended.::'['_x_':='_x_']'_x [notation, in PLF.MoreStlc]
StlcImpl [module, in PLF.Typechecking]
STLCProp [module, in PLF.StlcProp]
StlcProp [library]
STLCProp.afi_abs [constructor, in PLF.StlcProp]
STLCProp.afi_app1 [constructor, in PLF.StlcProp]
STLCProp.afi_app2 [constructor, in PLF.StlcProp]
STLCProp.afi_test1 [constructor, in PLF.StlcProp]
STLCProp.afi_test2 [constructor, in PLF.StlcProp]
STLCProp.afi_test3 [constructor, in PLF.StlcProp]
STLCProp.afi_var [constructor, in PLF.StlcProp]
STLCProp.appears_free_in [inductive, in PLF.StlcProp]
STLCProp.canonical_forms_bool [lemma, in PLF.StlcProp]
STLCProp.canonical_forms_fun [lemma, in PLF.StlcProp]
STLCProp.closed [definition, in PLF.StlcProp]
STLCProp.context_invariance [lemma, in PLF.StlcProp]
STLCProp.free_in_context [lemma, in PLF.StlcProp]
STLCProp.manual_grade_for_afi [definition, in PLF.StlcProp]
STLCProp.manual_grade_for_progress_preservation_statement [definition, in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation1 [definition, in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation2 [definition, in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation3 [definition, in PLF.StlcProp]
STLCProp.manual_grade_for_subject_expansion_stlc [definition, in PLF.StlcProp]
STLCProp.preservation [lemma, in PLF.StlcProp]
STLCProp.progress [lemma, in PLF.StlcProp]
STLCProp.progress' [lemma, in PLF.StlcProp]
STLCProp.soundness [lemma, in PLF.StlcProp]
STLCProp.stuck [definition, in PLF.StlcProp]
STLCProp.substitution_preserves_typing [lemma, in PLF.StlcProp]
STLCProp.typable_empty__closed [lemma, in PLF.StlcProp]
STLCProp.unique_types [lemma, in PLF.StlcProp]
STLCRef [module, in PLF.References]
STLCRef.abs [constructor, in PLF.References]
STLCRef.afi_abs [constructor, in PLF.References]
STLCRef.afi_app1 [constructor, in PLF.References]
STLCRef.afi_app2 [constructor, in PLF.References]
STLCRef.afi_assign1 [constructor, in PLF.References]
STLCRef.afi_assign2 [constructor, in PLF.References]
STLCRef.afi_deref [constructor, in PLF.References]
STLCRef.afi_if0_1 [constructor, in PLF.References]
STLCRef.afi_if0_2 [constructor, in PLF.References]
STLCRef.afi_if0_3 [constructor, in PLF.References]
STLCRef.afi_mult1 [constructor, in PLF.References]
STLCRef.afi_mult2 [constructor, in PLF.References]
STLCRef.afi_pred [constructor, in PLF.References]
STLCRef.afi_ref [constructor, in PLF.References]
STLCRef.afi_succ [constructor, in PLF.References]
STLCRef.afi_var [constructor, in PLF.References]
STLCRef.app [constructor, in PLF.References]
STLCRef.appears_free_in [inductive, in PLF.References]
STLCRef.Arrow [constructor, in PLF.References]
STLCRef.assign [constructor, in PLF.References]
STLCRef.assign_pres_store_typing [lemma, in PLF.References]
STLCRef.const [constructor, in PLF.References]
STLCRef.context [definition, in PLF.References]
STLCRef.context_invariance [lemma, in PLF.References]
STLCRef.deref [constructor, in PLF.References]
STLCRef.ExampleVariables [module, in PLF.References]
STLCRef.ExampleVariables.r [definition, in PLF.References]
STLCRef.ExampleVariables.s [definition, in PLF.References]
STLCRef.ExampleVariables.x [definition, in PLF.References]
STLCRef.ExampleVariables.y [definition, in PLF.References]
STLCRef.extends [inductive, in PLF.References]
STLCRef.extends_app [lemma, in PLF.References]
STLCRef.extends_cons [constructor, in PLF.References]
STLCRef.extends_lookup [lemma, in PLF.References]
STLCRef.extends_nil [constructor, in PLF.References]
STLCRef.extends_refl [lemma, in PLF.References]
STLCRef.free_in_context [lemma, in PLF.References]
STLCRef.has_type [inductive, in PLF.References]
STLCRef.length_extends [lemma, in PLF.References]
STLCRef.length_replace [lemma, in PLF.References]
STLCRef.loc [constructor, in PLF.References]
STLCRef.lookup_replace_eq [lemma, in PLF.References]
STLCRef.lookup_replace_neq [lemma, in PLF.References]
STLCRef.manual_grade_for_compact_update [definition, in PLF.References]
STLCRef.manual_grade_for_cyclic_store [definition, in PLF.References]
STLCRef.manual_grade_for_preservation_informal [definition, in PLF.References]
STLCRef.manual_grade_for_store_not_unique [definition, in PLF.References]
STLCRef.manual_grade_for_type_safety_violation [definition, in PLF.References]
STLCRef.mlt [constructor, in PLF.References]
STLCRef.multistep [definition, in PLF.References]
STLCRef.Nat [constructor, in PLF.References]
STLCRef.nth_eq_last [lemma, in PLF.References]
STLCRef.prd [constructor, in PLF.References]
STLCRef.preservation [lemma, in PLF.References]
STLCRef.preservation_theorem [definition, in PLF.References]
STLCRef.preservation_wrong1 [lemma, in PLF.References]
STLCRef.preservation_wrong2 [lemma, in PLF.References]
STLCRef.progress [lemma, in PLF.References]
STLCRef.ref [constructor, in PLF.References]
STLCRef.Ref [constructor, in PLF.References]
STLCRef.RefsAndNontermination [module, in PLF.References]
STLCRef.RefsAndNontermination.factorial [definition, in PLF.References]
STLCRef.RefsAndNontermination.factorial_type [lemma, in PLF.References]
STLCRef.RefsAndNontermination.loop [definition, in PLF.References]
STLCRef.RefsAndNontermination.loop_fun [definition, in PLF.References]
STLCRef.RefsAndNontermination.loop_fun_step_self [lemma, in PLF.References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [lemma, in PLF.References]
STLCRef.RefsAndNontermination.loop_typeable [lemma, in PLF.References]
STLCRef.RefsAndNontermination.multistep1 [definition, in PLF.References]
STLCRef.RefsAndNontermination.sc_one [constructor, in PLF.References]
STLCRef.RefsAndNontermination.sc_step [constructor, in PLF.References]
STLCRef.RefsAndNontermination.step_closure [inductive, in PLF.References]
-->+'_x_'/'_x">STLCRef.RefsAndNontermination.::x_'/'_x_'-->+'_x_'/'_x [notation, in PLF.References]
STLCRef.replace [definition, in PLF.References]
STLCRef.replace_nil [lemma, in PLF.References]
STLCRef.scc [constructor, in PLF.References]
STLCRef.step [inductive, in PLF.References]
STLCRef.store [definition, in PLF.References]
STLCRef.store_lookup [definition, in PLF.References]
STLCRef.store_Tlookup [definition, in PLF.References]
STLCRef.store_ty [definition, in PLF.References]
STLCRef.store_weakening [lemma, in PLF.References]
STLCRef.store_well_typed [definition, in PLF.References]
STLCRef.store_well_typed_app [lemma, in PLF.References]
STLCRef.ST_AppAbs [constructor, in PLF.References]
STLCRef.ST_App1 [constructor, in PLF.References]
STLCRef.ST_App2 [constructor, in PLF.References]
STLCRef.ST_Assign [constructor, in PLF.References]
STLCRef.ST_Assign1 [constructor, in PLF.References]
STLCRef.ST_Assign2 [constructor, in PLF.References]
STLCRef.ST_Deref [constructor, in PLF.References]
STLCRef.ST_DerefLoc [constructor, in PLF.References]
STLCRef.ST_If₀ [constructor, in PLF.References]
STLCRef.ST_If0_Nonzero [constructor, in PLF.References]
STLCRef.ST_If0_Zero [constructor, in PLF.References]
STLCRef.ST_MultNats [constructor, in PLF.References]
STLCRef.ST_Mult1 [constructor, in PLF.References]
STLCRef.ST_Mult2 [constructor, in PLF.References]
STLCRef.ST_Pred [constructor, in PLF.References]
STLCRef.ST_PredNat [constructor, in PLF.References]
STLCRef.ST_Ref [constructor, in PLF.References]
STLCRef.ST_RefValue [constructor, in PLF.References]
STLCRef.ST_Succ [constructor, in PLF.References]
STLCRef.ST_SuccNat [constructor, in PLF.References]
STLCRef.subst [definition, in PLF.References]
STLCRef.substitution_preserves_typing [lemma, in PLF.References]
STLCRef.test0 [constructor, in PLF.References]
STLCRef.tm [inductive, in PLF.References]
STLCRef.tseq [definition, in PLF.References]
STLCRef.ty [inductive, in PLF.References]
STLCRef.T_Abs [constructor, in PLF.References]
STLCRef.T_App [constructor, in PLF.References]
STLCRef.T_Assign [constructor, in PLF.References]
STLCRef.T_Deref [constructor, in PLF.References]
STLCRef.T_If₀ [constructor, in PLF.References]
STLCRef.T_Loc [constructor, in PLF.References]
STLCRef.T_Mult [constructor, in PLF.References]
STLCRef.T_Nat [constructor, in PLF.References]
STLCRef.T_Pred [constructor, in PLF.References]
STLCRef.T_Ref [constructor, in PLF.References]
STLCRef.T_Succ [constructor, in PLF.References]
STLCRef.T_Unit [constructor, in PLF.References]
STLCRef.T_Var [constructor, in PLF.References]
STLCRef.Unit [constructor, in PLF.References]
STLCRef.unit [constructor, in PLF.References]
STLCRef.value [inductive, in PLF.References]
STLCRef.var [constructor, in PLF.References]
STLCRef.v_abs [constructor, in PLF.References]
STLCRef.v_loc [constructor, in PLF.References]
STLCRef.v_nat [constructor, in PLF.References]
STLCRef.v_unit [constructor, in PLF.References]
-->'_x_'/'_x">STLCRef.::x_'/'_x_'-->'_x_'/'_x [notation, in PLF.References]
-->*'_x_'/'_x">STLCRef.::x_'/'_x_'-->*'_x_'/'_x [notation, in PLF.References]
STLCRef.::x_';'_x_'⊢'_x_'∈'_x [notation, in PLF.References]
STLCRef.::'['_x_':='_x_']'_x [notation, in PLF.References]
STLCTypes [module, in PLF.Typechecking]
STLCTypes.eqb_ty [definition, in PLF.Typechecking]
STLCTypes.eqb_ty_refl [lemma, in PLF.Typechecking]
STLCTypes.eqb_ty__eq [lemma, in PLF.Typechecking]
STLC.abs [constructor, in PLF.Stlc]
STLC.app [constructor, in PLF.Stlc]
STLC.Arrow [constructor, in PLF.Stlc]
STLC.Bool [constructor, in PLF.Stlc]
STLC.context [definition, in PLF.Stlc]
STLC.fls [constructor, in PLF.Stlc]
STLC.has_type [inductive, in PLF.Stlc]
STLC.idB [abbreviation, in PLF.Stlc]
STLC.idBB [abbreviation, in PLF.Stlc]
STLC.idBBBB [abbreviation, in PLF.Stlc]
STLC.k [abbreviation, in PLF.Stlc]
STLC.multistep [abbreviation, in PLF.Stlc]
STLC.notB [abbreviation, in PLF.Stlc]
STLC.step [inductive, in PLF.Stlc]
STLC.step_example1 [lemma, in PLF.Stlc]
STLC.step_example1' [lemma, in PLF.Stlc]
STLC.step_example2 [lemma, in PLF.Stlc]
STLC.step_example2' [lemma, in PLF.Stlc]
STLC.step_example3 [lemma, in PLF.Stlc]
STLC.step_example3' [lemma, in PLF.Stlc]
STLC.step_example4 [lemma, in PLF.Stlc]
STLC.step_example4' [lemma, in PLF.Stlc]
STLC.step_example5 [lemma, in PLF.Stlc]
STLC.step_example5_with_normalize [lemma, in PLF.Stlc]
STLC.ST_AppAbs [constructor, in PLF.Stlc]
STLC.ST_App1 [constructor, in PLF.Stlc]
STLC.ST_App2 [constructor, in PLF.Stlc]
STLC.ST_Test [constructor, in PLF.Stlc]
STLC.ST_TestFls [constructor, in PLF.Stlc]
STLC.ST_TestTru [constructor, in PLF.Stlc]
STLC.subst [definition, in PLF.Stlc]
STLC.substi [inductive, in PLF.Stlc]
STLC.substi_correct [lemma, in PLF.Stlc]
STLC.s_var1 [constructor, in PLF.Stlc]
STLC.test [constructor, in PLF.Stlc]
STLC.tm [inductive, in PLF.Stlc]
STLC.tru [constructor, in PLF.Stlc]
STLC.ty [inductive, in PLF.Stlc]
STLC.typing_example_1 [definition, in PLF.Stlc]
STLC.typing_example_1' [definition, in PLF.Stlc]
STLC.typing_example_2 [definition, in PLF.Stlc]
STLC.typing_example_2_full [definition, in PLF.Stlc]
STLC.typing_example_3 [definition, in PLF.Stlc]
STLC.typing_nonexample_1 [definition, in PLF.Stlc]
STLC.typing_nonexample_3 [definition, in PLF.Stlc]
STLC.T_Abs [constructor, in PLF.Stlc]
STLC.T_App [constructor, in PLF.Stlc]
STLC.T_Fls [constructor, in PLF.Stlc]
STLC.T_Test [constructor, in PLF.Stlc]
STLC.T_Tru [constructor, in PLF.Stlc]
STLC.T_Var [constructor, in PLF.Stlc]
STLC.value [inductive, in PLF.Stlc]
STLC.var [constructor, in PLF.Stlc]
STLC.v_abs [constructor, in PLF.Stlc]
STLC.v_fls [constructor, in PLF.Stlc]
STLC.v_tru [constructor, in PLF.Stlc]
STLC.x [definition, in PLF.Stlc]
STLC.y [definition, in PLF.Stlc]
STLC.z [definition, in PLF.Stlc]
-->'_x">STLC.::x_'-->'_x [notation, in PLF.Stlc]
-->*'_x">STLC.::x_'-->*'_x [notation, in PLF.Stlc]
STLC.::x_'⊢'_x_'∈'_x [notation, in PLF.Stlc]
STLC.::'['_x_':='_x_']'_x [notation, in PLF.Stlc]
strong_progress [lemma, in PLF.Smallstep]
stuck [definition, in PLF.Types]
ST_AppAbs [constructor, in PLF.Sub]
ST_AppAbs [constructor, in PLF.RecordSub]
ST_AppAbs [constructor, in PLF.Norm]
ST_App1 [constructor, in PLF.RecordSub]
ST_App1 [constructor, in PLF.Sub]
ST_App1 [constructor, in PLF.Norm]
ST_App2 [constructor, in PLF.RecordSub]
ST_App2 [constructor, in PLF.Sub]
ST_App2 [constructor, in PLF.Norm]
ST_Fst [constructor, in PLF.Norm]
ST_FstPair [constructor, in PLF.Norm]
ST_Iszro [constructor, in PLF.Types]
ST_IszroScc [constructor, in PLF.Types]
ST_IszroZro [constructor, in PLF.Types]
ST_Pair1 [constructor, in PLF.Norm]
ST_Pair2 [constructor, in PLF.Norm]
ST_PlusConstConst [constructor, in PLF.Smallstep]
ST_Plus1 [constructor, in PLF.Smallstep]
ST_Plus2 [constructor, in PLF.Smallstep]
ST_Prd [constructor, in PLF.Types]
ST_PrdScc [constructor, in PLF.Types]
ST_PrdZro [constructor, in PLF.Types]
ST_ProjRcd [constructor, in PLF.RecordSub]
ST_Proj1 [constructor, in PLF.RecordSub]
ST_Rcd_Head [constructor, in PLF.RecordSub]
ST_Rcd_Tail [constructor, in PLF.RecordSub]
ST_Scc [constructor, in PLF.Types]
ST_Snd [constructor, in PLF.Norm]
ST_SndPair [constructor, in PLF.Norm]
ST_Test [constructor, in PLF.Norm]
ST_Test [constructor, in PLF.Types]
ST_Test [constructor, in PLF.Sub]
ST_TestFalse [constructor, in PLF.Norm]
ST_TestFalse [constructor, in PLF.Sub]
ST_TestFls [constructor, in PLF.Types]
ST_TestTru [constructor, in PLF.Types]
ST_TestTrue [constructor, in PLF.Sub]
ST_TestTrue [constructor, in PLF.Norm]
Sub [library]
subst [definition, in PLF.Sub]
subst [definition, in PLF.Norm]
subst [definition, in PLF.RecordSub]
substitution_preserves_typing [lemma, in PLF.RecordSub]
substitution_preserves_typing [lemma, in PLF.Sub]
substitution_preserves_typing [lemma, in PLF.Norm]
subst_aexp [definition, in PLF.Equiv]
subst_aexp_ex [definition, in PLF.Equiv]
subst_closed [lemma, in PLF.Norm]
subst_equiv_property [definition, in PLF.Equiv]
subst_inequiv [lemma, in PLF.Equiv]
subst_msubst [lemma, in PLF.Norm]
subst_not_afi [lemma, in PLF.Norm]
subtract_slowly_dec [definition, in PLF.Hoare2]
subtract_slowly_dec_correct [lemma, in PLF.Hoare2]
subtype [inductive, in PLF.RecordSub]
subtype [inductive, in PLF.Sub]
subtype [axiom, in PLF.UseAuto]
subtype_refl [axiom, in PLF.UseAuto]
subtype_trans [axiom, in PLF.UseAuto]
subtype__wf [lemma, in PLF.RecordSub]
SubtypingInversion [module, in PLF.UseAuto]
SubtypingInversion.abs_arrow [lemma, in PLF.UseAuto]
SubtypingInversion.abs_arrow' [lemma, in PLF.UseAuto]
sub_inversion_arrow [lemma, in PLF.RecordSub]
sub_inversion_arrow [lemma, in PLF.Sub]
sub_inversion_Bool [lemma, in PLF.Sub]
swap [definition, in PLF.Hoare2]
swap_correct [lemma, in PLF.Hoare2]
swap_dec [definition, in PLF.Hoare2]
swap_exercise [lemma, in PLF.Hoare]
swap_if_branches [lemma, in PLF.Equiv]
swap_noninterfering_assignments [lemma, in PLF.Equiv]
swap_program [definition, in PLF.Hoare]
swap_subst [lemma, in PLF.Norm]
sym_aequiv [lemma, in PLF.Equiv]
sym_bequiv [lemma, in PLF.Equiv]
sym_cequiv [lemma, in PLF.Equiv]
S_Arrow [constructor, in PLF.Sub]
S_Arrow [constructor, in PLF.RecordSub]
S_RcdDepth [constructor, in PLF.RecordSub]
S_RcdPerm [constructor, in PLF.RecordSub]
S_RcdWidth [constructor, in PLF.RecordSub]
S_Refl [constructor, in PLF.Sub]
S_Refl [constructor, in PLF.RecordSub]
S_Top [constructor, in PLF.RecordSub]
S_Top [constructor, in PLF.Sub]
S_Trans [constructor, in PLF.RecordSub]
S_Trans [constructor, in PLF.Sub]

T

T [definition, in PLF.Hoare2]
tass [definition, in PLF.Norm]
Temp1 [module, in PLF.Smallstep]
Temp1.step [inductive, in PLF.Smallstep]
Temp1.ST_PlusConstConst [constructor, in PLF.Smallstep]
Temp1.ST_Plus1 [constructor, in PLF.Smallstep]
Temp1.ST_Plus2 [constructor, in PLF.Smallstep]
Temp1.value [inductive, in PLF.Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in PLF.Smallstep]
Temp1.v_const [constructor, in PLF.Smallstep]
Temp1.v_funny [constructor, in PLF.Smallstep]
-->'_x">Temp1.::x_'-->'_x [notation, in PLF.Smallstep]
Temp2 [module, in PLF.Smallstep]
Temp2.step [inductive, in PLF.Smallstep]
Temp2.ST_Funny [constructor, in PLF.Smallstep]
Temp2.ST_PlusConstConst [constructor, in PLF.Smallstep]
Temp2.ST_Plus1 [constructor, in PLF.Smallstep]
Temp2.ST_Plus2 [constructor, in PLF.Smallstep]
Temp2.value [inductive, in PLF.Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in PLF.Smallstep]
Temp2.v_const [constructor, in PLF.Smallstep]
-->'_x">Temp2.::x_'-->'_x [notation, in PLF.Smallstep]
Temp3 [module, in PLF.Smallstep]
Temp3.step [inductive, in PLF.Smallstep]
Temp3.ST_PlusConstConst [constructor, in PLF.Smallstep]
Temp3.ST_Plus1 [constructor, in PLF.Smallstep]
Temp3.value [inductive, in PLF.Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in PLF.Smallstep]
Temp3.v_const [constructor, in PLF.Smallstep]
-->'_x">Temp3.::x_'-->'_x [notation, in PLF.Smallstep]
Temp4 [module, in PLF.Smallstep]
Temp4.bool_step_prop1 [definition, in PLF.Smallstep]
Temp4.bool_step_prop2 [definition, in PLF.Smallstep]
Temp4.bool_step_prop3 [definition, in PLF.Smallstep]
Temp4.fls [constructor, in PLF.Smallstep]
Temp4.manual_grade_for_smallstep_bools [definition, in PLF.Smallstep]
Temp4.step [inductive, in PLF.Smallstep]
Temp4.step_deterministic [lemma, in PLF.Smallstep]
Temp4.strong_progress [lemma, in PLF.Smallstep]
Temp4.ST_If [constructor, in PLF.Smallstep]
Temp4.ST_IfFalse [constructor, in PLF.Smallstep]
Temp4.ST_IfTrue [constructor, in PLF.Smallstep]
Temp4.Temp5 [module, in PLF.Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in PLF.Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in PLF.Smallstep]
Temp4.Temp5.step [inductive, in PLF.Smallstep]
Temp4.Temp5.ST_If [constructor, in PLF.Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in PLF.Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in PLF.Smallstep]
-->'_x">Temp4.Temp5.::x_'-->'_x [notation, in PLF.Smallstep]
Temp4.test [constructor, in PLF.Smallstep]
Temp4.tm [inductive, in PLF.Smallstep]
Temp4.tru [constructor, in PLF.Smallstep]
Temp4.value [inductive, in PLF.Smallstep]
Temp4.v_fls [constructor, in PLF.Smallstep]
Temp4.v_tru [constructor, in PLF.Smallstep]
-->'_x">Temp4.::x_'-->'_x [notation, in PLF.Smallstep]
test [constructor, in PLF.Types]
test [constructor, in PLF.Norm]
test [constructor, in PLF.Sub]
TEST_false [lemma, in PLF.Equiv]
test_multistep_1 [lemma, in PLF.Smallstep]
test_multistep_1' [lemma, in PLF.Smallstep]
test_multistep_2 [lemma, in PLF.Smallstep]
test_multistep_3 [lemma, in PLF.Smallstep]
test_multistep_4 [lemma, in PLF.Smallstep]
test_pe_aexp1 [definition, in PLF.PE]
test_pe_bexp1 [definition, in PLF.PE]
test_pe_bexp2 [definition, in PLF.PE]
test_pe_update [definition, in PLF.PE]
TEST_true [lemma, in PLF.Equiv]
TEST_true_simple [lemma, in PLF.Equiv]
text_pe_aexp2 [definition, in PLF.PE]
Tlookup [definition, in PLF.RecordSub]
tlookup [definition, in PLF.RecordSub]
tm [inductive, in PLF.Smallstep]
tm [inductive, in PLF.RecordSub]
tm [inductive, in PLF.Norm]
tm [inductive, in PLF.Types]
tm [inductive, in PLF.Sub]
Top [constructor, in PLF.RecordSub]
Top [constructor, in PLF.Sub]
transitivity_bad_hint_1 [lemma, in PLF.UseAuto]
transitivity_workaround_1 [lemma, in PLF.UseAuto]
transitivity_workaround_2 [lemma, in PLF.UseAuto]
trans_aequiv [lemma, in PLF.Equiv]
trans_bequiv [lemma, in PLF.Equiv]
trans_cequiv [lemma, in PLF.Equiv]
tru [constructor, in PLF.Types]
tru [constructor, in PLF.Norm]
tru [constructor, in PLF.Sub]
two_loops_correct [lemma, in PLF.Hoare2]
two_loops_dec [definition, in PLF.Hoare2]
ty [inductive, in PLF.Norm]
ty [inductive, in PLF.RecordSub]
ty [inductive, in PLF.Types]
ty [inductive, in PLF.Sub]
typ [axiom, in PLF.UseAuto]
typable_empty__closed [lemma, in PLF.Norm]
TypecheckerExtensions [module, in PLF.Typechecking]
TypecheckerExtensions.eqb_ty [definition, in PLF.Typechecking]
TypecheckerExtensions.eqb_ty_refl [lemma, in PLF.Typechecking]
TypecheckerExtensions.eqb_ty__eq [lemma, in PLF.Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_complete [definition, in PLF.Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_sound [definition, in PLF.Typechecking]
TypecheckerExtensions.type_check [definition, in PLF.Typechecking]
TypecheckerExtensions.type_checking_complete [lemma, in PLF.Typechecking]
TypecheckerExtensions.type_checking_sound [lemma, in PLF.Typechecking]
Typechecking [library]
Types [library]
typing_inversion_abs [lemma, in PLF.RecordSub]
typing_inversion_abs [lemma, in PLF.Sub]
typing_inversion_app [lemma, in PLF.RecordSub]
typing_inversion_app [lemma, in PLF.Sub]
typing_inversion_false [lemma, in PLF.Sub]
typing_inversion_if [lemma, in PLF.Sub]
typing_inversion_proj [lemma, in PLF.RecordSub]
typing_inversion_rcons [lemma, in PLF.RecordSub]
typing_inversion_true [lemma, in PLF.Sub]
typing_inversion_unit [lemma, in PLF.Sub]
typing_inversion_var [lemma, in PLF.RecordSub]
typing_inversion_var [lemma, in PLF.Sub]
T_Abs [constructor, in PLF.Norm]
T_Abs [constructor, in PLF.RecordSub]
T_Abs [constructor, in PLF.Sub]
T_App [constructor, in PLF.RecordSub]
T_App [constructor, in PLF.Sub]
T_App [constructor, in PLF.Norm]
T_False [constructor, in PLF.Norm]
T_False [constructor, in PLF.Sub]
T_Fls [constructor, in PLF.Types]
T_Fst [constructor, in PLF.Norm]
T_Iszro [constructor, in PLF.Types]
T_Pair [constructor, in PLF.Norm]
T_Prd [constructor, in PLF.Types]
T_Proj [constructor, in PLF.RecordSub]
T_RCons [constructor, in PLF.RecordSub]
T_RNil [constructor, in PLF.RecordSub]
T_Scc [constructor, in PLF.Types]
T_Snd [constructor, in PLF.Norm]
T_Sub [constructor, in PLF.Sub]
T_Sub [constructor, in PLF.RecordSub]
T_Test [constructor, in PLF.Norm]
T_Test [constructor, in PLF.Types]
T_Test [constructor, in PLF.Sub]
T_Tru [constructor, in PLF.Types]
T_True [constructor, in PLF.Norm]
T_True [constructor, in PLF.Sub]
T_Unit [constructor, in PLF.Sub]
T_Var [constructor, in PLF.RecordSub]
T_Var [constructor, in PLF.Sub]
T_Var [constructor, in PLF.Norm]
T_Zro [constructor, in PLF.Types]

U

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

V

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

W

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

Z

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

:

->>'_'{{'_x_'}}'">:dcom_scope:x_'->>'_'{{'_x_'}}' [notation, in PLF.Hoare2]
:dcom_scope:x_'::='_x_'{{'_x_'}}' [notation, in PLF.Hoare2]
:dcom_scope:x_';;'_x [notation, in PLF.Hoare2]
:dcom_scope:'SKIP'_'{{'_x_'}}' [notation, in PLF.Hoare2]
:dcom_scope:'TEST'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}' [notation, in PLF.Hoare2]
:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [notation, in PLF.Hoare2]
->>'_'{{'_x_'}}'_x">:dcom_scope:'->>'_'{{'_x_'}}'_x [notation, in PLF.Hoare2]
:dcom_scope:'{{'_x_'}}'_x [notation, in PLF.Hoare2]
->>'_x">:hoare_spec_scope:x_'->>'_x [notation, in PLF.Hoare]
<<->>'_x">:hoare_spec_scope:x_'<<->>'_x [notation, in PLF.Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [notation, in PLF.Hoare]
:ltac_scope:'>>' [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [notation, in PLF.LibTactics]
:ltac_scope:'__' [notation, in PLF.LibTactics]
:ltac_scope:'___' [notation, in PLF.LibTactics]
-->'_x">::x_'-->'_x [notation, in PLF.RecordSub]
-->'_x">::x_'-->'_x [notation, in PLF.Sub]
-->'_x">::x_'-->'_x [notation, in PLF.Norm]
-->'_x">::x_'-->'_x [notation, in PLF.Smallstep]
-->'_x">::x_'-->'_x [notation, in PLF.Types]
-->*'_x">::x_'-->*'_x [notation, in PLF.Types]
-->*'_x">::x_'-->*'_x [notation, in PLF.Smallstep]
-->*'_x">::x_'-->*'_x [notation, in PLF.Norm]
-->a'_x">::x_'/'_x_'-->a'_x [notation, in PLF.Smallstep]
-->b'_x">::x_'/'_x_'-->b'_x [notation, in PLF.Smallstep]
-->'_x_'/'_x">::x_'/'_x_'-->'_x_'/'_x [notation, in PLF.Smallstep]
::x_'/'_x_'/'_x_'\\'_x [notation, in PLF.PE]
::x_'/'_x_'\\'_x_'/'_x [notation, in PLF.PE]
::x_'<-'_x_';;'_x [notation, in PLF.Typechecking]
::x_'<:'_x [notation, in PLF.RecordSub]
::x_'<:'_x [notation, in PLF.Sub]
::x_'='''_x [notation, in PLF.LibTactics]
::x_'==>'_x [notation, in PLF.Smallstep]
⊢>'_x_']'">::x_'['_x_'⊢>'_x_']' [notation, in PLF.Hoare]
::x_'⊢'_x_'∈'_x [notation, in PLF.RecordSub]
::x_'⊢'_x_'∈'_x [notation, in PLF.Sub]
::'fail' [notation, in PLF.Typechecking]
::'nosimpl'_x [notation, in PLF.LibTactics]
::'Register'_x_x [notation, in PLF.LibTactics]
::'return'_x [notation, in PLF.Typechecking]
::'Something' [notation, in PLF.LibTactics]
::'['_x_':='_x_']'_x [notation, in PLF.Sub]
::'['_x_':='_x_']'_x [notation, in PLF.RecordSub]
::'['_x_':='_x_']'_x [notation, in PLF.Norm]
::'⊢'_x_'∈'_x [notation, in PLF.Types]

---

Notation Index

C

-->'_x_'/'_x">CImp.::x_'/'_x_'-->'_x_'/'_x [in PLF.Smallstep]
-->*'_x_'/'_x">CImp.::x_'/'_x_'-->*'_x_'/'_x [in PLF.Smallstep]
CImp.::x_'::='_x [in PLF.Smallstep]
CImp.::x_';;'_x [in PLF.Smallstep]
CImp.::'PAR'_x_'WITH'_x_'END' [in PLF.Smallstep]
CImp.::'SKIP' [in PLF.Smallstep]
CImp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Smallstep]
CImp.::'WHILE'_x_'DO'_x_'END' [in PLF.Smallstep]
-->'_x">Combined.::x_'-->'_x [in PLF.Smallstep]

H

Himp.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in PLF.Hoare]
Himp.:imp_scope:x_'::='_x [in PLF.Equiv]
Himp.:imp_scope:x_';;'_x [in PLF.Equiv]
Himp.:imp_scope:'HAVOC'_x [in PLF.Equiv]
Himp.:imp_scope:'SKIP' [in PLF.Equiv]
Himp.:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Equiv]
Himp.:imp_scope:'WHILE'_x_'DO'_x_'END' [in PLF.Equiv]
Himp.::x_'::='_x [in PLF.Hoare]
Himp.::x_';;'_x [in PLF.Hoare]
Himp.::x_'=['_x_']=>'_x [in PLF.Equiv]
Himp.::x_'=['_x_']=>'_x [in PLF.Hoare]
Himp.::'HAVOC'_x [in PLF.Hoare]
Himp.::'SKIP' [in PLF.Hoare]
Himp.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Hoare]
Himp.::'WHILE'_x_'DO'_x_'END' [in PLF.Hoare]
HoareAssertAssume.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in PLF.Hoare]
HoareAssertAssume.::x_'::='_x [in PLF.Hoare]
HoareAssertAssume.::x_';;'_x [in PLF.Hoare]
HoareAssertAssume.::x_'=['_x_']=>'_x [in PLF.Hoare]
HoareAssertAssume.::'ASSERT'_x [in PLF.Hoare]
HoareAssertAssume.::'ASSUME'_x [in PLF.Hoare]
HoareAssertAssume.::'SKIP' [in PLF.Hoare]
HoareAssertAssume.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Hoare]
HoareAssertAssume.::'WHILE'_x_'DO'_x_'END' [in PLF.Hoare]

I

If₁.:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in PLF.Hoare]
If₁.:imp_scope:x_'::='_x [in PLF.Hoare]
If₁.:imp_scope:x_';;'_x [in PLF.Hoare]
If₁.:imp_scope:'IF₁'_x_'THEN'_x_'FI' [in PLF.Hoare]
If₁.:imp_scope:'SKIP' [in PLF.Hoare]
If₁.:imp_scope:'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Hoare]
If₁.:imp_scope:'WHILE'_x_'DO'_x_'END' [in PLF.Hoare]
If₁.::x_'=['_x_']=>'_x [in PLF.Hoare]

L

Loop.::x_'/'_x_'/'_x_'/'_x_'\\'_x_'#'_x [in PLF.PE]
Loop.::x_'/'_x_'\\'_x_'#'_x [in PLF.PE]
Loop.::x_'/'_x_'\\'_x_'/'_x_'/'_x [in PLF.PE]

R

RepeatExercise.::x_'::='_x [in PLF.Hoare]
RepeatExercise.::x_';;'_x [in PLF.Hoare]
RepeatExercise.::x_'=['_x_']=>'_x [in PLF.Hoare]
RepeatExercise.::'REPEAT'_x_'UNTIL'_x_'END' [in PLF.Hoare]
RepeatExercise.::'SKIP' [in PLF.Hoare]
RepeatExercise.::'TEST'_x_'THEN'_x_'ELSE'_x_'FI' [in PLF.Hoare]
RepeatExercise.::'WHILE'_x_'DO'_x_'END' [in PLF.Hoare]
RepeatExercise.::'{{'_x_'}}'_x_'{{'_x_'}}' [in PLF.Hoare]

S

-->'_x">SimpleArith1.::x_'-->'_x [in PLF.Smallstep]
-->'_x">STLCExtendedRecords.::x_'-->'_x [in PLF.Records]
-->*'_x">STLCExtendedRecords.::x_'-->*'_x [in PLF.Records]
STLCExtendedRecords.::x_'⊢'_x_'∈'_x [in PLF.Records]
STLCExtendedRecords.::'['_x_':='_x_']'_x [in PLF.Records]
-->'_x">STLCExtended.::x_'-->'_x [in PLF.MoreStlc]
-->*'_x">STLCExtended.::x_'-->*'_x [in PLF.MoreStlc]
STLCExtended.::x_'⊢'_x_'∈'_x [in PLF.MoreStlc]
STLCExtended.::'['_x_':='_x_']'_x [in PLF.MoreStlc]
-->+'_x_'/'_x">STLCRef.RefsAndNontermination.::x_'/'_x_'-->+'_x_'/'_x [in PLF.References]
-->'_x_'/'_x">STLCRef.::x_'/'_x_'-->'_x_'/'_x [in PLF.References]
-->*'_x_'/'_x">STLCRef.::x_'/'_x_'-->*'_x_'/'_x [in PLF.References]
STLCRef.::x_';'_x_'⊢'_x_'∈'_x [in PLF.References]
STLCRef.::'['_x_':='_x_']'_x [in PLF.References]
-->'_x">STLC.::x_'-->'_x [in PLF.Stlc]
-->*'_x">STLC.::x_'-->*'_x [in PLF.Stlc]
STLC.::x_'⊢'_x_'∈'_x [in PLF.Stlc]
STLC.::'['_x_':='_x_']'_x [in PLF.Stlc]

T

-->'_x">Temp1.::x_'-->'_x [in PLF.Smallstep]
-->'_x">Temp2.::x_'-->'_x [in PLF.Smallstep]
-->'_x">Temp3.::x_'-->'_x [in PLF.Smallstep]
-->'_x">Temp4.Temp5.::x_'-->'_x [in PLF.Smallstep]
-->'_x">Temp4.::x_'-->'_x [in PLF.Smallstep]

:

->>'_'{{'_x_'}}'">:dcom_scope:x_'->>'_'{{'_x_'}}' [in PLF.Hoare2]
:dcom_scope:x_'::='_x_'{{'_x_'}}' [in PLF.Hoare2]
:dcom_scope:x_';;'_x [in PLF.Hoare2]
:dcom_scope:'SKIP'_'{{'_x_'}}' [in PLF.Hoare2]
:dcom_scope:'TEST'_x_'THEN'_'{{'_x_'}}'_x_'ELSE'_'{{'_x_'}}'_x_'FI'_'{{'_x_'}}' [in PLF.Hoare2]
:dcom_scope:'WHILE'_x_'DO'_'{{'_x_'}}'_x_'END'_'{{'_x_'}}' [in PLF.Hoare2]
->>'_'{{'_x_'}}'_x">:dcom_scope:'->>'_'{{'_x_'}}'_x [in PLF.Hoare2]
:dcom_scope:'{{'_x_'}}'_x [in PLF.Hoare2]
->>'_x">:hoare_spec_scope:x_'->>'_x [in PLF.Hoare]
<<->>'_x">:hoare_spec_scope:x_'<<->>'_x [in PLF.Hoare]
:hoare_spec_scope:'{{'_x_'}}'_x_'{{'_x_'}}' [in PLF.Hoare]
:ltac_scope:'>>' [in PLF.LibTactics]
:ltac_scope:'>>'_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'>>'_x_x_x_x_x_x_x_x_x_x_x_x_x [in PLF.LibTactics]
:ltac_scope:'__' [in PLF.LibTactics]
:ltac_scope:'___' [in PLF.LibTactics]
-->'_x">::x_'-->'_x [in PLF.RecordSub]
-->'_x">::x_'-->'_x [in PLF.Sub]
-->'_x">::x_'-->'_x [in PLF.Norm]
-->'_x">::x_'-->'_x [in PLF.Smallstep]
-->'_x">::x_'-->'_x [in PLF.Types]
-->*'_x">::x_'-->*'_x [in PLF.Types]
-->*'_x">::x_'-->*'_x [in PLF.Smallstep]
-->*'_x">::x_'-->*'_x [in PLF.Norm]
-->a'_x">::x_'/'_x_'-->a'_x [in PLF.Smallstep]
-->b'_x">::x_'/'_x_'-->b'_x [in PLF.Smallstep]
-->'_x_'/'_x">::x_'/'_x_'-->'_x_'/'_x [in PLF.Smallstep]
::x_'/'_x_'/'_x_'\\'_x [in PLF.PE]
::x_'/'_x_'\\'_x_'/'_x [in PLF.PE]
::x_'<-'_x_';;'_x [in PLF.Typechecking]
::x_'<:'_x [in PLF.RecordSub]
::x_'<:'_x [in PLF.Sub]
::x_'='''_x [in PLF.LibTactics]
::x_'==>'_x [in PLF.Smallstep]
⊢>'_x_']'">::x_'['_x_'⊢>'_x_']' [in PLF.Hoare]
::x_'⊢'_x_'∈'_x [in PLF.RecordSub]
::x_'⊢'_x_'∈'_x [in PLF.Sub]
::'fail' [in PLF.Typechecking]
::'nosimpl'_x [in PLF.LibTactics]
::'Register'_x_x [in PLF.LibTactics]
::'return'_x [in PLF.Typechecking]
::'Something' [in PLF.LibTactics]
::'['_x_':='_x_']'_x [in PLF.Sub]
::'['_x_':='_x_']'_x [in PLF.RecordSub]
::'['_x_':='_x_']'_x [in PLF.Norm]
::'⊢'_x_'∈'_x [in PLF.Types]

---

Module Index

C

CImp [in PLF.Smallstep]
Combined [in PLF.Smallstep]

D

DeterministicImp [in PLF.UseAuto]

E

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

F

FirstTry [in PLF.Typechecking]

G

GenExample [in PLF.UseTactics]

H

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

I

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

L

LibTacticsCompatibility [in PLF.LibTactics]
Loop [in PLF.PE]

N

NaryExamples [in PLF.UseTactics]

P

PreservationProgressReferences [in PLF.UseAuto]
PreservationProgressStlc [in PLF.UseAuto]
ProductExtension [in PLF.Sub]

R

RepeatExercise [in PLF.Hoare]
RingDemo [in PLF.UseAuto]

S

Semantics [in PLF.UseAuto]
SimpleArith1 [in PLF.Smallstep]
SimpleArith2 [in PLF.Smallstep]
SimpleArith3 [in PLF.Smallstep]
SkipExample [in PLF.UseTactics]
SortExamples [in PLF.UseTactics]
StepFunction [in PLF.Typechecking]
STLC [in PLF.Stlc]
STLCArith [in PLF.StlcProp]
STLCChecker [in PLF.Typechecking]
STLCExtended [in PLF.MoreStlc]
STLCExtendedRecords [in PLF.Records]
STLCExtendedRecords.FirstTry [in PLF.Records]
STLCExtended.Examples [in PLF.MoreStlc]
STLCExtended.Examples.FixTest1 [in PLF.MoreStlc]
STLCExtended.Examples.FixTest2 [in PLF.MoreStlc]
STLCExtended.Examples.FixTest3 [in PLF.MoreStlc]
STLCExtended.Examples.FixTest4 [in PLF.MoreStlc]
STLCExtended.Examples.LetTest [in PLF.MoreStlc]
STLCExtended.Examples.ListTest [in PLF.MoreStlc]
STLCExtended.Examples.Numtest [in PLF.MoreStlc]
STLCExtended.Examples.Prodtest [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1 [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2 [in PLF.MoreStlc]
StlcImpl [in PLF.Typechecking]
STLCProp [in PLF.StlcProp]
STLCRef [in PLF.References]
STLCRef.ExampleVariables [in PLF.References]
STLCRef.RefsAndNontermination [in PLF.References]
STLCTypes [in PLF.Typechecking]
SubtypingInversion [in PLF.UseAuto]

T

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

U

UnfoldsExample [in PLF.UseTactics]

---

Variable Index

E

equatesLemma.A0 [in PLF.LibTactics]
equatesLemma.A1 [in PLF.LibTactics]
equatesLemma.A2 [in PLF.LibTactics]
equatesLemma.A3 [in PLF.LibTactics]
equatesLemma.A4 [in PLF.LibTactics]
equatesLemma.A5 [in PLF.LibTactics]
equatesLemma.A6 [in PLF.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

---

Constructor Index

A

abs [in PLF.Sub]
abs [in PLF.RecordSub]
abs [in PLF.Norm]
afi_abs [in PLF.Norm]
afi_abs [in PLF.RecordSub]
afi_abs [in PLF.Sub]
afi_app1 [in PLF.Norm]
afi_app1 [in PLF.RecordSub]
afi_app1 [in PLF.Sub]
afi_app2 [in PLF.Norm]
afi_app2 [in PLF.Sub]
afi_app2 [in PLF.RecordSub]
afi_fst [in PLF.Norm]
afi_pair1 [in PLF.Norm]
afi_pair2 [in PLF.Norm]
afi_proj [in PLF.RecordSub]
afi_rhead [in PLF.RecordSub]
afi_rtail [in PLF.RecordSub]
afi_snd [in PLF.Norm]
afi_test0 [in PLF.Norm]
afi_test1 [in PLF.Sub]
afi_test1 [in PLF.Norm]
afi_test2 [in PLF.Sub]
afi_test2 [in PLF.Norm]
afi_test3 [in PLF.Sub]
afi_var [in PLF.Norm]
afi_var [in PLF.Sub]
afi_var [in PLF.RecordSub]
app [in PLF.Norm]
app [in PLF.Sub]
app [in PLF.RecordSub]
Arrow [in PLF.Norm]
Arrow [in PLF.RecordSub]
Arrow [in PLF.Sub]
Assign [in PLF.PE]
AS_Id [in PLF.Smallstep]
AS_Minus [in PLF.Smallstep]
AS_Minus1 [in PLF.Smallstep]
AS_Minus2 [in PLF.Smallstep]
AS_Mult [in PLF.Smallstep]
AS_Mult1 [in PLF.Smallstep]
AS_Mult2 [in PLF.Smallstep]
AS_Plus [in PLF.Smallstep]
AS_Plus1 [in PLF.Smallstep]
AS_Plus2 [in PLF.Smallstep]
av_num [in PLF.Smallstep]

B

Base [in PLF.RecordSub]
Base [in PLF.Sub]
body [in PLF.PE]
Bool [in PLF.Norm]
Bool [in PLF.Types]
Bool [in PLF.Sub]
boxer [in PLF.LibTactics]
BS_AndFalse [in PLF.Smallstep]
BS_AndStep [in PLF.Smallstep]
BS_AndTrueFalse [in PLF.Smallstep]
BS_AndTrueStep [in PLF.Smallstep]
BS_AndTrueTrue [in PLF.Smallstep]
BS_Eq [in PLF.Smallstep]
BS_Eq₁ [in PLF.Smallstep]
BS_Eq₂ [in PLF.Smallstep]
BS_LtEq [in PLF.Smallstep]
BS_LtEq1 [in PLF.Smallstep]
BS_LtEq2 [in PLF.Smallstep]
BS_NotFalse [in PLF.Smallstep]
BS_NotStep [in PLF.Smallstep]
BS_NotTrue [in PLF.Smallstep]
bv_fls [in PLF.Types]
bv_tru [in PLF.Types]

C

C [in PLF.Smallstep]
CImp.CAss [in PLF.Smallstep]
CImp.CIf [in PLF.Smallstep]
CImp.CPar [in PLF.Smallstep]
CImp.CSeq [in PLF.Smallstep]
CImp.CSkip [in PLF.Smallstep]
CImp.CS_Ass [in PLF.Smallstep]
CImp.CS_AssStep [in PLF.Smallstep]
CImp.CS_IfFalse [in PLF.Smallstep]
CImp.CS_IfStep [in PLF.Smallstep]
CImp.CS_IfTrue [in PLF.Smallstep]
CImp.CS_ParDone [in PLF.Smallstep]
CImp.CS_Par1 [in PLF.Smallstep]
CImp.CS_Par2 [in PLF.Smallstep]
CImp.CS_SeqFinish [in PLF.Smallstep]
CImp.CS_SeqStep [in PLF.Smallstep]
CImp.CS_While [in PLF.Smallstep]
CImp.CWhile [in PLF.Smallstep]
Combined.C [in PLF.Smallstep]
Combined.fls [in PLF.Smallstep]
Combined.P [in PLF.Smallstep]
Combined.ST_If [in PLF.Smallstep]
Combined.ST_IfFalse [in PLF.Smallstep]
Combined.ST_IfTrue [in PLF.Smallstep]
Combined.ST_PlusConstConst [in PLF.Smallstep]
Combined.ST_Plus1 [in PLF.Smallstep]
Combined.ST_Plus2 [in PLF.Smallstep]
Combined.test [in PLF.Smallstep]
Combined.tru [in PLF.Smallstep]
Combined.v_const [in PLF.Smallstep]
Combined.v_fls [in PLF.Smallstep]
Combined.v_tru [in PLF.Smallstep]
CS_Ass [in PLF.Smallstep]
CS_AssStep [in PLF.Smallstep]
CS_IfFalse [in PLF.Smallstep]
CS_IfStep [in PLF.Smallstep]
CS_IfTrue [in PLF.Smallstep]
CS_SeqFinish [in PLF.Smallstep]
CS_SeqStep [in PLF.Smallstep]
CS_While [in PLF.Smallstep]

D

DCAsgn [in PLF.Hoare2]
DCIf [in PLF.Hoare2]
DCPost [in PLF.Hoare2]
DCPre [in PLF.Hoare2]
DCSeq [in PLF.Hoare2]
DCSkip [in PLF.Hoare2]
DCWhile [in PLF.Hoare2]
Decorated [in PLF.Hoare2]
done [in PLF.PE]

E

entry [in PLF.PE]
ev_SS [in PLF.Hoare2]
ev_0 [in PLF.Hoare2]
E_Const [in PLF.Smallstep]
E_None [in PLF.PE]
E_Plus [in PLF.Smallstep]
E_Some [in PLF.PE]

F

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

G

Goto [in PLF.PE]

H

Himp.CAsgn [in PLF.Hoare]
Himp.CAss [in PLF.Equiv]
Himp.CHavoc [in PLF.Equiv]
Himp.CHavoc [in PLF.Hoare]
Himp.CIf [in PLF.Equiv]
Himp.CIf [in PLF.Hoare]
Himp.CSeq [in PLF.Equiv]
Himp.CSeq [in PLF.Hoare]
Himp.CSkip [in PLF.Equiv]
Himp.CSkip [in PLF.Hoare]
Himp.CWhile [in PLF.Hoare]
Himp.CWhile [in PLF.Equiv]
Himp.E_Ass [in PLF.Equiv]
Himp.E_Ass [in PLF.Hoare]
Himp.E_Havoc [in PLF.Hoare]
Himp.E_IfFalse [in PLF.Equiv]
Himp.E_IfFalse [in PLF.Hoare]
Himp.E_IfTrue [in PLF.Hoare]
Himp.E_IfTrue [in PLF.Equiv]
Himp.E_Seq [in PLF.Hoare]
Himp.E_Seq [in PLF.Equiv]
Himp.E_Skip [in PLF.Equiv]
Himp.E_Skip [in PLF.Hoare]
Himp.E_WhileFalse [in PLF.Hoare]
Himp.E_WhileFalse [in PLF.Equiv]
Himp.E_WhileTrue [in PLF.Equiv]
Himp.E_WhileTrue [in PLF.Hoare]
HoareAssertAssume.CAss [in PLF.Hoare]
HoareAssertAssume.CAssert [in PLF.Hoare]
HoareAssertAssume.CAssume [in PLF.Hoare]
HoareAssertAssume.CIf [in PLF.Hoare]
HoareAssertAssume.CSeq [in PLF.Hoare]
HoareAssertAssume.CSkip [in PLF.Hoare]
HoareAssertAssume.CWhile [in PLF.Hoare]
HoareAssertAssume.E_Ass [in PLF.Hoare]
HoareAssertAssume.E_AssertFalse [in PLF.Hoare]
HoareAssertAssume.E_AssertTrue [in PLF.Hoare]
HoareAssertAssume.E_Assume [in PLF.Hoare]
HoareAssertAssume.E_IfFalse [in PLF.Hoare]
HoareAssertAssume.E_IfTrue [in PLF.Hoare]
HoareAssertAssume.E_SeqError [in PLF.Hoare]
HoareAssertAssume.E_SeqNormal [in PLF.Hoare]
HoareAssertAssume.E_Skip [in PLF.Hoare]
HoareAssertAssume.E_WhileFalse [in PLF.Hoare]
HoareAssertAssume.E_WhileTrueError [in PLF.Hoare]
HoareAssertAssume.E_WhileTrueNormal [in PLF.Hoare]
HoareAssertAssume.RError [in PLF.Hoare]
HoareAssertAssume.RNormal [in PLF.Hoare]
H_Asgn [in PLF.HoareAsLogic]
H_Consequence [in PLF.HoareAsLogic]
H_If [in PLF.HoareAsLogic]
H_Seq [in PLF.HoareAsLogic]
H_Skip [in PLF.HoareAsLogic]
H_While [in PLF.HoareAsLogic]

I

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

L

loop [in PLF.PE]
Loop.E'Ass [in PLF.PE]
Loop.E'IfFalse [in PLF.PE]
Loop.E'IfTrue [in PLF.PE]
Loop.E'Seq [in PLF.PE]
Loop.E'Skip [in PLF.PE]
Loop.E'WhileFalse [in PLF.PE]
Loop.E'WhileTrue [in PLF.PE]
Loop.PE_AssDynamic [in PLF.PE]
Loop.PE_AssStatic [in PLF.PE]
Loop.pe_ceval_count_intro [in PLF.PE]
Loop.PE_If [in PLF.PE]
Loop.PE_IfFalse [in PLF.PE]
Loop.PE_IfTrue [in PLF.PE]
Loop.PE_Seq [in PLF.PE]
Loop.PE_Skip [in PLF.PE]
Loop.PE_While [in PLF.PE]
Loop.PE_WhileFalse [in PLF.PE]
Loop.PE_WhileFixed [in PLF.PE]
Loop.PE_WhileFixedEnd [in PLF.PE]
Loop.PE_WhileFixedLoop [in PLF.PE]
Loop.PE_WhileTrue [in PLF.PE]
ltac_database_token [in PLF.LibTactics]
ltac_goal_to_discard_intro [in PLF.LibTactics]
ltac_mark [in PLF.LibTactics]
ltac_no_arg [in PLF.LibTactics]
ltac_wild [in PLF.LibTactics]
ltac_wilds [in PLF.LibTactics]

M

multi_refl [in PLF.Smallstep]
multi_step [in PLF.Smallstep]

N

Nat [in PLF.Types]
nv_scc [in PLF.Types]
nv_zro [in PLF.Types]

P

P [in PLF.Smallstep]
pair [in PLF.Norm]
PE_AssDynamic [in PLF.PE]
PE_AssStatic [in PLF.PE]
pe_ceval_intro [in PLF.PE]
PE_If [in PLF.PE]
PE_IfFalse [in PLF.PE]
PE_IfTrue [in PLF.PE]
pe_peval_intro [in PLF.PE]
PE_Seq [in PLF.PE]
PE_Skip [in PLF.PE]
prd [in PLF.Types]
Prod [in PLF.Norm]
ProductExtension.abs [in PLF.Sub]
ProductExtension.app [in PLF.Sub]
ProductExtension.Arrow [in PLF.Sub]
ProductExtension.Base [in PLF.Sub]
ProductExtension.Bool [in PLF.Sub]
ProductExtension.fls [in PLF.Sub]
ProductExtension.fst [in PLF.Sub]
ProductExtension.pair [in PLF.Sub]
ProductExtension.Prod [in PLF.Sub]
ProductExtension.snd [in PLF.Sub]
ProductExtension.test [in PLF.Sub]
ProductExtension.Top [in PLF.Sub]
ProductExtension.tru [in PLF.Sub]
ProductExtension.unit [in PLF.Sub]
ProductExtension.Unit [in PLF.Sub]
ProductExtension.var [in PLF.Sub]

R

rcons [in PLF.RecordSub]
RCons [in PLF.RecordSub]
RepeatExercise.CAsgn [in PLF.Hoare]
RepeatExercise.CIf [in PLF.Hoare]
RepeatExercise.CRepeat [in PLF.Hoare]
RepeatExercise.CSeq [in PLF.Hoare]
RepeatExercise.CSkip [in PLF.Hoare]
RepeatExercise.CWhile [in PLF.Hoare]
RepeatExercise.E_Ass [in PLF.Hoare]
RepeatExercise.E_IfFalse [in PLF.Hoare]
RepeatExercise.E_IfTrue [in PLF.Hoare]
RepeatExercise.E_Seq [in PLF.Hoare]
RepeatExercise.E_Skip [in PLF.Hoare]
RepeatExercise.E_WhileFalse [in PLF.Hoare]
RepeatExercise.E_WhileTrue [in PLF.Hoare]
RNil [in PLF.RecordSub]
rnil [in PLF.RecordSub]
rproj [in PLF.RecordSub]
rtcons [in PLF.RecordSub]
RTcons [in PLF.RecordSub]
rtnil [in PLF.RecordSub]
RTnil [in PLF.RecordSub]

S

scc [in PLF.Types]
SimpleArith1.ST_PlusConstConst [in PLF.Smallstep]
SimpleArith1.ST_Plus1 [in PLF.Smallstep]
SimpleArith1.ST_Plus2 [in PLF.Smallstep]
snd [in PLF.Norm]
SS_Load [in PLF.Smallstep]
SS_Minus [in PLF.Smallstep]
SS_Mult [in PLF.Smallstep]
SS_Plus [in PLF.Smallstep]
SS_Push [in PLF.Smallstep]
STLCArith.abs [in PLF.StlcProp]
STLCArith.app [in PLF.StlcProp]
STLCArith.Arrow [in PLF.StlcProp]
STLCArith.const [in PLF.StlcProp]
STLCArith.mlt [in PLF.StlcProp]
STLCArith.Nat [in PLF.StlcProp]
STLCArith.prd [in PLF.StlcProp]
STLCArith.scc [in PLF.StlcProp]
STLCArith.test0 [in PLF.StlcProp]
STLCArith.var [in PLF.StlcProp]
STLCExtendedRecords.abs [in PLF.Records]
STLCExtendedRecords.afi_abs [in PLF.Records]
STLCExtendedRecords.afi_app1 [in PLF.Records]
STLCExtendedRecords.afi_app2 [in PLF.Records]
STLCExtendedRecords.afi_proj [in PLF.Records]
STLCExtendedRecords.afi_rhead [in PLF.Records]
STLCExtendedRecords.afi_rtail [in PLF.Records]
STLCExtendedRecords.afi_var [in PLF.Records]
STLCExtendedRecords.app [in PLF.Records]
STLCExtendedRecords.Arrow [in PLF.Records]
STLCExtendedRecords.Base [in PLF.Records]
STLCExtendedRecords.FirstTry.Arrow [in PLF.Records]
STLCExtendedRecords.FirstTry.Base [in PLF.Records]
STLCExtendedRecords.FirstTry.TRcd [in PLF.Records]
STLCExtendedRecords.RCons [in PLF.Records]
STLCExtendedRecords.rcons [in PLF.Records]
STLCExtendedRecords.RNil [in PLF.Records]
STLCExtendedRecords.rproj [in PLF.Records]
STLCExtendedRecords.rtcons [in PLF.Records]
STLCExtendedRecords.RTcons [in PLF.Records]
STLCExtendedRecords.rtnil [in PLF.Records]
STLCExtendedRecords.RTnil [in PLF.Records]
STLCExtendedRecords.ST_AppAbs [in PLF.Records]
STLCExtendedRecords.ST_App1 [in PLF.Records]
STLCExtendedRecords.ST_App2 [in PLF.Records]
STLCExtendedRecords.ST_ProjRcd [in PLF.Records]
STLCExtendedRecords.ST_Proj1 [in PLF.Records]
STLCExtendedRecords.ST_Rcd_Head [in PLF.Records]
STLCExtendedRecords.ST_Rcd_Tail [in PLF.Records]
STLCExtendedRecords.trnil [in PLF.Records]
STLCExtendedRecords.T_Abs [in PLF.Records]
STLCExtendedRecords.T_App [in PLF.Records]
STLCExtendedRecords.T_Proj [in PLF.Records]
STLCExtendedRecords.T_RCons [in PLF.Records]
STLCExtendedRecords.T_RNil [in PLF.Records]
STLCExtendedRecords.T_Var [in PLF.Records]
STLCExtendedRecords.var [in PLF.Records]
STLCExtendedRecords.v_abs [in PLF.Records]
STLCExtendedRecords.v_rcons [in PLF.Records]
STLCExtendedRecords.v_rnil [in PLF.Records]
STLCExtendedRecords.wfArrow [in PLF.Records]
STLCExtendedRecords.wfBase [in PLF.Records]
STLCExtendedRecords.wfRCons [in PLF.Records]
STLCExtendedRecords.wfRNil [in PLF.Records]
STLCExtended.abs [in PLF.MoreStlc]
STLCExtended.afi_abs [in PLF.MoreStlc]
STLCExtended.afi_app1 [in PLF.MoreStlc]
STLCExtended.afi_app2 [in PLF.MoreStlc]
STLCExtended.afi_case0 [in PLF.MoreStlc]
STLCExtended.afi_case1 [in PLF.MoreStlc]
STLCExtended.afi_case2 [in PLF.MoreStlc]
STLCExtended.afi_cons1 [in PLF.MoreStlc]
STLCExtended.afi_cons2 [in PLF.MoreStlc]
STLCExtended.afi_inl [in PLF.MoreStlc]
STLCExtended.afi_inr [in PLF.MoreStlc]
STLCExtended.afi_lcase1 [in PLF.MoreStlc]
STLCExtended.afi_lcase2 [in PLF.MoreStlc]
STLCExtended.afi_lcase3 [in PLF.MoreStlc]
STLCExtended.afi_mult1 [in PLF.MoreStlc]
STLCExtended.afi_mult2 [in PLF.MoreStlc]
STLCExtended.afi_pred [in PLF.MoreStlc]
STLCExtended.afi_succ [in PLF.MoreStlc]
STLCExtended.afi_test01 [in PLF.MoreStlc]
STLCExtended.afi_test02 [in PLF.MoreStlc]
STLCExtended.afi_test03 [in PLF.MoreStlc]
STLCExtended.afi_var [in PLF.MoreStlc]
STLCExtended.app [in PLF.MoreStlc]
STLCExtended.Arrow [in PLF.MoreStlc]
STLCExtended.const [in PLF.MoreStlc]
STLCExtended.fst [in PLF.MoreStlc]
STLCExtended.List [in PLF.MoreStlc]
STLCExtended.mlt [in PLF.MoreStlc]
STLCExtended.Nat [in PLF.MoreStlc]
STLCExtended.pair [in PLF.MoreStlc]
STLCExtended.prd [in PLF.MoreStlc]
STLCExtended.Prod [in PLF.MoreStlc]
STLCExtended.scc [in PLF.MoreStlc]
STLCExtended.snd [in PLF.MoreStlc]
STLCExtended.ST_AppAbs [in PLF.MoreStlc]
STLCExtended.ST_App1 [in PLF.MoreStlc]
STLCExtended.ST_App2 [in PLF.MoreStlc]
STLCExtended.ST_Case [in PLF.MoreStlc]
STLCExtended.ST_CaseInl [in PLF.MoreStlc]
STLCExtended.ST_CaseInr [in PLF.MoreStlc]
STLCExtended.ST_Cons1 [in PLF.MoreStlc]
STLCExtended.ST_Cons2 [in PLF.MoreStlc]
STLCExtended.ST_Inl [in PLF.MoreStlc]
STLCExtended.ST_Inr [in PLF.MoreStlc]
STLCExtended.ST_LcaseCons [in PLF.MoreStlc]
STLCExtended.ST_LcaseNil [in PLF.MoreStlc]
STLCExtended.ST_Lcase1 [in PLF.MoreStlc]
STLCExtended.ST_Mulconsts [in PLF.MoreStlc]
STLCExtended.ST_Mult1 [in PLF.MoreStlc]
STLCExtended.ST_Mult2 [in PLF.MoreStlc]
STLCExtended.ST_Pred [in PLF.MoreStlc]
STLCExtended.ST_PredNat [in PLF.MoreStlc]
STLCExtended.ST_SuccNat [in PLF.MoreStlc]
STLCExtended.ST_Succ1 [in PLF.MoreStlc]
STLCExtended.ST_Test0Nonzero [in PLF.MoreStlc]
STLCExtended.ST_Test0Zero [in PLF.MoreStlc]
STLCExtended.ST_Test01 [in PLF.MoreStlc]
STLCExtended.Sum [in PLF.MoreStlc]
STLCExtended.tcase [in PLF.MoreStlc]
STLCExtended.tcons [in PLF.MoreStlc]
STLCExtended.test0 [in PLF.MoreStlc]
STLCExtended.tfix [in PLF.MoreStlc]
STLCExtended.tinl [in PLF.MoreStlc]
STLCExtended.tinr [in PLF.MoreStlc]
STLCExtended.tlcase [in PLF.MoreStlc]
STLCExtended.tlet [in PLF.MoreStlc]
STLCExtended.tnil [in PLF.MoreStlc]
STLCExtended.T_Abs [in PLF.MoreStlc]
STLCExtended.T_App [in PLF.MoreStlc]
STLCExtended.T_Case [in PLF.MoreStlc]
STLCExtended.T_Cons [in PLF.MoreStlc]
STLCExtended.T_Inl [in PLF.MoreStlc]
STLCExtended.T_Inr [in PLF.MoreStlc]
STLCExtended.T_Lcase [in PLF.MoreStlc]
STLCExtended.T_Mult [in PLF.MoreStlc]
STLCExtended.T_Nat [in PLF.MoreStlc]
STLCExtended.T_Nil [in PLF.MoreStlc]
STLCExtended.T_Pred [in PLF.MoreStlc]
STLCExtended.T_Succ [in PLF.MoreStlc]
STLCExtended.T_Test0 [in PLF.MoreStlc]
STLCExtended.T_Unit [in PLF.MoreStlc]
STLCExtended.T_Var [in PLF.MoreStlc]
STLCExtended.Unit [in PLF.MoreStlc]
STLCExtended.unit [in PLF.MoreStlc]
STLCExtended.var [in PLF.MoreStlc]
STLCExtended.v_abs [in PLF.MoreStlc]
STLCExtended.v_inl [in PLF.MoreStlc]
STLCExtended.v_inr [in PLF.MoreStlc]
STLCExtended.v_lcons [in PLF.MoreStlc]
STLCExtended.v_lnil [in PLF.MoreStlc]
STLCExtended.v_nat [in PLF.MoreStlc]
STLCExtended.v_pair [in PLF.MoreStlc]
STLCExtended.v_unit [in PLF.MoreStlc]
STLCProp.afi_abs [in PLF.StlcProp]
STLCProp.afi_app1 [in PLF.StlcProp]
STLCProp.afi_app2 [in PLF.StlcProp]
STLCProp.afi_test1 [in PLF.StlcProp]
STLCProp.afi_test2 [in PLF.StlcProp]
STLCProp.afi_test3 [in PLF.StlcProp]
STLCProp.afi_var [in PLF.StlcProp]
STLCRef.abs [in PLF.References]
STLCRef.afi_abs [in PLF.References]
STLCRef.afi_app1 [in PLF.References]
STLCRef.afi_app2 [in PLF.References]
STLCRef.afi_assign1 [in PLF.References]
STLCRef.afi_assign2 [in PLF.References]
STLCRef.afi_deref [in PLF.References]
STLCRef.afi_if0_1 [in PLF.References]
STLCRef.afi_if0_2 [in PLF.References]
STLCRef.afi_if0_3 [in PLF.References]
STLCRef.afi_mult1 [in PLF.References]
STLCRef.afi_mult2 [in PLF.References]
STLCRef.afi_pred [in PLF.References]
STLCRef.afi_ref [in PLF.References]
STLCRef.afi_succ [in PLF.References]
STLCRef.afi_var [in PLF.References]
STLCRef.app [in PLF.References]
STLCRef.Arrow [in PLF.References]
STLCRef.assign [in PLF.References]
STLCRef.const [in PLF.References]
STLCRef.deref [in PLF.References]
STLCRef.extends_cons [in PLF.References]
STLCRef.extends_nil [in PLF.References]
STLCRef.loc [in PLF.References]
STLCRef.mlt [in PLF.References]
STLCRef.Nat [in PLF.References]
STLCRef.prd [in PLF.References]
STLCRef.ref [in PLF.References]
STLCRef.Ref [in PLF.References]
STLCRef.RefsAndNontermination.sc_one [in PLF.References]
STLCRef.RefsAndNontermination.sc_step [in PLF.References]
STLCRef.scc [in PLF.References]
STLCRef.ST_AppAbs [in PLF.References]
STLCRef.ST_App1 [in PLF.References]
STLCRef.ST_App2 [in PLF.References]
STLCRef.ST_Assign [in PLF.References]
STLCRef.ST_Assign1 [in PLF.References]
STLCRef.ST_Assign2 [in PLF.References]
STLCRef.ST_Deref [in PLF.References]
STLCRef.ST_DerefLoc [in PLF.References]
STLCRef.ST_If₀ [in PLF.References]
STLCRef.ST_If0_Nonzero [in PLF.References]
STLCRef.ST_If0_Zero [in PLF.References]
STLCRef.ST_MultNats [in PLF.References]
STLCRef.ST_Mult1 [in PLF.References]
STLCRef.ST_Mult2 [in PLF.References]
STLCRef.ST_Pred [in PLF.References]
STLCRef.ST_PredNat [in PLF.References]
STLCRef.ST_Ref [in PLF.References]
STLCRef.ST_RefValue [in PLF.References]
STLCRef.ST_Succ [in PLF.References]
STLCRef.ST_SuccNat [in PLF.References]
STLCRef.test0 [in PLF.References]
STLCRef.T_Abs [in PLF.References]
STLCRef.T_App [in PLF.References]
STLCRef.T_Assign [in PLF.References]
STLCRef.T_Deref [in PLF.References]
STLCRef.T_If₀ [in PLF.References]
STLCRef.T_Loc [in PLF.References]
STLCRef.T_Mult [in PLF.References]
STLCRef.T_Nat [in PLF.References]
STLCRef.T_Pred [in PLF.References]
STLCRef.T_Ref [in PLF.References]
STLCRef.T_Succ [in PLF.References]
STLCRef.T_Unit [in PLF.References]
STLCRef.T_Var [in PLF.References]
STLCRef.Unit [in PLF.References]
STLCRef.unit [in PLF.References]
STLCRef.var [in PLF.References]
STLCRef.v_abs [in PLF.References]
STLCRef.v_loc [in PLF.References]
STLCRef.v_nat [in PLF.References]
STLCRef.v_unit [in PLF.References]
STLC.abs [in PLF.Stlc]
STLC.app [in PLF.Stlc]
STLC.Arrow [in PLF.Stlc]
STLC.Bool [in PLF.Stlc]
STLC.fls [in PLF.Stlc]
STLC.ST_AppAbs [in PLF.Stlc]
STLC.ST_App1 [in PLF.Stlc]
STLC.ST_App2 [in PLF.Stlc]
STLC.ST_Test [in PLF.Stlc]
STLC.ST_TestFls [in PLF.Stlc]
STLC.ST_TestTru [in PLF.Stlc]
STLC.s_var1 [in PLF.Stlc]
STLC.test [in PLF.Stlc]
STLC.tru [in PLF.Stlc]
STLC.T_Abs [in PLF.Stlc]
STLC.T_App [in PLF.Stlc]
STLC.T_Fls [in PLF.Stlc]
STLC.T_Test [in PLF.Stlc]
STLC.T_Tru [in PLF.Stlc]
STLC.T_Var [in PLF.Stlc]
STLC.var [in PLF.Stlc]
STLC.v_abs [in PLF.Stlc]
STLC.v_fls [in PLF.Stlc]
STLC.v_tru [in PLF.Stlc]
ST_AppAbs [in PLF.Sub]
ST_AppAbs [in PLF.RecordSub]
ST_AppAbs [in PLF.Norm]
ST_App1 [in PLF.RecordSub]
ST_App1 [in PLF.Sub]
ST_App1 [in PLF.Norm]
ST_App2 [in PLF.RecordSub]
ST_App2 [in PLF.Sub]
ST_App2 [in PLF.Norm]
ST_Fst [in PLF.Norm]
ST_FstPair [in PLF.Norm]
ST_Iszro [in PLF.Types]
ST_IszroScc [in PLF.Types]
ST_IszroZro [in PLF.Types]
ST_Pair1 [in PLF.Norm]
ST_Pair2 [in PLF.Norm]
ST_PlusConstConst [in PLF.Smallstep]
ST_Plus1 [in PLF.Smallstep]
ST_Plus2 [in PLF.Smallstep]
ST_Prd [in PLF.Types]
ST_PrdScc [in PLF.Types]
ST_PrdZro [in PLF.Types]
ST_ProjRcd [in PLF.RecordSub]
ST_Proj1 [in PLF.RecordSub]
ST_Rcd_Head [in PLF.RecordSub]
ST_Rcd_Tail [in PLF.RecordSub]
ST_Scc [in PLF.Types]
ST_Snd [in PLF.Norm]
ST_SndPair [in PLF.Norm]
ST_Test [in PLF.Norm]
ST_Test [in PLF.Types]
ST_Test [in PLF.Sub]
ST_TestFalse [in PLF.Norm]
ST_TestFalse [in PLF.Sub]
ST_TestFls [in PLF.Types]
ST_TestTru [in PLF.Types]
ST_TestTrue [in PLF.Sub]
ST_TestTrue [in PLF.Norm]
S_Arrow [in PLF.Sub]
S_Arrow [in PLF.RecordSub]
S_RcdDepth [in PLF.RecordSub]
S_RcdPerm [in PLF.RecordSub]
S_RcdWidth [in PLF.RecordSub]
S_Refl [in PLF.Sub]
S_Refl [in PLF.RecordSub]
S_Top [in PLF.RecordSub]
S_Top [in PLF.Sub]
S_Trans [in PLF.RecordSub]
S_Trans [in PLF.Sub]

T

Temp1.ST_PlusConstConst [in PLF.Smallstep]
Temp1.ST_Plus1 [in PLF.Smallstep]
Temp1.ST_Plus2 [in PLF.Smallstep]
Temp1.v_const [in PLF.Smallstep]
Temp1.v_funny [in PLF.Smallstep]
Temp2.ST_Funny [in PLF.Smallstep]
Temp2.ST_PlusConstConst [in PLF.Smallstep]
Temp2.ST_Plus1 [in PLF.Smallstep]
Temp2.ST_Plus2 [in PLF.Smallstep]
Temp2.v_const [in PLF.Smallstep]
Temp3.ST_PlusConstConst [in PLF.Smallstep]
Temp3.ST_Plus1 [in PLF.Smallstep]
Temp3.v_const [in PLF.Smallstep]
Temp4.fls [in PLF.Smallstep]
Temp4.ST_If [in PLF.Smallstep]
Temp4.ST_IfFalse [in PLF.Smallstep]
Temp4.ST_IfTrue [in PLF.Smallstep]
Temp4.Temp5.ST_If [in PLF.Smallstep]
Temp4.Temp5.ST_IfFalse [in PLF.Smallstep]
Temp4.Temp5.ST_IfTrue [in PLF.Smallstep]
Temp4.test [in PLF.Smallstep]
Temp4.tru [in PLF.Smallstep]
Temp4.v_fls [in PLF.Smallstep]
Temp4.v_tru [in PLF.Smallstep]
test [in PLF.Types]
test [in PLF.Norm]
test [in PLF.Sub]
Top [in PLF.RecordSub]
Top [in PLF.Sub]
tru [in PLF.Types]
tru [in PLF.Norm]
tru [in PLF.Sub]
T_Abs [in PLF.Norm]
T_Abs [in PLF.RecordSub]
T_Abs [in PLF.Sub]
T_App [in PLF.RecordSub]
T_App [in PLF.Sub]
T_App [in PLF.Norm]
T_False [in PLF.Norm]
T_False [in PLF.Sub]
T_Fls [in PLF.Types]
T_Fst [in PLF.Norm]
T_Iszro [in PLF.Types]
T_Pair [in PLF.Norm]
T_Prd [in PLF.Types]
T_Proj [in PLF.RecordSub]
T_RCons [in PLF.RecordSub]
T_RNil [in PLF.RecordSub]
T_Scc [in PLF.Types]
T_Snd [in PLF.Norm]
T_Sub [in PLF.Sub]
T_Sub [in PLF.RecordSub]
T_Test [in PLF.Norm]
T_Test [in PLF.Types]
T_Test [in PLF.Sub]
T_Tru [in PLF.Types]
T_True [in PLF.Norm]
T_True [in PLF.Sub]
T_Unit [in PLF.Sub]
T_Var [in PLF.RecordSub]
T_Var [in PLF.Sub]
T_Var [in PLF.Norm]
T_Zro [in PLF.Types]

U

Unit [in PLF.Sub]
unit [in PLF.Sub]

V

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

W

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

Z

zro [in PLF.Types]

---

Lemma Index

A

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

B

bassn_eval_false [in PLF.HoareAsLogic]
bequiv_example [in PLF.Equiv]
bexp_eval_false [in PLF.Hoare]
bexp_eval_true [in PLF.Hoare]
bool_canonical [in PLF.Types]

C

canonical_forms_of_arrow_types [in PLF.RecordSub]
canonical_forms_of_arrow_types [in PLF.Sub]
canonical_forms_of_Bool [in PLF.Sub]
CAss_congruence [in PLF.Equiv]
ceval_extensionality [in PLF.PE]
CIf_congruence [in PLF.Equiv]
CImp.par_body_n [in PLF.Smallstep]
CImp.par_body_n__Sn [in PLF.Smallstep]
CImp.par_loop_any_X [in PLF.Smallstep]
cmin_minimal [in PLF.Equiv]
compiler_is_correct [in PLF.Smallstep]
congruence_demo_1 [in PLF.UseAuto]
congruence_demo_2 [in PLF.UseAuto]
congruence_demo_3 [in PLF.UseAuto]
congruence_demo_4 [in PLF.UseAuto]
context_invariance [in PLF.Norm]
context_invariance [in PLF.RecordSub]
context_invariance [in PLF.Sub]
CSeq_congruence [in PLF.Equiv]
CWhile_congruence [in PLF.Equiv]
c3_c4_different [in PLF.Equiv]

D

dec_while_correct [in PLF.Hoare2]
demo_auto_absurd_1 [in PLF.UseAuto]
demo_auto_absurd_2 [in PLF.UseAuto]
demo_clears_all_and_clears_but [in PLF.LibTactics]
demo_false [in PLF.UseTactics]
demo_false [in PLF.UseAuto]
demo_false_arg [in PLF.UseTactics]
demo_hint_unfold_context_1 [in PLF.UseAuto]
demo_hint_unfold_context_2 [in PLF.UseAuto]
demo_hint_unfold_goal_1 [in PLF.UseAuto]
demo_hint_unfold_goal_2 [in PLF.UseAuto]
demo_tryfalse [in PLF.UseTactics]
DeterministicImp.ceval_deterministic [in PLF.UseAuto]
DeterministicImp.ceval_deterministic' [in PLF.UseAuto]
DeterministicImp.ceval_deterministic'' [in PLF.UseAuto]
DeterministicImp.ceval_deterministic''' [in PLF.UseAuto]
DeterministicImp.ceval_deterministic'''' [in PLF.UseAuto]
dfib_correct [in PLF.Hoare2]
div_mod_dec_correct [in PLF.Hoare2]
dpow2_down_correct [in PLF.Hoare2]
duplicate_subst [in PLF.Norm]
dup_lemma [in PLF.LibTactics]

E

EqualityExamples.demo_applys_eq_1 [in PLF.UseTactics]
EqualityExamples.demo_applys_eq_2 [in PLF.UseTactics]
EqualityExamples.demo_applys_eq_3 [in PLF.UseTactics]
EqualityExamples.demo_fequals [in PLF.UseTactics]
EqualityExamples.demo_substs [in PLF.UseTactics]
EqualityExamples.mult_0_plus [in PLF.UseTactics]
EqualityExamples.mult_0_plus' [in PLF.UseTactics]
EqualityExamples.mult_0_plus'' [in PLF.UseTactics]
equality_by_auto [in PLF.UseAuto]
equates_0 [in PLF.LibTactics]
equates_1 [in PLF.LibTactics]
equates_2 [in PLF.LibTactics]
equates_3 [in PLF.LibTactics]
equates_4 [in PLF.LibTactics]
equates_5 [in PLF.LibTactics]
equates_6 [in PLF.LibTactics]
evalF_eval [in PLF.Smallstep]
eval_assign [in PLF.PE]
eval__multistep [in PLF.Smallstep]
ExamplesInstantiations.substitution_preserves_typing [in PLF.UseTactics]
ExamplesLets.demo_lets_underscore [in PLF.UseTactics]
ExamplesLets.demo_lets_1 [in PLF.UseTactics]
ExamplesLets.demo_lets_2 [in PLF.UseTactics]
ExamplesLets.demo_lets_3 [in PLF.UseTactics]
ExamplesLets.demo_lets_4 [in PLF.UseTactics]
ExamplesLets.demo_lets_5 [in PLF.UseTactics]

F

False_and_P_imp [in PLF.HoareAsLogic]
fib_eqn [in PLF.Hoare2]
find_parity_correct [in PLF.Hoare2]
find_parity_correct' [in PLF.Hoare2]
fold_constants_aexp_sound [in PLF.Equiv]
fold_constants_bexp_sound [in PLF.Equiv]
fold_constants_com_sound [in PLF.Equiv]
free_in_context [in PLF.Sub]
free_in_context [in PLF.Norm]
free_in_context [in PLF.RecordSub]

G

GenExample.substitution_preserves_typing [in PLF.UseTactics]

H

has_type__wf [in PLF.RecordSub]
Himp.hoare_havoc [in PLF.Hoare]
Himp.ptwice_cequiv_pcopy [in PLF.Equiv]
Himp.pXY_cequiv_pYX [in PLF.Equiv]
Himp.p1_may_diverge [in PLF.Equiv]
Himp.p1_p2_equiv [in PLF.Equiv]
Himp.p2_may_diverge [in PLF.Equiv]
Himp.p3_p4_inequiv [in PLF.Equiv]
Himp.p5_p6_equiv [in PLF.Equiv]
Himp2.hoare_havoc_weakest [in PLF.Hoare2]
HoareAssertAssume.assert_assume_differ [in PLF.Hoare]
HoareAssertAssume.assert_implies_assume [in PLF.Hoare]
HoareAssertAssume.hoare_asgn [in PLF.Hoare]
HoareAssertAssume.hoare_consequence_post [in PLF.Hoare]
HoareAssertAssume.hoare_consequence_pre [in PLF.Hoare]
HoareAssertAssume.hoare_if [in PLF.Hoare]
HoareAssertAssume.hoare_seq [in PLF.Hoare]
HoareAssertAssume.hoare_skip [in PLF.Hoare]
HoareAssertAssume.hoare_while [in PLF.Hoare]
hoare_asgn [in PLF.Hoare]
hoare_asgn_fwd [in PLF.Hoare]
hoare_asgn_fwd_exists [in PLF.Hoare]
hoare_asgn_weakest [in PLF.Hoare2]
hoare_consequence [in PLF.Hoare]
hoare_consequence_post [in PLF.Hoare]
hoare_consequence_pre [in PLF.Hoare]
hoare_if [in PLF.Hoare]
hoare_post_true [in PLF.Hoare]
hoare_pre_false [in PLF.Hoare]
hoare_proof_complete [in PLF.HoareAsLogic]
hoare_proof_sound [in PLF.HoareAsLogic]
hoare_seq [in PLF.Hoare]
hoare_skip [in PLF.Hoare]
hoare_while [in PLF.Hoare]
H_Consequence_post [in PLF.HoareAsLogic]
H_Consequence_pre [in PLF.HoareAsLogic]
H_Post_True_deriv [in PLF.HoareAsLogic]
H_Pre_False_deriv [in PLF.HoareAsLogic]

I

identity_assignment [in PLF.Equiv]
iff_intro_swap [in PLF.LibTactics]
iff_trans [in PLF.Equiv]
If₁.hoare_if1_good [in PLF.Hoare]
if_minus_correct [in PLF.Hoare2]
if_minus_plus [in PLF.Hoare]
if_minus_plus_correct [in PLF.Hoare2]
inbP [in PLF.PE]
induct_height_max2 [in PLF.LibTactics]
inequiv_exercise [in PLF.Equiv]
instantiation_domains_match [in PLF.Norm]
instantiation_drop [in PLF.Norm]
instantiation_env_closed [in PLF.Norm]
instantiation_R [in PLF.Norm]
IntrovExamples.ceval_deterministic [in PLF.UseTactics]
IntrovExamples.ceval_deterministic' [in PLF.UseTactics]
IntrovExamples.dist_exists_or [in PLF.UseTactics]
IntrovExamples.exists_impl [in PLF.UseTactics]
InvertsExamples.ceval_deterministic [in PLF.UseTactics]
InvertsExamples.ceval_deterministic' [in PLF.UseTactics]
InvertsExamples.skip_left [in PLF.UseTactics]
InvertsExamples.skip_left' [in PLF.UseTactics]
is_wp_example [in PLF.Hoare2]

L

lookup_field_in_value [in PLF.RecordSub]
Loop.ceval_count_complete [in PLF.PE]
Loop.ceval_count_sound [in PLF.PE]
Loop.pe_ceval_count_le [in PLF.PE]
Loop.pe_compare_nil_lookup [in PLF.PE]
Loop.pe_compare_nil_update [in PLF.PE]
Loop.pe_com_complete [in PLF.PE]
Loop.pe_com_correct [in PLF.PE]
Loop.pe_com_sound [in PLF.PE]
loop_unrolling [in PLF.Equiv]
ltac_database_provide [in PLF.LibTactics]
ltac_something_eq [in PLF.LibTactics]
ltac_something_hide [in PLF.LibTactics]
ltac_something_show [in PLF.LibTactics]
l₁ [in PLF.Hoare2]
l₂ [in PLF.Hoare2]
l₃ [in PLF.Hoare2]
l₃' [in PLF.Hoare2]
l₄ [in PLF.Hoare2]

M

msubst_abs [in PLF.Norm]
msubst_app [in PLF.Norm]
msubst_closed [in PLF.Norm]
msubst_preserves_typing [in PLF.Norm]
msubst_R [in PLF.Norm]
msubst_var [in PLF.Norm]
multistep_App2 [in PLF.Norm]
multistep_congr_1 [in PLF.Smallstep]
multistep_congr_2 [in PLF.Smallstep]
multistep_preserves_R [in PLF.Norm]
multistep_preserves_R' [in PLF.Norm]
multistep__eval [in PLF.Smallstep]
multi_R [in PLF.Smallstep]
multi_trans [in PLF.Smallstep]
mupdate_drop [in PLF.Norm]
mupdate_lookup [in PLF.Norm]

N

NaryExamples.demo_branch [in PLF.UseTactics]
NaryExamples.demo_splits [in PLF.UseTactics]
nat_canonical [in PLF.Types]
nat_le_refl [in PLF.UseAuto]
negation_study_1 [in PLF.UseAuto]
negation_study_2 [in PLF.UseAuto]
nf_is_value [in PLF.Smallstep]
nf_same_as_value [in PLF.Smallstep]
normalization [in PLF.Norm]
normalize_ex [in PLF.Smallstep]
normalize_ex' [in PLF.Smallstep]
normal_forms_unique [in PLF.Smallstep]

O

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

P

parity_correct [in PLF.Hoare2]
parity_dec_correct [in PLF.Hoare2]
parity_ge_2 [in PLF.Hoare2]
parity_lt_2 [in PLF.Hoare2]
pe_add_correct [in PLF.PE]
pe_aexp_correct [in PLF.PE]
pe_aexp_correct_weak [in PLF.PE]
pe_bexp_correct [in PLF.PE]
pe_block_correct [in PLF.PE]
pe_compare_correct [in PLF.PE]
pe_compare_removes [in PLF.PE]
pe_compare_update [in PLF.PE]
pe_com_complete [in PLF.PE]
pe_com_correct [in PLF.PE]
pe_com_sound [in PLF.PE]
pe_consistent_update [in PLF.PE]
pe_disagree_domain [in PLF.PE]
pe_domain [in PLF.PE]
pe_program_correct [in PLF.PE]
pe_removes_correct [in PLF.PE]
pe_remove_correct [in PLF.PE]
pe_unique_correct [in PLF.PE]
pe_update_consistent [in PLF.PE]
pe_update_correct [in PLF.PE]
pe_update_update_add [in PLF.PE]
pe_update_update_remove [in PLF.PE]
pow2_le_1 [in PLF.Hoare2]
pow2_plus_1 [in PLF.Hoare2]
preservation [in PLF.RecordSub]
preservation [in PLF.Sub]
preservation [in PLF.Norm]
preservation [in PLF.Types]
PreservationProgressReferences.nth_eq_last' [in PLF.UseAuto]
PreservationProgressReferences.preservation [in PLF.UseAuto]
PreservationProgressReferences.preservation' [in PLF.UseAuto]
PreservationProgressReferences.preservation_ref [in PLF.UseAuto]
PreservationProgressReferences.progress [in PLF.UseAuto]
PreservationProgressStlc.preservation [in PLF.UseAuto]
PreservationProgressStlc.preservation' [in PLF.UseAuto]
PreservationProgressStlc.progress [in PLF.UseAuto]
PreservationProgressStlc.progress' [in PLF.UseAuto]
preservation' [in PLF.Types]
ProductExtension.preservation [in PLF.Sub]
ProductExtension.progress [in PLF.Sub]
progress [in PLF.RecordSub]
progress [in PLF.Sub]
progress [in PLF.Types]

R

rcd_types_match [in PLF.RecordSub]
reduce_to_zero_correct' [in PLF.Hoare2]
refl_aequiv [in PLF.Equiv]
refl_bequiv [in PLF.Equiv]
refl_cequiv [in PLF.Equiv]
RepeatExercise.ex1_repeat_works [in PLF.Hoare]
RingDemo.ring_demo [in PLF.UseAuto]
R_halts [in PLF.Norm]
R_typable_empty [in PLF.Norm]

S

search_depth_0 [in PLF.UseAuto]
search_depth_1 [in PLF.UseAuto]
search_depth_3 [in PLF.UseAuto]
search_depth_4 [in PLF.UseAuto]
search_depth_5 [in PLF.UseAuto]
Semantics.multistep_eval_ind [in PLF.UseAuto]
Semantics.multistep__eval [in PLF.UseAuto]
Semantics.multistep__eval' [in PLF.UseAuto]
Semantics.multistep__eval'' [in PLF.UseAuto]
seq_assoc [in PLF.Equiv]
silly1 [in PLF.Hoare]
silly2 [in PLF.Hoare]
silly2_eassumption [in PLF.Hoare]
silly2_fixed [in PLF.Hoare]
SimpleArith2.step_deterministic [in PLF.Smallstep]
SimpleArith3.step_deterministic_alt [in PLF.Smallstep]
SkipExample.ceval_deterministic [in PLF.UseTactics]
SkipExample.demo_admits [in PLF.UseTactics]
SkipExample.mult_plus_0 [in PLF.UseTactics]
skip_left [in PLF.Equiv]
skip_right [in PLF.Equiv]
slow_assignment_dec_correct [in PLF.Hoare2]
solved_by_jauto [in PLF.UseAuto]
solving_by_apply [in PLF.UseAuto]
solving_by_eapply [in PLF.UseAuto]
solving_by_reflexivity [in PLF.UseAuto]
solving_conj_goal [in PLF.UseAuto]
solving_conj_hyp [in PLF.UseAuto]
solving_conj_hyp' [in PLF.UseAuto]
solving_conj_hyp_forall [in PLF.UseAuto]
solving_conj_more [in PLF.UseAuto]
solving_disj_goal [in PLF.UseAuto]
solving_disj_hyp [in PLF.UseAuto]
solving_exists_goal [in PLF.UseAuto]
solving_exists_hyp [in PLF.UseAuto]
solving_tauto [in PLF.UseAuto]
SortExamples.ceval_deterministic [in PLF.UseTactics]
soundness [in PLF.Types]
sqrt_correct [in PLF.Hoare2]
square_dec'_correct [in PLF.Hoare2]
square_dec_correct [in PLF.Hoare2]
square_simpler_dec_correct [in PLF.Hoare2]
stack_step_deterministic [in PLF.Smallstep]
StepFunction.complete_stepf [in PLF.Typechecking]
StepFunction.sound_stepf [in PLF.Typechecking]
step_deterministic [in PLF.Norm]
step_deterministic [in PLF.Smallstep]
step_deterministic [in PLF.Types]
step_normalizing [in PLF.Smallstep]
step_preserves_halting [in PLF.Norm]
step_preserves_R [in PLF.Norm]
step_preserves_record_tm [in PLF.RecordSub]
step_preserves_R' [in PLF.Norm]
step__eval [in PLF.Smallstep]
STLCChecker.type_checking_complete [in PLF.Typechecking]
STLCChecker.type_checking_sound [in PLF.Typechecking]
STLCExtendedRecords.context_invariance [in PLF.Records]
STLCExtendedRecords.free_in_context [in PLF.Records]
STLCExtendedRecords.has_type__wf [in PLF.Records]
STLCExtendedRecords.lookup_field_in_value [in PLF.Records]
STLCExtendedRecords.preservation [in PLF.Records]
STLCExtendedRecords.progress [in PLF.Records]
STLCExtendedRecords.step_preserves_record_tm [in PLF.Records]
STLCExtendedRecords.substitution_preserves_typing [in PLF.Records]
STLCExtendedRecords.typing_example_2 [in PLF.Records]
STLCExtendedRecords.wf_rcd_lookup [in PLF.Records]
STLCExtended.context_invariance [in PLF.MoreStlc]
STLCExtended.free_in_context [in PLF.MoreStlc]
STLCExtended.preservation [in PLF.MoreStlc]
STLCExtended.progress [in PLF.MoreStlc]
STLCExtended.substitution_preserves_typing [in PLF.MoreStlc]
STLCProp.canonical_forms_bool [in PLF.StlcProp]
STLCProp.canonical_forms_fun [in PLF.StlcProp]
STLCProp.context_invariance [in PLF.StlcProp]
STLCProp.free_in_context [in PLF.StlcProp]
STLCProp.preservation [in PLF.StlcProp]
STLCProp.progress [in PLF.StlcProp]
STLCProp.progress' [in PLF.StlcProp]
STLCProp.soundness [in PLF.StlcProp]
STLCProp.substitution_preserves_typing [in PLF.StlcProp]
STLCProp.typable_empty__closed [in PLF.StlcProp]
STLCProp.unique_types [in PLF.StlcProp]
STLCRef.assign_pres_store_typing [in PLF.References]
STLCRef.context_invariance [in PLF.References]
STLCRef.extends_app [in PLF.References]
STLCRef.extends_lookup [in PLF.References]
STLCRef.extends_refl [in PLF.References]
STLCRef.free_in_context [in PLF.References]
STLCRef.length_extends [in PLF.References]
STLCRef.length_replace [in PLF.References]
STLCRef.lookup_replace_eq [in PLF.References]
STLCRef.lookup_replace_neq [in PLF.References]
STLCRef.nth_eq_last [in PLF.References]
STLCRef.preservation [in PLF.References]
STLCRef.preservation_wrong1 [in PLF.References]
STLCRef.preservation_wrong2 [in PLF.References]
STLCRef.progress [in PLF.References]
STLCRef.RefsAndNontermination.factorial_type [in PLF.References]
STLCRef.RefsAndNontermination.loop_fun_step_self [in PLF.References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [in PLF.References]
STLCRef.RefsAndNontermination.loop_typeable [in PLF.References]
STLCRef.replace_nil [in PLF.References]
STLCRef.store_weakening [in PLF.References]
STLCRef.store_well_typed_app [in PLF.References]
STLCRef.substitution_preserves_typing [in PLF.References]
STLCTypes.eqb_ty_refl [in PLF.Typechecking]
STLCTypes.eqb_ty__eq [in PLF.Typechecking]
STLC.step_example1 [in PLF.Stlc]
STLC.step_example1' [in PLF.Stlc]
STLC.step_example2 [in PLF.Stlc]
STLC.step_example2' [in PLF.Stlc]
STLC.step_example3 [in PLF.Stlc]
STLC.step_example3' [in PLF.Stlc]
STLC.step_example4 [in PLF.Stlc]
STLC.step_example4' [in PLF.Stlc]
STLC.step_example5 [in PLF.Stlc]
STLC.step_example5_with_normalize [in PLF.Stlc]
STLC.substi_correct [in PLF.Stlc]
strong_progress [in PLF.Smallstep]
substitution_preserves_typing [in PLF.RecordSub]
substitution_preserves_typing [in PLF.Sub]
substitution_preserves_typing [in PLF.Norm]
subst_closed [in PLF.Norm]
subst_inequiv [in PLF.Equiv]
subst_msubst [in PLF.Norm]
subst_not_afi [in PLF.Norm]
subtract_slowly_dec_correct [in PLF.Hoare2]
subtype__wf [in PLF.RecordSub]
SubtypingInversion.abs_arrow [in PLF.UseAuto]
SubtypingInversion.abs_arrow' [in PLF.UseAuto]
sub_inversion_arrow [in PLF.RecordSub]
sub_inversion_arrow [in PLF.Sub]
sub_inversion_Bool [in PLF.Sub]
swap_correct [in PLF.Hoare2]
swap_exercise [in PLF.Hoare]
swap_if_branches [in PLF.Equiv]
swap_noninterfering_assignments [in PLF.Equiv]
swap_subst [in PLF.Norm]
sym_aequiv [in PLF.Equiv]
sym_bequiv [in PLF.Equiv]
sym_cequiv [in PLF.Equiv]

T

Temp1.value_not_same_as_normal_form [in PLF.Smallstep]
Temp2.value_not_same_as_normal_form [in PLF.Smallstep]
Temp3.value_not_same_as_normal_form [in PLF.Smallstep]
Temp4.step_deterministic [in PLF.Smallstep]
Temp4.strong_progress [in PLF.Smallstep]
TEST_false [in PLF.Equiv]
test_multistep_1 [in PLF.Smallstep]
test_multistep_1' [in PLF.Smallstep]
test_multistep_2 [in PLF.Smallstep]
test_multistep_3 [in PLF.Smallstep]
test_multistep_4 [in PLF.Smallstep]
TEST_true [in PLF.Equiv]
TEST_true_simple [in PLF.Equiv]
transitivity_bad_hint_1 [in PLF.UseAuto]
transitivity_workaround_1 [in PLF.UseAuto]
transitivity_workaround_2 [in PLF.UseAuto]
trans_aequiv [in PLF.Equiv]
trans_bequiv [in PLF.Equiv]
trans_cequiv [in PLF.Equiv]
two_loops_correct [in PLF.Hoare2]
typable_empty__closed [in PLF.Norm]
TypecheckerExtensions.eqb_ty_refl [in PLF.Typechecking]
TypecheckerExtensions.eqb_ty__eq [in PLF.Typechecking]
TypecheckerExtensions.type_checking_complete [in PLF.Typechecking]
TypecheckerExtensions.type_checking_sound [in PLF.Typechecking]
typing_inversion_abs [in PLF.RecordSub]
typing_inversion_abs [in PLF.Sub]
typing_inversion_app [in PLF.RecordSub]
typing_inversion_app [in PLF.Sub]
typing_inversion_false [in PLF.Sub]
typing_inversion_if [in PLF.Sub]
typing_inversion_proj [in PLF.RecordSub]
typing_inversion_rcons [in PLF.RecordSub]
typing_inversion_true [in PLF.Sub]
typing_inversion_unit [in PLF.Sub]
typing_inversion_var [in PLF.RecordSub]
typing_inversion_var [in PLF.Sub]

U

UnfoldsExample.bexp_eval_true [in PLF.UseTactics]

V

vacuous_substitution [in PLF.Norm]
value_halts [in PLF.Norm]
value_is_nf [in PLF.Smallstep]
value_is_nf [in PLF.Types]
value__normal [in PLF.Norm]
verification_correct [in PLF.Hoare2]
verification_correct_dec [in PLF.Hoare2]

W

wf_rcd_lookup [in PLF.RecordSub]
WHILE_false [in PLF.Equiv]
WHILE_true [in PLF.Equiv]
WHILE_true_nonterm [in PLF.Equiv]
working_of_auto_1 [in PLF.UseAuto]
working_of_auto_2 [in PLF.UseAuto]
wp_is_precondition [in PLF.HoareAsLogic]
wp_is_weakest [in PLF.HoareAsLogic]

Z

zprop_preserving [in PLF.Equiv]

---

Axiom Index

E

EqualityExamples.big_expression_using [in PLF.UseTactics]
ExamplesLets.typing_inversion_var [in PLF.UseTactics]

G

gt_not_le [in PLF.UseAuto]

I

inj_pair2 [in PLF.LibTactics]

L

le_gt_false [in PLF.UseAuto]
le_not_gt [in PLF.UseAuto]

P

P [in PLF.UseAuto]

S

subtype [in PLF.UseAuto]
subtype_refl [in PLF.UseAuto]
subtype_trans [in PLF.UseAuto]

T

typ [in PLF.UseAuto]

---

Inductive Index

A

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

B

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

C

CImp.com [in PLF.Smallstep]
CImp.cstep [in PLF.Smallstep]
Combined.step [in PLF.Smallstep]
Combined.tm [in PLF.Smallstep]
Combined.value [in PLF.Smallstep]
cstep [in PLF.Smallstep]

D

dcom [in PLF.Hoare2]
decorated [in PLF.Hoare2]

E

ev [in PLF.Hoare2]
eval [in PLF.Smallstep]

H

has_type [in PLF.Sub]
has_type [in PLF.RecordSub]
has_type [in PLF.Types]
has_type [in PLF.Norm]
Himp.ceval [in PLF.Hoare]
Himp.ceval [in PLF.Equiv]
Himp.com [in PLF.Hoare]
Himp.com [in PLF.Equiv]
HoareAssertAssume.ceval [in PLF.Hoare]
HoareAssertAssume.com [in PLF.Hoare]
HoareAssertAssume.result [in PLF.Hoare]
hoare_proof [in PLF.HoareAsLogic]

I

If₁.ceval [in PLF.Hoare]
If₁.com [in PLF.Hoare]
instantiation [in PLF.Norm]

L

Loop.ceval_count [in PLF.PE]
Loop.pe_ceval_count [in PLF.PE]
Loop.pe_com [in PLF.PE]
Ltac_database_token [in PLF.LibTactics]
ltac_goal_to_discard [in PLF.LibTactics]
ltac_Mark [in PLF.LibTactics]
ltac_No_arg [in PLF.LibTactics]
ltac_Wild [in PLF.LibTactics]
ltac_Wilds [in PLF.LibTactics]

M

multi [in PLF.Smallstep]

N

nvalue [in PLF.Types]

P

parity_label [in PLF.PE]
peval [in PLF.PE]
pe_ceval [in PLF.PE]
pe_com [in PLF.PE]
pe_peval [in PLF.PE]
ProductExtension.tm [in PLF.Sub]
ProductExtension.ty [in PLF.Sub]

R

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

S

SimpleArith1.step [in PLF.Smallstep]
stack_step [in PLF.Smallstep]
step [in PLF.Sub]
step [in PLF.Types]
step [in PLF.RecordSub]
step [in PLF.Smallstep]
step [in PLF.Norm]
STLCArith.tm [in PLF.StlcProp]
STLCArith.ty [in PLF.StlcProp]
STLCExtendedRecords.appears_free_in [in PLF.Records]
STLCExtendedRecords.FirstTry.ty [in PLF.Records]
STLCExtendedRecords.has_type [in PLF.Records]
STLCExtendedRecords.record_tm [in PLF.Records]
STLCExtendedRecords.record_ty [in PLF.Records]
STLCExtendedRecords.step [in PLF.Records]
STLCExtendedRecords.tm [in PLF.Records]
STLCExtendedRecords.ty [in PLF.Records]
STLCExtendedRecords.value [in PLF.Records]
STLCExtendedRecords.well_formed_ty [in PLF.Records]
STLCExtended.appears_free_in [in PLF.MoreStlc]
STLCExtended.has_type [in PLF.MoreStlc]
STLCExtended.step [in PLF.MoreStlc]
STLCExtended.tm [in PLF.MoreStlc]
STLCExtended.ty [in PLF.MoreStlc]
STLCExtended.value [in PLF.MoreStlc]
STLCProp.appears_free_in [in PLF.StlcProp]
STLCRef.appears_free_in [in PLF.References]
STLCRef.extends [in PLF.References]
STLCRef.has_type [in PLF.References]
STLCRef.RefsAndNontermination.step_closure [in PLF.References]
STLCRef.step [in PLF.References]
STLCRef.tm [in PLF.References]
STLCRef.ty [in PLF.References]
STLCRef.value [in PLF.References]
STLC.has_type [in PLF.Stlc]
STLC.step [in PLF.Stlc]
STLC.substi [in PLF.Stlc]
STLC.tm [in PLF.Stlc]
STLC.ty [in PLF.Stlc]
STLC.value [in PLF.Stlc]
subtype [in PLF.RecordSub]
subtype [in PLF.Sub]

T

Temp1.step [in PLF.Smallstep]
Temp1.value [in PLF.Smallstep]
Temp2.step [in PLF.Smallstep]
Temp2.value [in PLF.Smallstep]
Temp3.step [in PLF.Smallstep]
Temp3.value [in PLF.Smallstep]
Temp4.step [in PLF.Smallstep]
Temp4.Temp5.step [in PLF.Smallstep]
Temp4.tm [in PLF.Smallstep]
Temp4.value [in PLF.Smallstep]
tm [in PLF.Smallstep]
tm [in PLF.RecordSub]
tm [in PLF.Norm]
tm [in PLF.Types]
tm [in PLF.Sub]
ty [in PLF.Norm]
ty [in PLF.RecordSub]
ty [in PLF.Types]
ty [in PLF.Sub]

V

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

W

well_formed_ty [in PLF.RecordSub]

---

Section Index

D

DemoAbsurd1 [in PLF.UseAuto]

E

equatesLemma [in PLF.LibTactics]

H

HintsTransitivity [in PLF.UseAuto]

---

Abbreviation Index

E

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

M

multistep [in PLF.Norm]

S

step_normal_form [in PLF.Types]
step_normal_form [in PLF.Norm]
STLCExtendedRecords.A [in PLF.Records]
STLCExtendedRecords.a [in PLF.Records]
STLCExtendedRecords.B [in PLF.Records]
STLCExtendedRecords.f [in PLF.Records]
STLCExtendedRecords.g [in PLF.Records]
STLCExtendedRecords.i1 [in PLF.Records]
STLCExtendedRecords.i2 [in PLF.Records]
STLCExtendedRecords.k [in PLF.Records]
STLCExtendedRecords.l [in PLF.Records]
STLCExtendedRecords.multistep [in PLF.Records]
STLCExtended.Examples.a [in PLF.MoreStlc]
STLCExtended.Examples.eo [in PLF.MoreStlc]
STLCExtended.Examples.eq [in PLF.MoreStlc]
STLCExtended.Examples.even [in PLF.MoreStlc]
STLCExtended.Examples.evenodd [in PLF.MoreStlc]
STLCExtended.Examples.f [in PLF.MoreStlc]
STLCExtended.Examples.g [in PLF.MoreStlc]
STLCExtended.Examples.i1 [in PLF.MoreStlc]
STLCExtended.Examples.i2 [in PLF.MoreStlc]
STLCExtended.Examples.k [in PLF.MoreStlc]
STLCExtended.Examples.l [in PLF.MoreStlc]
STLCExtended.Examples.m [in PLF.MoreStlc]
STLCExtended.Examples.n [in PLF.MoreStlc]
STLCExtended.Examples.odd [in PLF.MoreStlc]
STLCExtended.Examples.processSum [in PLF.MoreStlc]
STLCExtended.Examples.x [in PLF.MoreStlc]
STLCExtended.Examples.y [in PLF.MoreStlc]
STLCExtended.multistep [in PLF.MoreStlc]
STLC.idB [in PLF.Stlc]
STLC.idBB [in PLF.Stlc]
STLC.idBBBB [in PLF.Stlc]
STLC.k [in PLF.Stlc]
STLC.multistep [in PLF.Stlc]
STLC.notB [in PLF.Stlc]

---

Definition Index

A

aequiv [in PLF.Equiv]
Assertion [in PLF.Hoare]
assert_implies [in PLF.Hoare]
assign [in PLF.PE]
assigned [in PLF.PE]
assn_sub [in PLF.Hoare]
assn_sub_example [in PLF.Hoare]
assn_sub_example2 [in PLF.Hoare]
atrans_sound [in PLF.Equiv]

B

bassn [in PLF.Hoare]
bequiv [in PLF.Equiv]
btrans_sound [in PLF.Equiv]

C

capprox [in PLF.Equiv]
cequiv [in PLF.Equiv]
CImp.cmultistep [in PLF.Smallstep]
CImp.par_loop [in PLF.Smallstep]
CImp.par_loop_example_0 [in PLF.Smallstep]
CImp.par_loop_example_2 [in PLF.Smallstep]
closed [in PLF.Norm]
closed_env [in PLF.Norm]
cmin [in PLF.Equiv]
COIND [in PLF.LibTactics]
compiler_is_correct_statement [in PLF.Smallstep]
congruence_example [in PLF.Equiv]
context [in PLF.Norm]
context [in PLF.RecordSub]
context [in PLF.Sub]
ctrans_sound [in PLF.Equiv]
c₃ [in PLF.Equiv]
c₄ [in PLF.Equiv]

D

dec0 [in PLF.Hoare2]
dec1 [in PLF.Hoare2]
dec_correct [in PLF.Hoare2]
dec_while [in PLF.Hoare2]
deterministic [in PLF.Smallstep]
dfib [in PLF.Hoare2]
div_mod_dec [in PLF.Hoare2]
dpow2_down [in PLF.Hoare2]
drop [in PLF.Norm]

E

empty_pe_state [in PLF.PE]
env [in PLF.Norm]
equiv_classes [in PLF.Equiv]
eq' [in PLF.LibTactics]
evalF [in PLF.Smallstep]
Examples.Employee [in PLF.Sub]
Examples.Person [in PLF.Sub]
Examples.Student [in PLF.Sub]
Examples.subtyping_example_0 [in PLF.RecordSub]
Examples.subtyping_example_0 [in PLF.Sub]
Examples.subtyping_example_1 [in PLF.Sub]
Examples.subtyping_example_1 [in PLF.RecordSub]
Examples.subtyping_example_2 [in PLF.RecordSub]
Examples.subtyping_example_2 [in PLF.Sub]
Examples.subtyping_example_3 [in PLF.RecordSub]
Examples.subtyping_example_4 [in PLF.RecordSub]
Examples.sub_employee_person [in PLF.Sub]
Examples.sub_student_person [in PLF.Sub]
Examples.TRcd_j [in PLF.RecordSub]
Examples.TRcd_kj [in PLF.RecordSub]
Examples2.trcd_kj [in PLF.RecordSub]
Examples2.typing_example_0 [in PLF.RecordSub]
Examples2.typing_example_1 [in PLF.RecordSub]
Examples2.typing_example_2 [in PLF.RecordSub]
ExAssertions.as1 [in PLF.Hoare]
ExAssertions.as2 [in PLF.Hoare]
ExAssertions.as3 [in PLF.Hoare]
ExAssertions.as4 [in PLF.Hoare]
ExAssertions.as5 [in PLF.Hoare]
ExAssertions.as6 [in PLF.Hoare]
extract [in PLF.Hoare2]
extract_dec [in PLF.Hoare2]

F

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

H

halts [in PLF.Norm]
has_type_not [in PLF.Types]
has_type_1 [in PLF.Types]
Himp.cequiv [in PLF.Equiv]
Himp.havoc_example1 [in PLF.Equiv]
Himp.havoc_example2 [in PLF.Equiv]
Himp.havoc_pre [in PLF.Hoare]
Himp.hoare_triple [in PLF.Hoare]
Himp.manual_grade_for_Check_rule_for_HAVOC [in PLF.Equiv]
Himp.pcopy [in PLF.Equiv]
Himp.ptwice [in PLF.Equiv]
Himp.pXY [in PLF.Equiv]
Himp.pYX [in PLF.Equiv]
Himp.p1 [in PLF.Equiv]
Himp.p2 [in PLF.Equiv]
Himp.p3 [in PLF.Equiv]
Himp.p4 [in PLF.Equiv]
Himp.p5 [in PLF.Equiv]
Himp.p6 [in PLF.Equiv]
HoareAssertAssume.assert_assume_example [in PLF.Hoare]
HoareAssertAssume.hoare_triple [in PLF.Hoare]
hoare_asgn_example1 [in PLF.Hoare]
hoare_asgn_example1' [in PLF.Hoare]
hoare_asgn_example3 [in PLF.Hoare]
hoare_asgn_example4 [in PLF.Hoare]
hoare_triple [in PLF.Hoare]

I

If₁.hoare_triple [in PLF.Hoare]
if_example [in PLF.Hoare]
if_minus_dec [in PLF.Hoare2]
if_minus_plus_com [in PLF.Hoare2]
if_minus_plus_dec [in PLF.Hoare2]
inb [in PLF.PE]
InvertsExamples.typing_nonexample_1 [in PLF.UseTactics]
is_wp [in PLF.Hoare2]

K

keval [in PLF.PE]
keval_example [in PLF.PE]

L

lookup [in PLF.Norm]
Loop.pe_loop_example1 [in PLF.PE]
Loop.pe_loop_example2 [in PLF.PE]
Loop.pe_loop_example3 [in PLF.PE]
Loop.pe_loop_example4 [in PLF.PE]
Loop.square_loop [in PLF.PE]
ltac_database [in PLF.LibTactics]
ltac_int_to_nat [in PLF.LibTactics]
ltac_something [in PLF.LibTactics]
ltac_tag_subst [in PLF.LibTactics]
ltac_to_generalize [in PLF.LibTactics]

M

manual_grade_for_arrow_sub_wrong [in PLF.Sub]
manual_grade_for_check_defn_of_slow_assignment_dec [in PLF.Hoare2]
manual_grade_for_combined_properties [in PLF.Smallstep]
manual_grade_for_decorations_in_factorial [in PLF.Hoare2]
manual_grade_for_decorations_in_if_minus_plus_reloaded [in PLF.Hoare2]
manual_grade_for_decorations_in_Min_Hoare [in PLF.Hoare2]
manual_grade_for_decorations_in_slow_assignment [in PLF.Hoare2]
manual_grade_for_decorations_in_two_loops [in PLF.Hoare2]
manual_grade_for_equiv_classes [in PLF.Equiv]
manual_grade_for_eval__multistep_inf [in PLF.Smallstep]
manual_grade_for_factorial_dec [in PLF.Hoare2]
manual_grade_for_finish_preservation_informal [in PLF.Types]
manual_grade_for_finish_progress_informal [in PLF.Types]
manual_grade_for_hoarestate1 [in PLF.Hoare]
manual_grade_for_hoare_asgn_examples [in PLF.Hoare]
manual_grade_for_hoare_asgn_examples_2 [in PLF.Hoare]
manual_grade_for_hoare_asgn_wrong [in PLF.Hoare]
manual_grade_for_hoare_repeat [in PLF.Hoare]
manual_grade_for_if1_hoare [in PLF.Hoare]
manual_grade_for_norm [in PLF.Norm]
manual_grade_for_norm_fail [in PLF.Norm]
manual_grade_for_pair_permutation [in PLF.Sub]
manual_grade_for_preservation [in PLF.Sub]
manual_grade_for_progress [in PLF.Sub]
manual_grade_for_prog_pres_bigstep [in PLF.Types]
manual_grade_for_proper_subtypes [in PLF.Sub]
manual_grade_for_rcd_types_match_informal [in PLF.RecordSub]
manual_grade_for_remove_predzro [in PLF.Types]
manual_grade_for_smallest_1 [in PLF.Sub]
manual_grade_for_smallest_2 [in PLF.Sub]
manual_grade_for_small_large_1 [in PLF.Sub]
manual_grade_for_small_large_2 [in PLF.Sub]
manual_grade_for_small_large_4 [in PLF.Sub]
manual_grade_for_subject_expansion [in PLF.Types]
manual_grade_for_subtype_concepts_tf [in PLF.Sub]
manual_grade_for_subtype_instances_tf_2 [in PLF.Sub]
manual_grade_for_subtype_order [in PLF.Sub]
manual_grade_for_variations [in PLF.Sub]
manual_grade_for_variation1 [in PLF.Types]
manual_grade_for_variation2 [in PLF.Types]
msubst [in PLF.Norm]
multistep [in PLF.Types]
mupdate [in PLF.Norm]
myFact [in PLF.UseAuto]

N

normalizing [in PLF.Smallstep]
normal_form [in PLF.Smallstep]
normal_form_of [in PLF.Smallstep]

P

parity [in PLF.PE]
parity [in PLF.Hoare2]
parity_body [in PLF.PE]
parity_dec [in PLF.Hoare2]
parity_eval [in PLF.PE]
pe_add [in PLF.PE]
pe_aexp [in PLF.PE]
pe_bexp [in PLF.PE]
pe_block [in PLF.PE]
pe_block_example [in PLF.PE]
pe_compare [in PLF.PE]
pe_consistent [in PLF.PE]
pe_disagree_at [in PLF.PE]
pe_example1 [in PLF.PE]
pe_example2 [in PLF.PE]
pe_example3 [in PLF.PE]
pe_lookup [in PLF.PE]
pe_program [in PLF.PE]
pe_remove [in PLF.PE]
pe_removes [in PLF.PE]
pe_state [in PLF.PE]
pe_unique [in PLF.PE]
pe_update [in PLF.PE]
post [in PLF.Hoare2]
post_dec [in PLF.Hoare2]
pow2 [in PLF.Hoare2]
pre_dec [in PLF.Hoare2]
prog [in PLF.Smallstep]
program [in PLF.PE]
prog_a [in PLF.Equiv]
prog_b [in PLF.Equiv]
prog_c [in PLF.Equiv]
prog_d [in PLF.Equiv]
prog_e [in PLF.Equiv]
prog_f [in PLF.Equiv]
prog_g [in PLF.Equiv]
prog_h [in PLF.Equiv]
prog_i [in PLF.Equiv]

R

R [in PLF.Norm]
real_fact [in PLF.Hoare2]
reduce_to_zero' [in PLF.Hoare2]
relation [in PLF.Smallstep]
RepeatExercise.ex1_repeat [in PLF.Hoare]
RepeatExercise.hoare_triple [in PLF.Hoare]
rm [in PLF.LibTactics]

S

sample_proof [in PLF.HoareAsLogic]
scc_hastype_nat__hastype_nat [in PLF.Types]
SimpleArith1.test_step_1 [in PLF.Smallstep]
SimpleArith1.test_step_2 [in PLF.Smallstep]
slow_assignment_dec [in PLF.Hoare2]
some_term_is_stuck [in PLF.Types]
sqrt_dec [in PLF.Hoare2]
square_dec [in PLF.Hoare2]
square_dec' [in PLF.Hoare2]
square_simpler_dec [in PLF.Hoare2]
stack [in PLF.Smallstep]
stack_multistep [in PLF.Smallstep]
StepFunction.stepf [in PLF.Typechecking]
step_example1 [in PLF.Smallstep]
step_example1' [in PLF.Smallstep]
step_example1'' [in PLF.Smallstep]
step_example1''' [in PLF.Smallstep]
step_normal_form [in PLF.Smallstep]
STLCArith.manual_grade_for_stlc_arith [in PLF.StlcProp]
STLCChecker.type_check [in PLF.Typechecking]
STLCExtendedRecords.context [in PLF.Records]
STLCExtendedRecords.FirstTry.alist [in PLF.Records]
STLCExtendedRecords.subst [in PLF.Records]
STLCExtendedRecords.Tlookup [in PLF.Records]
STLCExtendedRecords.tlookup [in PLF.Records]
STLCExtendedRecords.typing_nonexample [in PLF.Records]
STLCExtendedRecords.typing_nonexample_2 [in PLF.Records]
STLCExtendedRecords.weird_type [in PLF.Records]
STLCExtended.context [in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.fact [in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.reduces [in PLF.MoreStlc]
STLCExtended.Examples.FixTest1.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.map [in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.reduces [in PLF.MoreStlc]
STLCExtended.Examples.FixTest2.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.equal [in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.reduces [in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.reduces2 [in PLF.MoreStlc]
STLCExtended.Examples.FixTest3.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.eotest [in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.reduces [in PLF.MoreStlc]
STLCExtended.Examples.FixTest4.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.LetTest.reduces [in PLF.MoreStlc]
STLCExtended.Examples.LetTest.test [in PLF.MoreStlc]
STLCExtended.Examples.LetTest.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.ListTest.reduces [in PLF.MoreStlc]
STLCExtended.Examples.ListTest.test [in PLF.MoreStlc]
STLCExtended.Examples.ListTest.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.Numtest.numtest_reduces [in PLF.MoreStlc]
STLCExtended.Examples.Numtest.test [in PLF.MoreStlc]
STLCExtended.Examples.Numtest.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.reduces [in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.test [in PLF.MoreStlc]
STLCExtended.Examples.Prodtest.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.reduces [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.test [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest1.typechecks [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.reduces [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.test [in PLF.MoreStlc]
STLCExtended.Examples.Sumtest2.typechecks [in PLF.MoreStlc]
STLCExtended.manual_grade_for_context_invariance [in PLF.MoreStlc]
STLCExtended.manual_grade_for_extensions_definition [in PLF.MoreStlc]
STLCExtended.manual_grade_for_preservation [in PLF.MoreStlc]
STLCExtended.manual_grade_for_progress [in PLF.MoreStlc]
STLCExtended.manual_grade_for_substitution_preserves_typing [in PLF.MoreStlc]
STLCExtended.subst [in PLF.MoreStlc]
STLCProp.closed [in PLF.StlcProp]
STLCProp.manual_grade_for_afi [in PLF.StlcProp]
STLCProp.manual_grade_for_progress_preservation_statement [in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation1 [in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation2 [in PLF.StlcProp]
STLCProp.manual_grade_for_stlc_variation3 [in PLF.StlcProp]
STLCProp.manual_grade_for_subject_expansion_stlc [in PLF.StlcProp]
STLCProp.stuck [in PLF.StlcProp]
STLCRef.context [in PLF.References]
STLCRef.ExampleVariables.r [in PLF.References]
STLCRef.ExampleVariables.s [in PLF.References]
STLCRef.ExampleVariables.x [in PLF.References]
STLCRef.ExampleVariables.y [in PLF.References]
STLCRef.manual_grade_for_compact_update [in PLF.References]
STLCRef.manual_grade_for_cyclic_store [in PLF.References]
STLCRef.manual_grade_for_preservation_informal [in PLF.References]
STLCRef.manual_grade_for_store_not_unique [in PLF.References]
STLCRef.manual_grade_for_type_safety_violation [in PLF.References]
STLCRef.multistep [in PLF.References]
STLCRef.preservation_theorem [in PLF.References]
STLCRef.RefsAndNontermination.factorial [in PLF.References]
STLCRef.RefsAndNontermination.loop [in PLF.References]
STLCRef.RefsAndNontermination.loop_fun [in PLF.References]
STLCRef.RefsAndNontermination.multistep1 [in PLF.References]
STLCRef.replace [in PLF.References]
STLCRef.store [in PLF.References]
STLCRef.store_lookup [in PLF.References]
STLCRef.store_Tlookup [in PLF.References]
STLCRef.store_ty [in PLF.References]
STLCRef.store_well_typed [in PLF.References]
STLCRef.subst [in PLF.References]
STLCRef.tseq [in PLF.References]
STLCTypes.eqb_ty [in PLF.Typechecking]
STLC.context [in PLF.Stlc]
STLC.subst [in PLF.Stlc]
STLC.typing_example_1 [in PLF.Stlc]
STLC.typing_example_1' [in PLF.Stlc]
STLC.typing_example_2 [in PLF.Stlc]
STLC.typing_example_2_full [in PLF.Stlc]
STLC.typing_example_3 [in PLF.Stlc]
STLC.typing_nonexample_1 [in PLF.Stlc]
STLC.typing_nonexample_3 [in PLF.Stlc]
STLC.x [in PLF.Stlc]
STLC.y [in PLF.Stlc]
STLC.z [in PLF.Stlc]
stuck [in PLF.Types]
subst [in PLF.Sub]
subst [in PLF.Norm]
subst [in PLF.RecordSub]
subst_aexp [in PLF.Equiv]
subst_aexp_ex [in PLF.Equiv]
subst_equiv_property [in PLF.Equiv]
subtract_slowly_dec [in PLF.Hoare2]
swap [in PLF.Hoare2]
swap_dec [in PLF.Hoare2]
swap_program [in PLF.Hoare]

T

T [in PLF.Hoare2]
tass [in PLF.Norm]
Temp4.bool_step_prop1 [in PLF.Smallstep]
Temp4.bool_step_prop2 [in PLF.Smallstep]
Temp4.bool_step_prop3 [in PLF.Smallstep]
Temp4.manual_grade_for_smallstep_bools [in PLF.Smallstep]
Temp4.Temp5.bool_step_prop4 [in PLF.Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in PLF.Smallstep]
test_pe_aexp1 [in PLF.PE]
test_pe_bexp1 [in PLF.PE]
test_pe_bexp2 [in PLF.PE]
test_pe_update [in PLF.PE]
text_pe_aexp2 [in PLF.PE]
Tlookup [in PLF.RecordSub]
tlookup [in PLF.RecordSub]
two_loops_dec [in PLF.Hoare2]
TypecheckerExtensions.eqb_ty [in PLF.Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_complete [in PLF.Typechecking]
TypecheckerExtensions.manual_grade_for_type_checking_sound [in PLF.Typechecking]
TypecheckerExtensions.type_check [in PLF.Typechecking]

V

value [in PLF.Types]
verification_conditions [in PLF.Hoare2]
verification_conditions_dec [in PLF.Hoare2]

W

while_example [in PLF.Hoare]
wp [in PLF.HoareAsLogic]

Z

zprop [in PLF.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

:

_

(1933 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

:

_

(132 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

_

(66 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

_

(7 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

_

(22 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

_

(686 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

_

(457 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

_

(11 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

_

(123 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

_

(3 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

_

(55 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

_

(371 entries)