| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2515 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (73 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (500 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (622 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (738 entries) |
Global Index
A
aequiv [definition, in Equiv]aequiv_example [lemma, in Equiv]
aeval_weakening [lemma, in Equiv]
Aexp [definition, in Hoare]
Aexp_of_aexp [definition, in Hoare]
Aexp_of_nat [definition, in Hoare]
afi_snd [constructor, in Norm]
afi_fst [constructor, in Norm]
afi_pair2 [constructor, in Norm]
afi_pair1 [constructor, in Norm]
afi_test2 [constructor, in Norm]
afi_test1 [constructor, in Norm]
afi_test0 [constructor, in Norm]
afi_abs [constructor, in Norm]
afi_app2 [constructor, in Norm]
afi_app1 [constructor, in Norm]
afi_var [constructor, in Norm]
always_loop_hoare [lemma, in Hoare]
appears_free_in_sind [definition, in Norm]
appears_free_in_ind [definition, in Norm]
appears_free_in [inductive, in Norm]
applys_eq_step [lemma, in LibTactics]
applys_eq_step_dep [lemma, in LibTactics]
applys_eq_init [lemma, in LibTactics]
args_eq_7 [lemma, in LibTactics]
args_eq_6 [lemma, in LibTactics]
args_eq_5 [lemma, in LibTactics]
args_eq_4 [lemma, in LibTactics]
args_eq_3 [lemma, in LibTactics]
args_eq_2 [lemma, in LibTactics]
args_eq_1 [lemma, in LibTactics]
Assertion [definition, in Hoare]
assertion_sub_ex2' [definition, in Hoare]
assertion_sub_ex1' [definition, in Hoare]
assertion_sub_example2'' [definition, in Hoare]
assertion_sub_example2' [definition, in Hoare]
assertion_sub_example2 [definition, in Hoare]
assertion_sub_example [definition, in Hoare]
assertion_sub [definition, in Hoare]
assert_implies [definition, in Hoare]
assert_of_Prop [definition, in Hoare]
Assign [constructor, in PE]
assign [definition, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
astep [inductive, in Smallstep]
astep_sind [definition, in Smallstep]
astep_ind [definition, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
aval [inductive, in Smallstep]
aval_sind [definition, in Smallstep]
aval_ind [definition, in Smallstep]
av_num [constructor, in Smallstep]
B
bassertion [definition, in Hoare]bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
bexp_eval_false [lemma, in Hoare]
Bib [library]
block [inductive, in PE]
block_sind [definition, in PE]
block_rec [definition, in PE]
block_ind [definition, in PE]
block_rect [definition, in PE]
body [constructor, in PE]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
Boxer_sind [definition, in LibTactics]
Boxer_rec [definition, in LibTactics]
Boxer_ind [definition, in LibTactics]
Boxer_rect [definition, in LibTactics]
bstep [inductive, in Smallstep]
bstep_sind [definition, in Smallstep]
bstep_ind [definition, in Smallstep]
BS_AndTrueFalse [constructor, in Smallstep]
BS_AndTrueTrue [constructor, in Smallstep]
BS_AndFalse [constructor, in Smallstep]
BS_AndTrueStep [constructor, in Smallstep]
BS_AndStep [constructor, in Smallstep]
BS_NotFalse [constructor, in Smallstep]
BS_NotTrue [constructor, in Smallstep]
BS_NotStep [constructor, in Smallstep]
BS_LtEq [constructor, in Smallstep]
BS_LtEq2 [constructor, in Smallstep]
BS_LtEq1 [constructor, in Smallstep]
BS_Eq [constructor, in Smallstep]
BS_Eq2 [constructor, in Smallstep]
BS_Eq1 [constructor, in Smallstep]
btrans_sound [definition, in Equiv]
C
C [constructor, in Smallstep]capprox [definition, in Equiv]
CAsgn_congruence [lemma, in Equiv]
cequiv [definition, in Equiv]
ceval_extensionality [lemma, in PE]
CIf_congruence [lemma, in Equiv]
CImp [module, in Smallstep]
CImp.CAsgn [constructor, in Smallstep]
CImp.CIf [constructor, in Smallstep]
CImp.cmultistep [definition, in Smallstep]
CImp.com [inductive, in Smallstep]
CImp.com_sind [definition, in Smallstep]
CImp.com_rec [definition, in Smallstep]
CImp.com_ind [definition, in Smallstep]
CImp.com_rect [definition, in Smallstep]
CImp.CPar [constructor, in Smallstep]
CImp.CSeq [constructor, in Smallstep]
CImp.CSkip [constructor, in Smallstep]
CImp.cstep [inductive, in Smallstep]
CImp.cstep_sind [definition, in Smallstep]
CImp.cstep_ind [definition, in Smallstep]
CImp.CS_ParDone [constructor, in Smallstep]
CImp.CS_Par2 [constructor, in Smallstep]
CImp.CS_Par1 [constructor, in Smallstep]
CImp.CS_While [constructor, in Smallstep]
CImp.CS_IfFalse [constructor, in Smallstep]
CImp.CS_IfTrue [constructor, in Smallstep]
CImp.CS_IfStep [constructor, in Smallstep]
CImp.CS_SeqFinish [constructor, in Smallstep]
CImp.CS_SeqStep [constructor, in Smallstep]
CImp.CS_Asgn [constructor, in Smallstep]
CImp.CS_AsgnStep [constructor, in Smallstep]
CImp.CWhile [constructor, in Smallstep]
CImp.par_loop_any_X [lemma, in Smallstep]
CImp.par_body_n [lemma, in Smallstep]
CImp.par_body_n__Sn [lemma, in Smallstep]
CImp.par_loop_example_2 [definition, in Smallstep]
CImp.par_loop_example_0 [definition, in Smallstep]
CImp.par_loop [definition, in Smallstep]
com:_ ; _ [notation, in Smallstep]
com:_ := _ [notation, in Smallstep]
com:_ || _ [notation, in Smallstep]
com:if _ then _ else _ end [notation, in Smallstep]
com:skip [notation, in Smallstep]
com:while _ do _ end [notation, in Smallstep]
_ / _ -->* _ / _ [notation, in Smallstep]
_ / _ --> _ / _ [notation, in Smallstep]
closed [definition, in Norm]
closed_env [definition, in Norm]
cmin [definition, in Equiv]
cmin_minimal [lemma, in Equiv]
COIND [definition, in LibTactics]
Combined [module, in Smallstep]
Combined.C [constructor, in Smallstep]
Combined.combined_strong_progress [lemma, in Smallstep]
Combined.combined_step_deterministic [lemma, in Smallstep]
Combined.fls [constructor, in Smallstep]
Combined.P [constructor, in Smallstep]
Combined.step [inductive, in Smallstep]
Combined.step_sind [definition, in Smallstep]
Combined.step_ind [definition, in Smallstep]
Combined.ST_If [constructor, in Smallstep]
Combined.ST_IfFalse [constructor, in Smallstep]
Combined.ST_IfTrue [constructor, in Smallstep]
Combined.ST_Plus2 [constructor, in Smallstep]
Combined.ST_Plus1 [constructor, in Smallstep]
Combined.ST_PlusConstConst [constructor, in Smallstep]
Combined.test [constructor, in Smallstep]
Combined.tm [inductive, in Smallstep]
Combined.tm_sind [definition, in Smallstep]
Combined.tm_rec [definition, in Smallstep]
Combined.tm_ind [definition, in Smallstep]
Combined.tm_rect [definition, in Smallstep]
Combined.tru [constructor, in Smallstep]
Combined.value [inductive, in Smallstep]
Combined.value_sind [definition, in Smallstep]
Combined.value_ind [definition, in Smallstep]
Combined.v_fls [constructor, in Smallstep]
Combined.v_tru [constructor, in Smallstep]
Combined.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
compiler_is_correct [lemma, in Smallstep]
compiler_is_correct_statement [definition, in Smallstep]
congruence_demo_3 [lemma, in UseAuto]
congruence_demo_4 [lemma, in UseAuto]
congruence_demo_2 [lemma, in UseAuto]
congruence_demo_1 [lemma, in UseAuto]
congruence_example [definition, in Equiv]
context [definition, in Norm]
context_invariance [lemma, in Norm]
CSeq_congruence [lemma, in Equiv]
cstep [inductive, in Smallstep]
cstep_sind [definition, in Smallstep]
cstep_ind [definition, in Smallstep]
CS_While [constructor, in Smallstep]
CS_IfFalse [constructor, in Smallstep]
CS_IfTrue [constructor, in Smallstep]
CS_IfStep [constructor, in Smallstep]
CS_SeqFinish [constructor, in Smallstep]
CS_SeqStep [constructor, in Smallstep]
CS_Asgn [constructor, in Smallstep]
CS_AsgnStep [constructor, in Smallstep]
ctrans_sound [definition, in Equiv]
CWhile_congruence [lemma, in Equiv]
c3 [definition, in Equiv]
c3_c4_different [lemma, in Equiv]
c4 [definition, in Equiv]
D
DCAsgn [constructor, in Hoare2]DCIf [constructor, in Hoare2]
dcom [inductive, in Hoare2]
DComFirstTry [module, in Hoare2]
DComFirstTry.DCAsgn [constructor, in Hoare2]
DComFirstTry.DCIf [constructor, in Hoare2]
DComFirstTry.dcom [inductive, in Hoare2]
DComFirstTry.dcom_sind [definition, in Hoare2]
DComFirstTry.dcom_rec [definition, in Hoare2]
DComFirstTry.dcom_ind [definition, in Hoare2]
DComFirstTry.dcom_rect [definition, in Hoare2]
DComFirstTry.DCPost [constructor, in Hoare2]
DComFirstTry.DCPre [constructor, in Hoare2]
DComFirstTry.DCSeq [constructor, in Hoare2]
DComFirstTry.DCSkip [constructor, in Hoare2]
DComFirstTry.DCWhile [constructor, in Hoare2]
dcom_sind [definition, in Hoare2]
dcom_rec [definition, in Hoare2]
dcom_ind [definition, in Hoare2]
dcom_rect [definition, in Hoare2]
DCPost [constructor, in Hoare2]
DCPre [constructor, in Hoare2]
DCSeq [constructor, in Hoare2]
DCSkip [constructor, in Hoare2]
DCWhile [constructor, in Hoare2]
Decorated [constructor, in Hoare2]
decorated [inductive, in Hoare2]
decorated_sind [definition, in Hoare2]
decorated_rec [definition, in Hoare2]
decorated_ind [definition, in Hoare2]
decorated_rect [definition, in Hoare2]
dec_while_correct [lemma, in Hoare2]
dec_while_triple_correct [definition, in Hoare2]
dec_while [definition, in Hoare2]
dec0 [definition, in Hoare2]
dec1 [definition, in Hoare2]
def_with_exists [definition, in LibTactics]
DemoAbsurd1 [section, in UseAuto]
demo_false [lemma, in UseAuto]
demo_auto_absurd_2 [lemma, in UseAuto]
demo_auto_absurd_1 [lemma, in UseAuto]
demo_hint_unfold_context_2 [lemma, in UseAuto]
demo_hint_unfold_context_1 [lemma, in UseAuto]
demo_hint_unfold_goal_2 [lemma, in UseAuto]
demo_hint_unfold_goal_1 [lemma, in UseAuto]
demo_tryfalse [lemma, in UseTactics]
demo_false_arg [lemma, in UseTactics]
demo_false [lemma, in UseTactics]
demo_clears_all_and_clears_but [lemma, in LibTactics]
derivable [inductive, in HoareAsLogic]
derivable_sind [definition, in HoareAsLogic]
derivable_rec [definition, in HoareAsLogic]
derivable_ind [definition, in HoareAsLogic]
derivable_rect [definition, in HoareAsLogic]
deterministic [definition, in Smallstep]
DeterministicImp [module, in UseAuto]
DeterministicImp.ceval_deterministic'''' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic''' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic'' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic' [lemma, in UseAuto]
DeterministicImp.ceval_deterministic [lemma, in UseAuto]
dfib [definition, in Hoare2]
dfib_correct [lemma, in Hoare2]
div_mod_outer_triple_valid [lemma, in Hoare2]
div_mod_dec [definition, in Hoare2]
done [constructor, in PE]
dpow2_down_correct [lemma, in Hoare2]
dpow2_dec [definition, in Hoare2]
drop [definition, in Norm]
duplicate_subst [lemma, in Norm]
dup_lemma [lemma, in LibTactics]
E
empty_pe_state [definition, in PE]entry [constructor, in PE]
env [definition, in Norm]
EqualityExamples [module, in UseTactics]
EqualityExamples.big_expression_using [axiom, in UseTactics]
EqualityExamples.demo_applys_eq_2 [lemma, in UseTactics]
EqualityExamples.demo_applys_eq_1 [lemma, in UseTactics]
EqualityExamples.demo_fequals [lemma, in UseTactics]
EqualityExamples.demo_substs [lemma, in UseTactics]
EqualityExamples.mult_0_plus'' [lemma, in UseTactics]
EqualityExamples.mult_0_plus [lemma, in UseTactics]
equality_by_auto [lemma, in UseAuto]
equatesLemma [section, in LibTactics]
equatesLemma.A0 [variable, in LibTactics]
equatesLemma.A1 [variable, in LibTactics]
equatesLemma.A2 [variable, in LibTactics]
equatesLemma.A3 [variable, in LibTactics]
equatesLemma.A4 [variable, in LibTactics]
equatesLemma.A5 [variable, in LibTactics]
equatesLemma.A6 [variable, in LibTactics]
equates_6 [lemma, in LibTactics]
equates_5 [lemma, in LibTactics]
equates_4 [lemma, in LibTactics]
equates_3 [lemma, in LibTactics]
equates_2 [lemma, in LibTactics]
equates_1 [lemma, in LibTactics]
equates_0 [lemma, in LibTactics]
Equiv [library]
equiv_classes [definition, in Equiv]
eq' [definition, in LibTactics]
erase [definition, in Hoare2]
erase_while_ex [definition, in Hoare2]
erase_d [definition, in Hoare2]
eval [inductive, in Smallstep]
evalF [definition, in Smallstep]
evalF_eval [lemma, in Smallstep]
eval__multistep [lemma, in Smallstep]
eval_sind [definition, in Smallstep]
eval_ind [definition, in Smallstep]
eval_assign [lemma, in PE]
ExampleAssertionSub [module, in Hoare]
ExampleAssertionSub.equivalent_assertion2 [definition, in Hoare]
ExampleAssertionSub.equivalent_assertion1 [definition, in Hoare]
ExamplePrettyAssertions [module, in Hoare]
ExamplePrettyAssertions.assertion1 [definition, in Hoare]
ExamplePrettyAssertions.assertion2 [definition, in Hoare]
ExamplePrettyAssertions.assertion3 [definition, in Hoare]
ExamplePrettyAssertions.assertion4 [definition, in Hoare]
ExamplePrettyAssertions.assertion5 [definition, in Hoare]
ExamplePrettyAssertions.assertion6 [definition, in Hoare]
ExamplePrettyAssertions.assertion7 [definition, in Hoare]
ExamplePrettyAssertions.assertion8 [definition, in Hoare]
ExamplePrettyAssertions.assertion9 [definition, in Hoare]
ExamplesLets [module, in UseTactics]
ExamplesLets.demo_lets_underscore [lemma, in UseTactics]
ExamplesLets.demo_lets_5 [lemma, in UseTactics]
ExamplesLets.demo_lets_4 [lemma, in UseTactics]
ExamplesLets.demo_lets_3 [lemma, in UseTactics]
ExamplesLets.demo_lets_2 [lemma, in UseTactics]
ExamplesLets.demo_lets_1 [lemma, in UseTactics]
ExamplesLets.typing_inversion_var [axiom, in UseTactics]
ExAssertions [module, in Hoare]
ExAssertions.assertion1 [definition, in Hoare]
ExAssertions.assertion2 [definition, in Hoare]
ExAssertions.assertion3 [definition, in Hoare]
ExAssertions.assertion4 [definition, in Hoare]
E_Plus [constructor, in Smallstep]
E_Const [constructor, in Smallstep]
E_Some [constructor, in PE]
E_None [constructor, in PE]
F
factorial_correct [lemma, in Hoare2]factorial_dec [definition, in Hoare2]
false_eqb_string [lemma, in Norm]
false_eqb_string [lemma, in PE]
fib [definition, in Hoare2]
fib_eqn [lemma, in Hoare2]
FILL_IN_HERE [definition, in Smallstep]
FILL_IN_HERE [definition, in Hoare2]
FirstTry [module, in Typechecking]
FirstTry.type_check [definition, in Typechecking]
fold_constants_com_sound [lemma, in Equiv]
fold_constants_bexp_sound [lemma, in Equiv]
fold_constants_aexp_sound [lemma, in Equiv]
fold_com_ex1 [definition, in Equiv]
fold_constants_com [definition, in Equiv]
fold_bexp_ex2 [definition, in Equiv]
fold_bexp_ex1 [definition, in Equiv]
fold_constants_bexp [definition, in Equiv]
fold_aexp_ex2 [definition, in Equiv]
fold_aexp_ex1 [definition, in Equiv]
fold_constants_aexp [definition, in Equiv]
free_in_context [lemma, in Norm]
FuncEq [section, in LibTactics]
FuncEq.A1 [variable, in LibTactics]
FuncEq.A2 [variable, in LibTactics]
FuncEq.A3 [variable, in LibTactics]
FuncEq.A4 [variable, in LibTactics]
FuncEq.A5 [variable, in LibTactics]
FuncEq.A6 [variable, in LibTactics]
FuncEq.A7 [variable, in LibTactics]
FuncEq.B [variable, in LibTactics]
G
GenExample [module, in UseTactics]GenExample.substitution_preserves_typing [lemma, in UseTactics]
Goto [constructor, in PE]
gt_not_le [axiom, in UseAuto]
H
halts [definition, in Norm]has_type_sind [definition, in Norm]
has_type_ind [definition, in Norm]
has_type [inductive, in Norm]
Himp [module, in Hoare]
Himp [module, in Equiv]
Himp.CAsgn [constructor, in Hoare]
Himp.CAsgn [constructor, in Equiv]
Himp.cequiv [definition, in Equiv]
Himp.ceval [inductive, in Hoare]
Himp.ceval [inductive, in Equiv]
Himp.ceval_sind [definition, in Hoare]
Himp.ceval_ind [definition, in Hoare]
Himp.ceval_sind [definition, in Equiv]
Himp.ceval_ind [definition, in Equiv]
Himp.CHavoc [constructor, in Hoare]
Himp.CHavoc [constructor, in Equiv]
Himp.CIf [constructor, in Hoare]
Himp.CIf [constructor, in Equiv]
Himp.com [inductive, in Hoare]
Himp.com [inductive, in Equiv]
Himp.com_sind [definition, in Hoare]
Himp.com_rec [definition, in Hoare]
Himp.com_ind [definition, in Hoare]
Himp.com_rect [definition, in Hoare]
Himp.com_sind [definition, in Equiv]
Himp.com_rec [definition, in Equiv]
Himp.com_ind [definition, in Equiv]
Himp.com_rect [definition, in Equiv]
Himp.CSeq [constructor, in Hoare]
Himp.CSeq [constructor, in Equiv]
Himp.CSkip [constructor, in Hoare]
Himp.CSkip [constructor, in Equiv]
Himp.CWhile [constructor, in Hoare]
Himp.CWhile [constructor, in Equiv]
Himp.E_Havoc [constructor, in Hoare]
Himp.E_WhileTrue [constructor, in Hoare]
Himp.E_WhileFalse [constructor, in Hoare]
Himp.E_IfFalse [constructor, in Hoare]
Himp.E_IfTrue [constructor, in Hoare]
Himp.E_Seq [constructor, in Hoare]
Himp.E_Asgn [constructor, in Hoare]
Himp.E_Skip [constructor, in Hoare]
Himp.E_WhileTrue [constructor, in Equiv]
Himp.E_WhileFalse [constructor, in Equiv]
Himp.E_IfFalse [constructor, in Equiv]
Himp.E_IfTrue [constructor, in Equiv]
Himp.E_Seq [constructor, in Equiv]
Himp.E_Asgn [constructor, in Equiv]
Himp.E_Skip [constructor, in Equiv]
Himp.havoc_post [lemma, in Hoare]
Himp.havoc_pre [definition, in Hoare]
Himp.havoc_example2 [definition, in Equiv]
Himp.havoc_example1 [definition, in Equiv]
Himp.hoare_havoc [lemma, in Hoare]
Himp.hoare_consequence_pre [lemma, in Hoare]
Himp.manual_grade_for_Check_rule_for_HAVOC [definition, in Equiv]
Himp.pcopy [definition, in Equiv]
Himp.ptwice [definition, in Equiv]
Himp.ptwice_cequiv_pcopy [lemma, in Equiv]
Himp.pXY [definition, in Equiv]
Himp.pXY_cequiv_pYX [lemma, in Equiv]
Himp.pYX [definition, in Equiv]
Himp.p1 [definition, in Equiv]
Himp.p1_p2_equiv [lemma, in Equiv]
Himp.p1_may_diverge [lemma, in Equiv]
Himp.p2 [definition, in Equiv]
Himp.p2_may_diverge [lemma, in Equiv]
Himp.p3 [definition, in Equiv]
Himp.p3_p4_inequiv [lemma, in Equiv]
Himp.p4 [definition, in Equiv]
Himp.p5 [definition, in Equiv]
Himp.p5_p6_equiv [lemma, in Equiv]
Himp.p6 [definition, in Equiv]
Himp.valid_hoare_triple [definition, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:_ ; _ [notation, in Equiv]
com:_ := _ [notation, in Equiv]
com:havoc _ [notation, in Hoare]
com:havoc _ [notation, in Equiv]
com:if _ then _ else _ end [notation, in Hoare]
com:if _ then _ else _ end [notation, in Equiv]
com:skip [notation, in Hoare]
com:skip [notation, in Equiv]
com:while _ do _ end [notation, in Hoare]
com:while _ do _ end [notation, in Equiv]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Equiv]
Himp2 [module, in Hoare2]
Himp2.hoare_havoc_weakest [lemma, in Hoare2]
HintsTransitivity [section, in UseAuto]
Hoare [library]
HoareAsLogic [library]
HoareAssertAssume [module, in Hoare]
HoareAssertAssume.assert_assume_example [definition, in Hoare]
HoareAssertAssume.assert_implies_assume [lemma, in Hoare]
HoareAssertAssume.assert_assume_differ [lemma, in Hoare]
HoareAssertAssume.CAsgn [constructor, in Hoare]
HoareAssertAssume.CAssert [constructor, in Hoare]
HoareAssertAssume.CAssume [constructor, in Hoare]
HoareAssertAssume.ceval [inductive, in Hoare]
HoareAssertAssume.ceval_sind [definition, in Hoare]
HoareAssertAssume.ceval_ind [definition, in Hoare]
HoareAssertAssume.CIf [constructor, in Hoare]
HoareAssertAssume.com [inductive, in Hoare]
HoareAssertAssume.com_sind [definition, in Hoare]
HoareAssertAssume.com_rec [definition, in Hoare]
HoareAssertAssume.com_ind [definition, in Hoare]
HoareAssertAssume.com_rect [definition, in Hoare]
HoareAssertAssume.CSeq [constructor, in Hoare]
HoareAssertAssume.CSkip [constructor, in Hoare]
HoareAssertAssume.CWhile [constructor, in Hoare]
HoareAssertAssume.E_Assume [constructor, in Hoare]
HoareAssertAssume.E_AssertFalse [constructor, in Hoare]
HoareAssertAssume.E_AssertTrue [constructor, in Hoare]
HoareAssertAssume.E_WhileTrueError [constructor, in Hoare]
HoareAssertAssume.E_WhileTrueNormal [constructor, in Hoare]
HoareAssertAssume.E_WhileFalse [constructor, in Hoare]
HoareAssertAssume.E_IfFalse [constructor, in Hoare]
HoareAssertAssume.E_IfTrue [constructor, in Hoare]
HoareAssertAssume.E_SeqError [constructor, in Hoare]
HoareAssertAssume.E_SeqNormal [constructor, in Hoare]
HoareAssertAssume.E_Asgn [constructor, in Hoare]
HoareAssertAssume.E_Skip [constructor, in Hoare]
HoareAssertAssume.hoare_while [lemma, in Hoare]
HoareAssertAssume.hoare_if [lemma, in Hoare]
HoareAssertAssume.hoare_skip [lemma, in Hoare]
HoareAssertAssume.hoare_seq [lemma, in Hoare]
HoareAssertAssume.hoare_consequence_post [lemma, in Hoare]
HoareAssertAssume.hoare_consequence_pre [lemma, in Hoare]
HoareAssertAssume.hoare_asgn [lemma, in Hoare]
HoareAssertAssume.RError [constructor, in Hoare]
HoareAssertAssume.result [inductive, in Hoare]
HoareAssertAssume.result_sind [definition, in Hoare]
HoareAssertAssume.result_rec [definition, in Hoare]
HoareAssertAssume.result_ind [definition, in Hoare]
HoareAssertAssume.result_rect [definition, in Hoare]
HoareAssertAssume.RNormal [constructor, in Hoare]
HoareAssertAssume.valid_hoare_triple [definition, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:assert _ [notation, in Hoare]
com:assume _ [notation, in Hoare]
com:if _ then _ else _ end [notation, in Hoare]
com:skip [notation, in Hoare]
com:while _ do _ end [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
hoare_while [lemma, in Hoare]
hoare_if [lemma, in Hoare]
hoare_asgn_example4 [definition, in Hoare]
hoare_asgn_example3 [definition, in Hoare]
hoare_asgn_example1''' [definition, in Hoare]
hoare_asgn_example1'' [definition, in Hoare]
hoare_asgn_example1' [definition, in Hoare]
hoare_consequence_post' [lemma, in Hoare]
hoare_consequence_pre'''' [lemma, in Hoare]
hoare_consequence_pre''' [lemma, in Hoare]
hoare_consequence_pre'' [lemma, in Hoare]
hoare_consequence_pre' [lemma, in Hoare]
hoare_consequence [lemma, in Hoare]
hoare_asgn_example1 [definition, in Hoare]
hoare_consequence_post [lemma, in Hoare]
hoare_consequence_pre [lemma, in Hoare]
hoare_asgn_fwd_exists [lemma, in Hoare]
hoare_asgn_fwd [lemma, in Hoare]
hoare_asgn_wrong [lemma, in Hoare]
hoare_asgn_examples2 [definition, in Hoare]
hoare_asgn_examples1 [definition, in Hoare]
hoare_asgn [lemma, in Hoare]
hoare_seq [lemma, in Hoare]
hoare_skip [lemma, in Hoare]
hoare_pre_false [lemma, in Hoare]
hoare_post_true [lemma, in Hoare]
hoare_asgn_weakest [lemma, in Hoare2]
hoare_complete [lemma, in HoareAsLogic]
hoare_sound [lemma, in HoareAsLogic]
Hoare2 [library]
H_Consequence_post [lemma, in HoareAsLogic]
H_Consequence_pre [lemma, in HoareAsLogic]
H_Consequence [constructor, in HoareAsLogic]
H_While [constructor, in HoareAsLogic]
H_If [constructor, in HoareAsLogic]
H_Seq [constructor, in HoareAsLogic]
H_Asgn [constructor, in HoareAsLogic]
H_Skip [constructor, in HoareAsLogic]
I
identity_assignment [lemma, in Equiv]If [constructor, in PE]
iff_intro_swap [lemma, in LibTactics]
if_minus_plus [lemma, in Hoare]
if_example''' [definition, in Hoare]
if_example'' [definition, in Hoare]
if_example [definition, in Hoare]
if_minus_plus_correct [lemma, in Hoare2]
if_minus_plus_dec [definition, in Hoare2]
if_false [lemma, in Equiv]
if_true [lemma, in Equiv]
if_true_simple [lemma, in Equiv]
If1 [module, in Hoare]
If1.CAsgn [constructor, in Hoare]
If1.ceval [inductive, in Hoare]
If1.ceval_sind [definition, in Hoare]
If1.ceval_ind [definition, in Hoare]
If1.CIf [constructor, in Hoare]
If1.CIf1 [constructor, in Hoare]
If1.com [inductive, in Hoare]
If1.com_sind [definition, in Hoare]
If1.com_rec [definition, in Hoare]
If1.com_ind [definition, in Hoare]
If1.com_rect [definition, in Hoare]
If1.CSeq [constructor, in Hoare]
If1.CSkip [constructor, in Hoare]
If1.CWhile [constructor, in Hoare]
If1.E_WhileTrue [constructor, in Hoare]
If1.E_WhileFalse [constructor, in Hoare]
If1.E_IfFalse [constructor, in Hoare]
If1.E_IfTrue [constructor, in Hoare]
If1.E_Seq [constructor, in Hoare]
If1.E_Asgn [constructor, in Hoare]
If1.E_Skip [constructor, in Hoare]
If1.hoare_if1_good [lemma, in Hoare]
If1.hoare_asgn [lemma, in Hoare]
If1.hoare_consequence_pre [lemma, in Hoare]
If1.if1false_test [definition, in Hoare]
If1.if1true_test [definition, in Hoare]
If1.manual_grade_for_hoare_if1 [definition, in Hoare]
If1.valid_hoare_triple [definition, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:if _ then _ else _ end [notation, in Hoare]
com:if1 _ then _ end [notation, in Hoare]
com:skip [notation, in Hoare]
com:while _ do _ end [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
inb [definition, in PE]
inbP [lemma, in PE]
induct_height_max2 [lemma, in LibTactics]
inequiv_exercise [lemma, in Equiv]
inj_pair2 [axiom, in LibTactics]
instantiation [inductive, in Norm]
instantiation_drop [lemma, in Norm]
instantiation_R [lemma, in Norm]
instantiation_env_closed [lemma, in Norm]
instantiation_domains_match [lemma, in Norm]
instantiation_sind [definition, in Norm]
instantiation_ind [definition, in Norm]
IntrovExamples [module, in UseTactics]
IntrovExamples.ceval_deterministic' [lemma, in UseTactics]
IntrovExamples.ceval_deterministic [lemma, in UseTactics]
IntrovExamples.dist_exists_or [lemma, in UseTactics]
IntrovExamples.exists_impl [lemma, in UseTactics]
invalid_triple [lemma, in Hoare]
InvertsExamples [module, in UseTactics]
InvertsExamples.ceval_deterministic' [lemma, in UseTactics]
InvertsExamples.ceval_deterministic [lemma, in UseTactics]
InvertsExamples.skip_left' [lemma, in UseTactics]
InvertsExamples.skip_left [lemma, in UseTactics]
InvertsExamples1 [module, in UseTactics]
InvertsExamples1.typing_nonexample_1 [definition, in UseTactics]
is_wp_example [lemma, in Hoare2]
is_wp [definition, in Hoare2]
K
keval [definition, in PE]keval_example [definition, in PE]
L
le_gt_false [axiom, in UseAuto]le_not_gt [axiom, in UseAuto]
lia_demo_4 [lemma, in UseAuto]
lia_demo_3 [lemma, in UseAuto]
lia_demo_2 [lemma, in UseAuto]
lia_demo_1 [lemma, in UseAuto]
LibTactics [library]
LibTacticsCompatibility [module, in LibTactics]
lookup [definition, in Norm]
loop [constructor, in PE]
Loop [module, in PE]
loop_unrolling [lemma, in Equiv]
Loop.ceval_count_sound [lemma, in PE]
Loop.ceval_count_complete [lemma, in PE]
Loop.ceval_count_sind [definition, in PE]
Loop.ceval_count_ind [definition, in PE]
Loop.ceval_count [inductive, in PE]
Loop.E'Asgn [constructor, in PE]
Loop.E'IfFalse [constructor, in PE]
Loop.E'IfTrue [constructor, in PE]
Loop.E'Seq [constructor, in PE]
Loop.E'Skip [constructor, in PE]
Loop.E'WhileFalse [constructor, in PE]
Loop.E'WhileTrue [constructor, in PE]
Loop.pe_com_correct [lemma, in PE]
Loop.pe_com_sound [lemma, in PE]
Loop.pe_com_complete [lemma, in PE]
Loop.pe_ceval_count_le [lemma, in PE]
Loop.pe_ceval_count_sind [definition, in PE]
Loop.pe_ceval_count_ind [definition, in PE]
Loop.pe_ceval_count_intro [constructor, in PE]
Loop.pe_ceval_count [inductive, in PE]
Loop.pe_compare_nil_update [lemma, in PE]
Loop.pe_compare_nil_lookup [lemma, in PE]
Loop.pe_loop_example4 [definition, in PE]
Loop.pe_loop_example3 [definition, in PE]
Loop.pe_loop_example2 [definition, in PE]
Loop.pe_loop_example1 [definition, in PE]
Loop.pe_com_sind [definition, in PE]
Loop.pe_com_ind [definition, in PE]
Loop.PE_WhileFixed [constructor, in PE]
Loop.PE_WhileFixedLoop [constructor, in PE]
Loop.PE_WhileFixedEnd [constructor, in PE]
Loop.PE_While [constructor, in PE]
Loop.PE_WhileTrue [constructor, in PE]
Loop.PE_WhileFalse [constructor, in PE]
Loop.PE_If [constructor, in PE]
Loop.PE_IfFalse [constructor, in PE]
Loop.PE_IfTrue [constructor, in PE]
Loop.PE_Seq [constructor, in PE]
Loop.PE_AsgnDynamic [constructor, in PE]
Loop.PE_AsgnStatic [constructor, in PE]
Loop.PE_Skip [constructor, in PE]
Loop.pe_com [inductive, in PE]
Loop.square_loop [definition, in PE]
_ / _ / _ / _ ==> _ # _ [notation, in PE]
_ / _ ==> _ # _ [notation, in PE]
_ / _ ==> _ / _ / _ [notation, in PE]
ltac_goal_to_discard_sind [definition, in LibTactics]
ltac_goal_to_discard_rec [definition, in LibTactics]
ltac_goal_to_discard_ind [definition, in LibTactics]
ltac_goal_to_discard_rect [definition, in LibTactics]
ltac_goal_to_discard_intro [constructor, in LibTactics]
ltac_goal_to_discard [inductive, in LibTactics]
ltac_something_show [lemma, in LibTactics]
ltac_something_hide [lemma, in LibTactics]
ltac_something_eq [lemma, in LibTactics]
ltac_something [definition, in LibTactics]
ltac_to_generalize [definition, in LibTactics]
ltac_tag_subst [definition, in LibTactics]
ltac_int_to_nat [definition, in LibTactics]
ltac_database_provide [lemma, in LibTactics]
ltac_database [definition, in LibTactics]
Ltac_database_token_sind [definition, in LibTactics]
Ltac_database_token_rec [definition, in LibTactics]
Ltac_database_token_ind [definition, in LibTactics]
Ltac_database_token_rect [definition, in LibTactics]
ltac_database_token [constructor, in LibTactics]
Ltac_database_token [inductive, in LibTactics]
ltac_Mark_sind [definition, in LibTactics]
ltac_Mark_rec [definition, in LibTactics]
ltac_Mark_ind [definition, in LibTactics]
ltac_Mark_rect [definition, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_Wilds_sind [definition, in LibTactics]
ltac_Wilds_rec [definition, in LibTactics]
ltac_Wilds_ind [definition, in LibTactics]
ltac_Wilds_rect [definition, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
ltac_Wild_sind [definition, in LibTactics]
ltac_Wild_rec [definition, in LibTactics]
ltac_Wild_ind [definition, in LibTactics]
ltac_Wild_rect [definition, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_No_arg_sind [definition, in LibTactics]
ltac_No_arg_rec [definition, in LibTactics]
ltac_No_arg_ind [definition, in LibTactics]
ltac_No_arg_rect [definition, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
M
manual_grade_for_eval__multistep_inf [definition, in Smallstep]manual_grade_for_hoare_repeat [definition, in Hoare]
manual_grade_for_not_congr [definition, in Equiv]
manual_grade_for_equiv_classes [definition, in Equiv]
manual_grade_for_norm [definition, in Norm]
manual_grade_for_norm_fail [definition, in Norm]
manual_grade_for_pair_permutation [definition, in Sub]
manual_grade_for_smallest_2 [definition, in Sub]
manual_grade_for_smallest_1 [definition, in Sub]
manual_grade_for_small_large_4 [definition, in Sub]
manual_grade_for_small_large_2 [definition, in Sub]
manual_grade_for_small_large_1 [definition, in Sub]
manual_grade_for_proper_subtypes [definition, in Sub]
manual_grade_for_subtype_concepts_tf [definition, in Sub]
manual_grade_for_subtype_instances_tf_2 [definition, in Sub]
manual_grade_for_subtype_order [definition, in Sub]
manual_grade_for_arrow_sub_wrong [definition, in Sub]
minimum_correct [lemma, in Hoare2]
minimum_dec [definition, in Hoare2]
MoreStlc [library]
msubst [definition, in Norm]
msubst_R [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_abs [lemma, in Norm]
msubst_var [lemma, in Norm]
msubst_closed [lemma, in Norm]
multi [inductive, in Smallstep]
multistep [abbreviation, in Norm]
multistep__eval [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_congr_1 [lemma, in Smallstep]
multistep_App2 [lemma, in Norm]
multistep_preserves_R' [lemma, in Norm]
multistep_preserves_R [lemma, in Norm]
multi_trans [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_sind [definition, in Smallstep]
multi_ind [definition, in Smallstep]
multi_step [constructor, in Smallstep]
multi_refl [constructor, in Smallstep]
mupdate [definition, in Norm]
mupdate_drop [lemma, in Norm]
mupdate_lookup [lemma, in Norm]
myFact [definition, in UseAuto]
N
NaryExamples [module, in UseTactics]NaryExamples.demo_branch [lemma, in UseTactics]
NaryExamples.demo_splits [lemma, in UseTactics]
nat_le_refl [lemma, in UseAuto]
negation_study_2 [lemma, in UseAuto]
negation_study_1 [lemma, in UseAuto]
nf_same_as_value [lemma, in Smallstep]
nf_is_value [lemma, in Smallstep]
Norm [library]
normalization [lemma, in Norm]
normalize_ex' [lemma, in Smallstep]
normalize_ex [lemma, in Smallstep]
normalizing [definition, in Smallstep]
normal_forms_unique [lemma, in Smallstep]
normal_form_of [definition, in Smallstep]
normal_form [definition, in Smallstep]
O
optimizer [definition, in Equiv]optimizer_sound [lemma, in Equiv]
optimize_0plus_com_sound [lemma, in Equiv]
optimize_0plus_bexp_sound [lemma, in Equiv]
optimize_0plus_aexp_sound [lemma, in Equiv]
optimize_0plus_com [definition, in Equiv]
optimize_0plus_bexp [definition, in Equiv]
optimize_0plus_aexp [definition, in Equiv]
order_matters_2 [lemma, in UseAuto]
order_matters_1 [lemma, in UseAuto]
outer_triple_valid [definition, in Hoare2]
P
P [constructor, in Smallstep]P [axiom, in UseAuto]
parity [definition, in Hoare2]
parity [definition, in PE]
parity_outer_triple_valid [lemma, in Hoare2]
parity_lt_2 [lemma, in Hoare2]
parity_ge_2 [lemma, in Hoare2]
parity_dec [definition, in Hoare2]
parity_eval [definition, in PE]
parity_body [definition, in PE]
parity_label_sind [definition, in PE]
parity_label_rec [definition, in PE]
parity_label_ind [definition, in PE]
parity_label_rect [definition, in PE]
parity_label [inductive, in PE]
PE [library]
peval [inductive, in PE]
peval_sind [definition, in PE]
peval_ind [definition, in PE]
pe_program_correct [lemma, in PE]
pe_peval_sind [definition, in PE]
pe_peval_ind [definition, in PE]
pe_peval_intro [constructor, in PE]
pe_peval [inductive, in PE]
pe_program [definition, in PE]
pe_block_correct [lemma, in PE]
pe_block_example [definition, in PE]
pe_block [definition, in PE]
pe_com_correct [lemma, in PE]
pe_com_sound [lemma, in PE]
pe_com_complete [lemma, in PE]
pe_ceval_sind [definition, in PE]
pe_ceval_ind [definition, in PE]
pe_ceval_intro [constructor, in PE]
pe_ceval [inductive, in PE]
pe_example3 [definition, in PE]
pe_example2 [definition, in PE]
pe_example1 [definition, in PE]
pe_com_sind [definition, in PE]
pe_com_ind [definition, in PE]
PE_If [constructor, in PE]
PE_IfFalse [constructor, in PE]
PE_IfTrue [constructor, in PE]
PE_Seq [constructor, in PE]
PE_AsgnDynamic [constructor, in PE]
PE_AsgnStatic [constructor, in PE]
PE_Skip [constructor, in PE]
pe_com [inductive, in PE]
pe_compare_update [lemma, in PE]
pe_compare_removes [lemma, in PE]
pe_removes_correct [lemma, in PE]
pe_removes [definition, in PE]
pe_compare_correct [lemma, in PE]
pe_compare [definition, in PE]
pe_unique_correct [lemma, in PE]
pe_unique [definition, in PE]
pe_disagree_domain [lemma, in PE]
pe_disagree_at [definition, in PE]
pe_update_update_add [lemma, in PE]
pe_update_update_remove [lemma, in PE]
pe_add_correct [lemma, in PE]
pe_add [definition, in PE]
pe_remove_correct [lemma, in PE]
pe_remove [definition, in PE]
pe_bexp_correct [lemma, in PE]
pe_bexp [definition, in PE]
pe_aexp_correct [lemma, in PE]
pe_consistent_update [lemma, in PE]
pe_update_consistent [lemma, in PE]
pe_update_correct [lemma, in PE]
pe_update [definition, in PE]
pe_aexp_correct_weak [lemma, in PE]
pe_consistent [definition, in PE]
pe_aexp [definition, in PE]
pe_domain [lemma, in PE]
pe_lookup [definition, in PE]
pe_state [definition, in PE]
positive_difference_correct [lemma, in Hoare2]
positive_difference_dec [definition, in Hoare2]
post [definition, in Hoare2]
postcondition_from_while [definition, in Hoare2]
postcondition_from [definition, in Hoare2]
Postscript [library]
pow2 [definition, in Hoare2]
pow2_le_1 [lemma, in Hoare2]
pow2_plus_1 [lemma, in Hoare2]
precondition_from_while [definition, in Hoare2]
precondition_from [definition, in Hoare2]
Preface [library]
preservation [lemma, in Norm]
PreservationProgressReferences [module, in UseAuto]
PreservationProgressReferences.nth_eq_last' [lemma, in UseAuto]
PreservationProgressReferences.preservation [lemma, in UseAuto]
PreservationProgressReferences.preservation_ref [lemma, in UseAuto]
PreservationProgressReferences.preservation' [lemma, in UseAuto]
PreservationProgressReferences.progress [lemma, in UseAuto]
PreservationProgressStlc [module, in UseAuto]
PreservationProgressStlc.preservation [lemma, in UseAuto]
PreservationProgressStlc.preservation' [lemma, in UseAuto]
PreservationProgressStlc.progress [lemma, in UseAuto]
PreservationProgressStlc.progress' [lemma, in UseAuto]
prog [definition, in Smallstep]
program [definition, in PE]
prog_i [definition, in Equiv]
prog_h [definition, in Equiv]
prog_g [definition, in Equiv]
prog_f [definition, in Equiv]
prog_e [definition, in Equiv]
prog_d [definition, in Equiv]
prog_c [definition, in Equiv]
prog_b [definition, in Equiv]
prog_a [definition, in Equiv]
provable_false_pre [lemma, in HoareAsLogic]
provable_true_post [lemma, in HoareAsLogic]
R
R [definition, in Norm]Records [library]
RecordSub [module, in RecordSub]
RecordSub [library]
RecordSub.abs_arrow [lemma, in RecordSub]
RecordSub.canonical_forms_of_arrow_types [lemma, in RecordSub]
RecordSub.context [definition, in RecordSub]
RecordSub.Examples [module, in RecordSub]
RecordSub.Examples.A [abbreviation, in RecordSub]
RecordSub.Examples.B [abbreviation, in RecordSub]
RecordSub.Examples.C [abbreviation, in RecordSub]
RecordSub.Examples.i [abbreviation, in RecordSub]
RecordSub.Examples.j [abbreviation, in RecordSub]
RecordSub.Examples.k [abbreviation, in RecordSub]
RecordSub.Examples.subtyping_example_4 [definition, in RecordSub]
RecordSub.Examples.subtyping_example_3 [definition, in RecordSub]
RecordSub.Examples.subtyping_example_2 [definition, in RecordSub]
RecordSub.Examples.subtyping_example_1 [definition, in RecordSub]
RecordSub.Examples.subtyping_example_0 [definition, in RecordSub]
RecordSub.Examples.TRcd_kj [definition, in RecordSub]
RecordSub.Examples.TRcd_j [definition, in RecordSub]
RecordSub.Examples.x [abbreviation, in RecordSub]
RecordSub.Examples.y [abbreviation, in RecordSub]
RecordSub.Examples.z [abbreviation, in RecordSub]
RecordSub.Examples2 [module, in RecordSub]
RecordSub.Examples2.trcd_kj [definition, in RecordSub]
RecordSub.Examples2.typing_example_2 [definition, in RecordSub]
RecordSub.Examples2.typing_example_1 [definition, in RecordSub]
RecordSub.Examples2.typing_example_0 [definition, in RecordSub]
RecordSub.has_type__wf [lemma, in RecordSub]
RecordSub.has_type_sind [definition, in RecordSub]
RecordSub.has_type_ind [definition, in RecordSub]
RecordSub.has_type [inductive, in RecordSub]
RecordSub.lookup_field_in_value [lemma, in RecordSub]
RecordSub.manual_grade_for_rcd_types_match_informal [definition, in RecordSub]
RecordSub.preservation [lemma, in RecordSub]
RecordSub.progress [lemma, in RecordSub]
RecordSub.rcd_types_match [lemma, in RecordSub]
RecordSub.record_tm_sind [definition, in RecordSub]
RecordSub.record_tm_ind [definition, in RecordSub]
RecordSub.record_tm [inductive, in RecordSub]
RecordSub.record_ty_sind [definition, in RecordSub]
RecordSub.record_ty_ind [definition, in RecordSub]
RecordSub.record_ty [inductive, in RecordSub]
RecordSub.rtcons [constructor, in RecordSub]
RecordSub.RTcons [constructor, in RecordSub]
RecordSub.rtnil [constructor, in RecordSub]
RecordSub.RTnil [constructor, in RecordSub]
RecordSub.step [inductive, in RecordSub]
RecordSub.step_preserves_record_tm [lemma, in RecordSub]
RecordSub.step_sind [definition, in RecordSub]
RecordSub.step_ind [definition, in RecordSub]
RecordSub.ST_Rcd_Tail [constructor, in RecordSub]
RecordSub.ST_Rcd_Head [constructor, in RecordSub]
RecordSub.ST_ProjRcd [constructor, in RecordSub]
RecordSub.ST_Proj1 [constructor, in RecordSub]
RecordSub.ST_App2 [constructor, in RecordSub]
RecordSub.ST_App1 [constructor, in RecordSub]
RecordSub.ST_AppAbs [constructor, in RecordSub]
RecordSub.subst [definition, in RecordSub]
RecordSub.substitution_preserves_typing [lemma, in RecordSub]
RecordSub.subtype [inductive, in RecordSub]
RecordSub.subtype__wf [lemma, in RecordSub]
RecordSub.subtype_sind [definition, in RecordSub]
RecordSub.subtype_ind [definition, in RecordSub]
RecordSub.sub_inversion_arrow [lemma, in RecordSub]
RecordSub.S_RcdPerm [constructor, in RecordSub]
RecordSub.S_RcdDepth [constructor, in RecordSub]
RecordSub.S_RcdWidth [constructor, in RecordSub]
RecordSub.S_Arrow [constructor, in RecordSub]
RecordSub.S_Top [constructor, in RecordSub]
RecordSub.S_Trans [constructor, in RecordSub]
RecordSub.S_Refl [constructor, in RecordSub]
RecordSub.tlookup [definition, in RecordSub]
RecordSub.Tlookup [definition, in RecordSub]
RecordSub.tm [inductive, in RecordSub]
RecordSub.tm_sind [definition, in RecordSub]
RecordSub.tm_rec [definition, in RecordSub]
RecordSub.tm_ind [definition, in RecordSub]
RecordSub.tm_rect [definition, in RecordSub]
RecordSub.tm_rcons [constructor, in RecordSub]
RecordSub.tm_rnil [constructor, in RecordSub]
RecordSub.tm_rproj [constructor, in RecordSub]
RecordSub.tm_abs [constructor, in RecordSub]
RecordSub.tm_app [constructor, in RecordSub]
RecordSub.tm_var [constructor, in RecordSub]
RecordSub.ty [inductive, in RecordSub]
RecordSub.typing_inversion_abs [lemma, in RecordSub]
RecordSub.ty_sind [definition, in RecordSub]
RecordSub.ty_rec [definition, in RecordSub]
RecordSub.ty_ind [definition, in RecordSub]
RecordSub.ty_rect [definition, in RecordSub]
RecordSub.Ty_RCons [constructor, in RecordSub]
RecordSub.Ty_RNil [constructor, in RecordSub]
RecordSub.Ty_Arrow [constructor, in RecordSub]
RecordSub.Ty_Base [constructor, in RecordSub]
RecordSub.Ty_Top [constructor, in RecordSub]
RecordSub.T_RCons [constructor, in RecordSub]
RecordSub.T_RNil [constructor, in RecordSub]
RecordSub.T_Sub [constructor, in RecordSub]
RecordSub.T_Proj [constructor, in RecordSub]
RecordSub.T_App [constructor, in RecordSub]
RecordSub.T_Abs [constructor, in RecordSub]
RecordSub.T_Var [constructor, in RecordSub]
RecordSub.value [inductive, in RecordSub]
RecordSub.value_sind [definition, in RecordSub]
RecordSub.value_ind [definition, in RecordSub]
RecordSub.v_rcons [constructor, in RecordSub]
RecordSub.v_rnil [constructor, in RecordSub]
RecordSub.v_abs [constructor, in RecordSub]
RecordSub.weakening [lemma, in RecordSub]
RecordSub.weakening_empty [lemma, in RecordSub]
RecordSub.well_formed_ty_sind [definition, in RecordSub]
RecordSub.well_formed_ty_ind [definition, in RecordSub]
RecordSub.well_formed_ty [inductive, in RecordSub]
RecordSub.wfArrow [constructor, in RecordSub]
RecordSub.wfBase [constructor, in RecordSub]
RecordSub.wfRCons [constructor, in RecordSub]
RecordSub.wfRNil [constructor, in RecordSub]
RecordSub.wfTop [constructor, in RecordSub]
RecordSub.wf_rcd_lookup [lemma, in RecordSub]
stlc_ty:Top [notation, in RecordSub]
stlc_ty:nil [notation, in RecordSub]
stlc_ty:_ : _ :: _ [notation, in RecordSub]
stlc_ty:Base _ [notation, in RecordSub]
stlc_ty:_ -> _ [notation, in RecordSub]
stlc_ty:_ [notation, in RecordSub]
stlc_ty:( _ ) [notation, in RecordSub]
stlc:_ [notation, in RecordSub]
stlc:_ --> _ [notation, in RecordSub]
stlc:_ := _ :: _ [notation, in RecordSub]
stlc:_ _ [notation, in RecordSub]
stlc:nil [notation, in RecordSub]
stlc:( _ ) [notation, in RecordSub]
stlc:[ _ := _ ] _ [notation, in RecordSub]
stlc:\ _ : _ , _ [notation, in RecordSub]
stlc:{ _ } [notation, in RecordSub]
_ |-- _ ∈ _ [notation, in RecordSub]
_ <: _ [notation, in RecordSub]
_ --> _ [notation, in RecordSub]
<{ _ }> [notation, in RecordSub]
<{{ _ }}> [notation, in RecordSub]
reduce_to_zero_correct''' [lemma, in Hoare2]
reduce_to_zero_correct' [lemma, in Hoare2]
reduce_to_zero [definition, in Hoare2]
References [library]
refines [definition, in Equiv]
refl_cequiv [lemma, in Equiv]
refl_bequiv [lemma, in Equiv]
refl_aequiv [lemma, in Equiv]
relation [definition, in Smallstep]
RepeatExercise [module, in Hoare]
RepeatExercise.CAsgn [constructor, in Hoare]
RepeatExercise.ceval [inductive, in Hoare]
RepeatExercise.ceval_sind [definition, in Hoare]
RepeatExercise.ceval_ind [definition, in Hoare]
RepeatExercise.CIf [constructor, in Hoare]
RepeatExercise.com [inductive, in Hoare]
RepeatExercise.com_sind [definition, in Hoare]
RepeatExercise.com_rec [definition, in Hoare]
RepeatExercise.com_ind [definition, in Hoare]
RepeatExercise.com_rect [definition, in Hoare]
RepeatExercise.CRepeat [constructor, in Hoare]
RepeatExercise.CSeq [constructor, in Hoare]
RepeatExercise.CSkip [constructor, in Hoare]
RepeatExercise.CWhile [constructor, in Hoare]
RepeatExercise.ex1_repeat_works [lemma, in Hoare]
RepeatExercise.ex1_repeat [definition, in Hoare]
RepeatExercise.E_WhileTrue [constructor, in Hoare]
RepeatExercise.E_WhileFalse [constructor, in Hoare]
RepeatExercise.E_IfFalse [constructor, in Hoare]
RepeatExercise.E_IfTrue [constructor, in Hoare]
RepeatExercise.E_Seq [constructor, in Hoare]
RepeatExercise.E_Asgn [constructor, in Hoare]
RepeatExercise.E_Skip [constructor, in Hoare]
RepeatExercise.valid_hoare_triple [definition, in Hoare]
com:_ ; _ [notation, in Hoare]
com:_ := _ [notation, in Hoare]
com:if _ then _ else _ end [notation, in Hoare]
com:repeat _ until _ end [notation, in Hoare]
com:skip [notation, in Hoare]
com:while _ do _ end [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ =[ _ ]=> _ [notation, in Hoare]
RingDemo [module, in UseAuto]
RingDemo.ring_demo [lemma, in UseAuto]
rm [definition, in LibTactics]
R_typable_empty [lemma, in Norm]
R_halts [lemma, in Norm]
S
sample_proof [definition, in HoareAsLogic]search_depth_5 [lemma, in UseAuto]
search_depth_4 [lemma, in UseAuto]
search_depth_3 [lemma, in UseAuto]
search_depth_1 [lemma, in UseAuto]
search_depth_0 [lemma, in UseAuto]
Semantics [module, in UseAuto]
Semantics.multistep__eval'' [lemma, in UseAuto]
Semantics.multistep__eval' [lemma, in UseAuto]
Semantics.multistep_eval_ind [lemma, in UseAuto]
Semantics.multistep__eval [lemma, in UseAuto]
seq_assoc [lemma, in Equiv]
SimpleArith1 [module, in Smallstep]
SimpleArith1.step [inductive, in Smallstep]
SimpleArith1.step_sind [definition, in Smallstep]
SimpleArith1.step_ind [definition, in Smallstep]
SimpleArith1.ST_Plus2 [constructor, in Smallstep]
SimpleArith1.ST_Plus1 [constructor, in Smallstep]
SimpleArith1.ST_PlusConstConst [constructor, in Smallstep]
SimpleArith1.test_step_2 [definition, in Smallstep]
SimpleArith1.test_step_1 [definition, in Smallstep]
_ --> _ [notation, in Smallstep]
SimpleArith2 [module, in Smallstep]
SimpleArith2.step_deterministic [lemma, in Smallstep]
SimpleArith3 [module, in Smallstep]
SimpleArith3.step_deterministic_alt [lemma, in Smallstep]
SkipExample [module, in UseTactics]
SkipExample.ceval_deterministic [lemma, in UseTactics]
SkipExample.demo_admits [lemma, in UseTactics]
SkipExample.mult_plus_0 [lemma, in UseTactics]
skip_right [lemma, in Equiv]
skip_left [lemma, in Equiv]
skip_axiom [axiom, in LibTactics]
slow_assignment [lemma, in Hoare2]
slow_assignment_dec [definition, in Hoare2]
Smallstep [library]
solved_by_jauto [lemma, in UseAuto]
solving_by_symmetry [lemma, in UseAuto]
solving_exists_hyp [lemma, in UseAuto]
solving_exists_goal [lemma, in UseAuto]
solving_tauto [lemma, in UseAuto]
solving_disj_hyp [lemma, in UseAuto]
solving_disj_goal [lemma, in UseAuto]
solving_conj_hyp_forall [lemma, in UseAuto]
solving_conj_more [lemma, in UseAuto]
solving_conj_hyp' [lemma, in UseAuto]
solving_conj_hyp [lemma, in UseAuto]
solving_conj_goal [lemma, in UseAuto]
solving_by_eapply [lemma, in UseAuto]
solving_by_apply [lemma, in UseAuto]
solving_by_reflexivity [lemma, in UseAuto]
SortExamples [module, in UseTactics]
SortExamples.ceval_deterministic [lemma, in UseTactics]
sqrt_correct [lemma, in Hoare2]
sqrt_dec [definition, in Hoare2]
SS_Mult [constructor, in Smallstep]
SS_Minus [constructor, in Smallstep]
SS_Plus [constructor, in Smallstep]
SS_Load [constructor, in Smallstep]
SS_Push [constructor, in Smallstep]
stack [definition, in Smallstep]
stack_multistep [definition, in Smallstep]
stack_step_deterministic [lemma, in Smallstep]
stack_step_sind [definition, in Smallstep]
stack_step_ind [definition, in Smallstep]
stack_step [inductive, in Smallstep]
step [inductive, in Smallstep]
step [inductive, in Norm]
StepFunction [module, in Typechecking]
StepFunction.assert [definition, in Typechecking]
StepFunction.complete_stepf [lemma, in Typechecking]
StepFunction.complete_valuef [lemma, in Typechecking]
StepFunction.manual_grade_for_stepf_defn [definition, in Typechecking]
StepFunction.manual_grade_for_valuef_defn [definition, in Typechecking]
StepFunction.sound_stepf [lemma, in Typechecking]
StepFunction.sound_valuef [lemma, in Typechecking]
StepFunction.stepf [definition, in Typechecking]
StepFunction.valuef [definition, in Typechecking]
StepFunction.value_stepf_nf [lemma, in Typechecking]
step_example1''' [definition, in Smallstep]
step_example1'' [definition, in Smallstep]
step_example1' [definition, in Smallstep]
step_example1 [definition, in Smallstep]
step__eval [lemma, in Smallstep]
step_normalizing [lemma, in Smallstep]
step_normal_form [definition, in Smallstep]
step_deterministic [lemma, in Smallstep]
step_sind [definition, in Smallstep]
step_ind [definition, in Smallstep]
step_preserves_R' [lemma, in Norm]
step_preserves_R [lemma, in Norm]
step_preserves_halting [lemma, in Norm]
step_deterministic [lemma, in Norm]
step_normal_form [abbreviation, in Norm]
step_sind [definition, in Norm]
step_ind [definition, in Norm]
STLC [module, in Stlc]
Stlc [library]
STLCArith [module, in StlcProp]
STLCArith.context [definition, in StlcProp]
STLCArith.has_type_sind [definition, in StlcProp]
STLCArith.has_type_rec [definition, in StlcProp]
STLCArith.has_type_ind [definition, in StlcProp]
STLCArith.has_type_rect [definition, in StlcProp]
STLCArith.has_type [inductive, in StlcProp]
STLCArith.multistep [abbreviation, in StlcProp]
STLCArith.Nat_typing_example [definition, in StlcProp]
STLCArith.Nat_step_example [definition, in StlcProp]
STLCArith.preservation [lemma, in StlcProp]
STLCArith.progress [lemma, in StlcProp]
STLCArith.step [inductive, in StlcProp]
STLCArith.step_sind [definition, in StlcProp]
STLCArith.step_rec [definition, in StlcProp]
STLCArith.step_ind [definition, in StlcProp]
STLCArith.step_rect [definition, in StlcProp]
STLCArith.subst [definition, in StlcProp]
STLCArith.tm [inductive, in StlcProp]
STLCArith.tm_sind [definition, in StlcProp]
STLCArith.tm_rec [definition, in StlcProp]
STLCArith.tm_ind [definition, in StlcProp]
STLCArith.tm_rect [definition, in StlcProp]
STLCArith.tm_if0 [constructor, in StlcProp]
STLCArith.tm_mult [constructor, in StlcProp]
STLCArith.tm_pred [constructor, in StlcProp]
STLCArith.tm_succ [constructor, in StlcProp]
STLCArith.tm_const [constructor, in StlcProp]
STLCArith.tm_abs [constructor, in StlcProp]
STLCArith.tm_app [constructor, in StlcProp]
STLCArith.tm_var [constructor, in StlcProp]
STLCArith.ty [inductive, in StlcProp]
STLCArith.ty_sind [definition, in StlcProp]
STLCArith.ty_rec [definition, in StlcProp]
STLCArith.ty_ind [definition, in StlcProp]
STLCArith.ty_rect [definition, in StlcProp]
STLCArith.Ty_Nat [constructor, in StlcProp]
STLCArith.Ty_Arrow [constructor, in StlcProp]
STLCArith.value [inductive, in StlcProp]
STLCArith.value_sind [definition, in StlcProp]
STLCArith.value_rec [definition, in StlcProp]
STLCArith.value_ind [definition, in StlcProp]
STLCArith.value_rect [definition, in StlcProp]
STLCArith.weakening [lemma, in StlcProp]
stlc_tm:if0 _ then _ else _ (stlc_scope) [notation, in StlcProp]
stlc_tm:_ * _ (stlc_scope) [notation, in StlcProp]
stlc_tm:pred _ (stlc_scope) [notation, in StlcProp]
stlc_tm:succ _ (stlc_scope) [notation, in StlcProp]
stlc_ty:Nat [notation, in StlcProp]
stlc_tm:\ _ : _ , _ [notation, in StlcProp]
stlc_tm:_ _ (stlc_scope) [notation, in StlcProp]
stlc_tm:( _ ) (stlc_scope) [notation, in StlcProp]
stlc_tm:_ (stlc_scope) [notation, in StlcProp]
stlc_tm:$( _ ) (stlc_scope) [notation, in StlcProp]
stlc_ty:$( _ ) (stlc_scope) [notation, in StlcProp]
stlc_ty:_ -> _ (stlc_scope) [notation, in StlcProp]
stlc_ty:( _ ) (stlc_scope) [notation, in StlcProp]
<{ _ }> (stlc_scope) [notation, in StlcProp]
_ -->* _ [notation, in StlcProp]
_ --> _ [notation, in StlcProp]
<{ _ |-- _ ∈ _ }> [notation, in StlcProp]
<{{ _ }}> [notation, in StlcProp]
STLCChecker [module, in Typechecking]
STLCChecker.type_checking_complete [lemma, in Typechecking]
STLCChecker.type_checking_sound [lemma, in Typechecking]
STLCChecker.type_check [definition, in Typechecking]
STLCExtended [module, in MoreStlc]
STLCExtendedRecords [module, in Records]
STLCExtendedRecords.A [abbreviation, in Records]
STLCExtendedRecords.a [abbreviation, in Records]
STLCExtendedRecords.B [abbreviation, in Records]
STLCExtendedRecords.context [definition, in Records]
STLCExtendedRecords.f [abbreviation, in Records]
STLCExtendedRecords.FirstTry [module, in Records]
STLCExtendedRecords.FirstTry.alist [definition, in Records]
STLCExtendedRecords.FirstTry.Arrow [constructor, in Records]
STLCExtendedRecords.FirstTry.Base [constructor, in Records]
STLCExtendedRecords.FirstTry.TRcd [constructor, in Records]
STLCExtendedRecords.FirstTry.ty [inductive, in Records]
STLCExtendedRecords.FirstTry.ty_sind [definition, in Records]
STLCExtendedRecords.FirstTry.ty_rec [definition, in Records]
STLCExtendedRecords.FirstTry.ty_ind [definition, in Records]
STLCExtendedRecords.FirstTry.ty_rect [definition, in Records]
STLCExtendedRecords.g [abbreviation, in Records]
STLCExtendedRecords.has_type__wf [lemma, in Records]
STLCExtendedRecords.has_type_sind [definition, in Records]
STLCExtendedRecords.has_type_ind [definition, in Records]
STLCExtendedRecords.has_type [inductive, in Records]
STLCExtendedRecords.i1 [abbreviation, in Records]
STLCExtendedRecords.i2 [abbreviation, in Records]
STLCExtendedRecords.k [abbreviation, in Records]
STLCExtendedRecords.l [abbreviation, in Records]
STLCExtendedRecords.lookup_field_in_value [lemma, in Records]
STLCExtendedRecords.multistep [abbreviation, in Records]
STLCExtendedRecords.preservation [lemma, in Records]
STLCExtendedRecords.progress [lemma, in Records]
STLCExtendedRecords.record_tm_sind [definition, in Records]
STLCExtendedRecords.record_tm_ind [definition, in Records]
STLCExtendedRecords.record_tm [inductive, in Records]
STLCExtendedRecords.record_ty_sind [definition, in Records]
STLCExtendedRecords.record_ty_ind [definition, in Records]
STLCExtendedRecords.record_ty [inductive, in Records]
STLCExtendedRecords.rtcons [constructor, in Records]
STLCExtendedRecords.RTcons [constructor, in Records]
STLCExtendedRecords.rtnil [constructor, in Records]
STLCExtendedRecords.RTnil [constructor, in Records]
STLCExtendedRecords.step [inductive, in Records]
STLCExtendedRecords.step_preserves_record_tm [lemma, in Records]
STLCExtendedRecords.step_sind [definition, in Records]
STLCExtendedRecords.step_ind [definition, in Records]
STLCExtendedRecords.ST_Rcd_Tail [constructor, in Records]
STLCExtendedRecords.ST_Rcd_Head [constructor, in Records]
STLCExtendedRecords.ST_ProjRcd [constructor, in Records]
STLCExtendedRecords.ST_Proj1 [constructor, in Records]
STLCExtendedRecords.ST_App2 [constructor, in Records]
STLCExtendedRecords.ST_App1 [constructor, in Records]
STLCExtendedRecords.ST_AppAbs [constructor, in Records]
STLCExtendedRecords.subst [definition, in Records]
STLCExtendedRecords.substitution_preserves_typing [lemma, in Records]
STLCExtendedRecords.Tlookup [definition, in Records]
STLCExtendedRecords.tlookup [definition, in Records]
STLCExtendedRecords.tm [inductive, in Records]
STLCExtendedRecords.tm_sind [definition, in Records]
STLCExtendedRecords.tm_rec [definition, in Records]
STLCExtendedRecords.tm_ind [definition, in Records]
STLCExtendedRecords.tm_rect [definition, in Records]
STLCExtendedRecords.tm_rcons [constructor, in Records]
STLCExtendedRecords.tm_rnil [constructor, in Records]
STLCExtendedRecords.tm_rproj [constructor, in Records]
STLCExtendedRecords.tm_abs [constructor, in Records]
STLCExtendedRecords.tm_app [constructor, in Records]
STLCExtendedRecords.tm_var [constructor, in Records]
STLCExtendedRecords.ty [inductive, in Records]
STLCExtendedRecords.typing_nonexample_2 [definition, in Records]
STLCExtendedRecords.typing_nonexample [definition, in Records]
STLCExtendedRecords.typing_example_2 [lemma, in Records]
STLCExtendedRecords.ty_sind [definition, in Records]
STLCExtendedRecords.ty_rec [definition, in Records]
STLCExtendedRecords.ty_ind [definition, in Records]
STLCExtendedRecords.ty_rect [definition, in Records]
STLCExtendedRecords.Ty_RCons [constructor, in Records]
STLCExtendedRecords.Ty_RNil [constructor, in Records]
STLCExtendedRecords.Ty_Arrow [constructor, in Records]
STLCExtendedRecords.Ty_Base [constructor, in Records]
STLCExtendedRecords.T_RCons [constructor, in Records]
STLCExtendedRecords.T_RNil [constructor, in Records]
STLCExtendedRecords.T_Proj [constructor, in Records]
STLCExtendedRecords.T_App [constructor, in Records]
STLCExtendedRecords.T_Abs [constructor, in Records]
STLCExtendedRecords.T_Var [constructor, in Records]
STLCExtendedRecords.value [inductive, in Records]
STLCExtendedRecords.value_sind [definition, in Records]
STLCExtendedRecords.value_ind [definition, in Records]
STLCExtendedRecords.v_rcons [constructor, in Records]
STLCExtendedRecords.v_rnil [constructor, in Records]
STLCExtendedRecords.v_abs [constructor, in Records]
STLCExtendedRecords.weakening [lemma, in Records]
STLCExtendedRecords.weakening_empty [lemma, in Records]
STLCExtendedRecords.weird_type [definition, in Records]
STLCExtendedRecords.well_formed_ty_sind [definition, in Records]
STLCExtendedRecords.well_formed_ty_ind [definition, in Records]
STLCExtendedRecords.well_formed_ty [inductive, in Records]
STLCExtendedRecords.wfArrow [constructor, in Records]
STLCExtendedRecords.wfBase [constructor, in Records]
STLCExtendedRecords.wfRCons [constructor, in Records]
STLCExtendedRecords.wfRNil [constructor, in Records]
STLCExtendedRecords.wf_rcd_lookup [lemma, in Records]
STLCExtendedRecords.wf_ty_example [lemma, in Records]
stlc_tm:empty (stlc_scope) [notation, in Records]
stlc_tm:_ ⊢> _ (stlc_scope) [notation, in Records]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [notation, in Records]
stlc_tm:[ _ := _ ] _ [notation, in Records]
stlc_tm:_ --> _ [notation, in Records]
stlc_tm:nil [notation, in Records]
stlc_ty:nil [notation, in Records]
stlc_tm:_ := _ :: _ [notation, in Records]
stlc_ty:_ : _ :: _ [notation, in Records]
stlc_ty:Base _ (stlc_scope) [notation, in Records]
stlc_tm:\ _ : _ , _ [notation, in Records]
stlc_tm:_ _ (stlc_scope) [notation, in Records]
stlc_tm:( _ ) (stlc_scope) [notation, in Records]
stlc_tm:_ (stlc_scope) [notation, in Records]
stlc_tm:$( _ ) (stlc_scope) [notation, in Records]
stlc_ty:$( _ ) (stlc_scope) [notation, in Records]
stlc_ty:_ -> _ (stlc_scope) [notation, in Records]
stlc_ty:( _ ) (stlc_scope) [notation, in Records]
stlc_ty:_ (stlc_scope) [notation, in Records]
<{ _ }> (stlc_scope) [notation, in Records]
_ -->* _ [notation, in Records]
_ --> _ [notation, in Records]
<{ _ |-- _ ∈ _ }> [notation, in Records]
<{{ _ }}> [notation, in Records]
STLCExtended.context [definition, in MoreStlc]
STLCExtended.Examples [module, in MoreStlc]
STLCExtended.Examples.a [abbreviation, in MoreStlc]
STLCExtended.Examples.eo [abbreviation, in MoreStlc]
STLCExtended.Examples.eq [abbreviation, in MoreStlc]
STLCExtended.Examples.even [abbreviation, in MoreStlc]
STLCExtended.Examples.evenodd [abbreviation, in MoreStlc]
STLCExtended.Examples.f [abbreviation, in MoreStlc]
STLCExtended.Examples.FixTest1 [module, in MoreStlc]
STLCExtended.Examples.FixTest1.fact [definition, in MoreStlc]
STLCExtended.Examples.FixTest1.reduces [definition, in MoreStlc]
STLCExtended.Examples.FixTest1.typechecks [definition, in MoreStlc]
STLCExtended.Examples.FixTest2 [module, in MoreStlc]
STLCExtended.Examples.FixTest2.map [definition, in MoreStlc]
STLCExtended.Examples.FixTest2.reduces [definition, in MoreStlc]
STLCExtended.Examples.FixTest2.typechecks [definition, in MoreStlc]
STLCExtended.Examples.FixTest3 [module, in MoreStlc]
STLCExtended.Examples.FixTest3.equal [definition, in MoreStlc]
STLCExtended.Examples.FixTest3.reduces [definition, in MoreStlc]
STLCExtended.Examples.FixTest3.reduces2 [definition, in MoreStlc]
STLCExtended.Examples.FixTest3.typechecks [definition, in MoreStlc]
STLCExtended.Examples.FixTest4 [module, in MoreStlc]
STLCExtended.Examples.FixTest4.eotest [definition, in MoreStlc]
STLCExtended.Examples.FixTest4.reduces [definition, in MoreStlc]
STLCExtended.Examples.FixTest4.typechecks [definition, in MoreStlc]
STLCExtended.Examples.g [abbreviation, in MoreStlc]
STLCExtended.Examples.i1 [abbreviation, in MoreStlc]
STLCExtended.Examples.i2 [abbreviation, in MoreStlc]
STLCExtended.Examples.k [abbreviation, in MoreStlc]
STLCExtended.Examples.l [abbreviation, in MoreStlc]
STLCExtended.Examples.LetTest [module, in MoreStlc]
STLCExtended.Examples.LetTest.reduces [definition, in MoreStlc]
STLCExtended.Examples.LetTest.tm_test [definition, in MoreStlc]
STLCExtended.Examples.LetTest.typechecks [definition, in MoreStlc]
STLCExtended.Examples.LetTest1 [module, in MoreStlc]
STLCExtended.Examples.LetTest1.reduces [definition, in MoreStlc]
STLCExtended.Examples.LetTest1.tm_test [definition, in MoreStlc]
STLCExtended.Examples.LetTest1.typechecks [definition, in MoreStlc]
STLCExtended.Examples.ListTest [module, in MoreStlc]
STLCExtended.Examples.ListTest.reduces [definition, in MoreStlc]
STLCExtended.Examples.ListTest.tm_test [definition, in MoreStlc]
STLCExtended.Examples.ListTest.typechecks [definition, in MoreStlc]
STLCExtended.Examples.m [abbreviation, in MoreStlc]
STLCExtended.Examples.n [abbreviation, in MoreStlc]
STLCExtended.Examples.Numtest [module, in MoreStlc]
STLCExtended.Examples.Numtest.reduces [definition, in MoreStlc]
STLCExtended.Examples.Numtest.tm_test [definition, in MoreStlc]
STLCExtended.Examples.Numtest.typechecks [definition, in MoreStlc]
STLCExtended.Examples.odd [abbreviation, in MoreStlc]
STLCExtended.Examples.processSum [abbreviation, in MoreStlc]
STLCExtended.Examples.ProdTest [module, in MoreStlc]
STLCExtended.Examples.ProdTest.reduces [definition, in MoreStlc]
STLCExtended.Examples.ProdTest.tm_test [definition, in MoreStlc]
STLCExtended.Examples.ProdTest.typechecks [definition, in MoreStlc]
STLCExtended.Examples.Sumtest1 [module, in MoreStlc]
STLCExtended.Examples.Sumtest1.reduces [definition, in MoreStlc]
STLCExtended.Examples.Sumtest1.tm_test [definition, in MoreStlc]
STLCExtended.Examples.Sumtest1.typechecks [definition, in MoreStlc]
STLCExtended.Examples.Sumtest2 [module, in MoreStlc]
STLCExtended.Examples.Sumtest2.reduces [definition, in MoreStlc]
STLCExtended.Examples.Sumtest2.tm_test [definition, in MoreStlc]
STLCExtended.Examples.Sumtest2.typechecks [definition, in MoreStlc]
STLCExtended.Examples.x [abbreviation, in MoreStlc]
STLCExtended.Examples.y [abbreviation, in MoreStlc]
STLCExtended.has_type_sind [definition, in MoreStlc]
STLCExtended.has_type_ind [definition, in MoreStlc]
STLCExtended.has_type [inductive, in MoreStlc]
STLCExtended.multistep [abbreviation, in MoreStlc]
STLCExtended.preservation [lemma, in MoreStlc]
STLCExtended.progress [lemma, in MoreStlc]
STLCExtended.step [inductive, in MoreStlc]
STLCExtended.step_sind [definition, in MoreStlc]
STLCExtended.step_ind [definition, in MoreStlc]
STLCExtended.ST_LcaseCons [constructor, in MoreStlc]
STLCExtended.ST_LcaseNil [constructor, in MoreStlc]
STLCExtended.ST_Lcase1 [constructor, in MoreStlc]
STLCExtended.ST_Cons2 [constructor, in MoreStlc]
STLCExtended.ST_Cons1 [constructor, in MoreStlc]
STLCExtended.ST_CaseInr [constructor, in MoreStlc]
STLCExtended.ST_CaseInl [constructor, in MoreStlc]
STLCExtended.ST_Case [constructor, in MoreStlc]
STLCExtended.ST_Inr [constructor, in MoreStlc]
STLCExtended.ST_Inl [constructor, in MoreStlc]
STLCExtended.ST_If0_Nonzero [constructor, in MoreStlc]
STLCExtended.ST_If0_Zero [constructor, in MoreStlc]
STLCExtended.ST_If0 [constructor, in MoreStlc]
STLCExtended.ST_Mult2 [constructor, in MoreStlc]
STLCExtended.ST_Mult1 [constructor, in MoreStlc]
STLCExtended.ST_Mulconsts [constructor, in MoreStlc]
STLCExtended.ST_PredNat [constructor, in MoreStlc]
STLCExtended.ST_Pred [constructor, in MoreStlc]
STLCExtended.ST_SuccNat [constructor, in MoreStlc]
STLCExtended.ST_Succ [constructor, in MoreStlc]
STLCExtended.ST_App2 [constructor, in MoreStlc]
STLCExtended.ST_App1 [constructor, in MoreStlc]
STLCExtended.ST_AppAbs [constructor, in MoreStlc]
STLCExtended.subst [definition, in MoreStlc]
STLCExtended.substeg1 [definition, in MoreStlc]
STLCExtended.substeg2 [definition, in MoreStlc]
STLCExtended.substeg3 [definition, in MoreStlc]
STLCExtended.substitution_preserves_typing [lemma, in MoreStlc]
STLCExtended.tm [inductive, in MoreStlc]
STLCExtended.tm_sind [definition, in MoreStlc]
STLCExtended.tm_rec [definition, in MoreStlc]
STLCExtended.tm_ind [definition, in MoreStlc]
STLCExtended.tm_rect [definition, in MoreStlc]
STLCExtended.tm_fix [constructor, in MoreStlc]
STLCExtended.tm_let [constructor, in MoreStlc]
STLCExtended.tm_snd [constructor, in MoreStlc]
STLCExtended.tm_fst [constructor, in MoreStlc]
STLCExtended.tm_pair [constructor, in MoreStlc]
STLCExtended.tm_unit [constructor, in MoreStlc]
STLCExtended.tm_lcase [constructor, in MoreStlc]
STLCExtended.tm_cons [constructor, in MoreStlc]
STLCExtended.tm_nil [constructor, in MoreStlc]
STLCExtended.tm_case [constructor, in MoreStlc]
STLCExtended.tm_inr [constructor, in MoreStlc]
STLCExtended.tm_inl [constructor, in MoreStlc]
STLCExtended.tm_if0 [constructor, in MoreStlc]
STLCExtended.tm_mult [constructor, in MoreStlc]
STLCExtended.tm_pred [constructor, in MoreStlc]
STLCExtended.tm_succ [constructor, in MoreStlc]
STLCExtended.tm_const [constructor, in MoreStlc]
STLCExtended.tm_abs [constructor, in MoreStlc]
STLCExtended.tm_app [constructor, in MoreStlc]
STLCExtended.tm_var [constructor, in MoreStlc]
STLCExtended.ty [inductive, in MoreStlc]
STLCExtended.ty_sind [definition, in MoreStlc]
STLCExtended.ty_rec [definition, in MoreStlc]
STLCExtended.ty_ind [definition, in MoreStlc]
STLCExtended.ty_rect [definition, in MoreStlc]
STLCExtended.Ty_Prod [constructor, in MoreStlc]
STLCExtended.Ty_Unit [constructor, in MoreStlc]
STLCExtended.Ty_List [constructor, in MoreStlc]
STLCExtended.Ty_Sum [constructor, in MoreStlc]
STLCExtended.Ty_Nat [constructor, in MoreStlc]
STLCExtended.Ty_Arrow [constructor, in MoreStlc]
STLCExtended.T_Unit [constructor, in MoreStlc]
STLCExtended.T_Lcase [constructor, in MoreStlc]
STLCExtended.T_Cons [constructor, in MoreStlc]
STLCExtended.T_Nil [constructor, in MoreStlc]
STLCExtended.T_Case [constructor, in MoreStlc]
STLCExtended.T_Inr [constructor, in MoreStlc]
STLCExtended.T_Inl [constructor, in MoreStlc]
STLCExtended.T_If0 [constructor, in MoreStlc]
STLCExtended.T_Mult [constructor, in MoreStlc]
STLCExtended.T_Pred [constructor, in MoreStlc]
STLCExtended.T_Succ [constructor, in MoreStlc]
STLCExtended.T_Nat [constructor, in MoreStlc]
STLCExtended.T_App [constructor, in MoreStlc]
STLCExtended.T_Abs [constructor, in MoreStlc]
STLCExtended.T_Var [constructor, in MoreStlc]
STLCExtended.value [inductive, in MoreStlc]
STLCExtended.value_sind [definition, in MoreStlc]
STLCExtended.value_ind [definition, in MoreStlc]
STLCExtended.v_pair [constructor, in MoreStlc]
STLCExtended.v_unit [constructor, in MoreStlc]
STLCExtended.v_lcons [constructor, in MoreStlc]
STLCExtended.v_lnil [constructor, in MoreStlc]
STLCExtended.v_inr [constructor, in MoreStlc]
STLCExtended.v_inl [constructor, in MoreStlc]
STLCExtended.v_nat [constructor, in MoreStlc]
STLCExtended.v_abs [constructor, in MoreStlc]
STLCExtended.w [definition, in MoreStlc]
STLCExtended.weakening [lemma, in MoreStlc]
STLCExtended.weakening_empty [lemma, in MoreStlc]
STLCExtended.x [definition, in MoreStlc]
STLCExtended.y [definition, in MoreStlc]
STLCExtended.z [definition, in MoreStlc]
stlc_tm:empty (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ ⊢> _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:[ _ := _ ] _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:fix _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:let _ = _ in _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:unit (stlc_scope) [notation, in MoreStlc]
stlc_ty:Unit (stlc_scope) [notation, in MoreStlc]
stlc_tm:case _ of | nil => _ | _ :: _ => _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ :: _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:nil _ (stlc_scope) [notation, in MoreStlc]
stlc_ty:List _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ .snd (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ .fst (stlc_scope) [notation, in MoreStlc]
stlc_tm:( _ , _ ) (stlc_scope) [notation, in MoreStlc]
stlc_ty:_ * _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:case _ of | inl _ => _ | inr _ => _ [notation, in MoreStlc]
stlc_tm:inr _ _ [notation, in MoreStlc]
stlc_tm:inl _ _ [notation, in MoreStlc]
stlc_ty:_ + _ [notation, in MoreStlc]
stlc_tm:if0 _ then _ else _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ * _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:pred _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:succ _ (stlc_scope) [notation, in MoreStlc]
stlc_ty:Nat [notation, in MoreStlc]
stlc_tm:\ _ : _ , _ [notation, in MoreStlc]
stlc_tm:_ _ (stlc_scope) [notation, in MoreStlc]
stlc_tm:( _ ) (stlc_scope) [notation, in MoreStlc]
stlc_tm:_ (stlc_scope) [notation, in MoreStlc]
stlc_tm:$( _ ) (stlc_scope) [notation, in MoreStlc]
stlc_ty:$( _ ) (stlc_scope) [notation, in MoreStlc]
stlc_ty:_ -> _ (stlc_scope) [notation, in MoreStlc]
stlc_ty:( _ ) (stlc_scope) [notation, in MoreStlc]
stlc_ty:_ (stlc_scope) [notation, in MoreStlc]
List _ (stlc_scope) [notation, in MoreStlc]
<{ _ }> (stlc_scope) [notation, in MoreStlc]
_ -->* _ [notation, in MoreStlc]
_ --> _ [notation, in MoreStlc]
<{ _ |-- _ ∈ _ }> [notation, in MoreStlc]
<{{ _ }}> [notation, in MoreStlc]
StlcImpl [module, in Typechecking]
STLCProp [module, in StlcProp]
StlcProp [library]
STLCProp.afi_if3 [constructor, in StlcProp]
STLCProp.afi_if2 [constructor, in StlcProp]
STLCProp.afi_if1 [constructor, in StlcProp]
STLCProp.afi_abs [constructor, in StlcProp]
STLCProp.afi_app2 [constructor, in StlcProp]
STLCProp.afi_app1 [constructor, in StlcProp]
STLCProp.afi_var [constructor, in StlcProp]
STLCProp.appears_free_in_sind [definition, in StlcProp]
STLCProp.appears_free_in_ind [definition, in StlcProp]
STLCProp.appears_free_in [inductive, in StlcProp]
STLCProp.canonical_forms_fun [lemma, in StlcProp]
STLCProp.canonical_forms_bool [lemma, in StlcProp]
STLCProp.closed [definition, in StlcProp]
STLCProp.context_invariance [lemma, in StlcProp]
STLCProp.free_in_context [lemma, in StlcProp]
STLCProp.manual_grade_for_stlc_variation3 [definition, in StlcProp]
STLCProp.manual_grade_for_stlc_variation2 [definition, in StlcProp]
STLCProp.manual_grade_for_stlc_variation1 [definition, in StlcProp]
STLCProp.manual_grade_for_progress_preservation_statement [definition, in StlcProp]
STLCProp.manual_grade_for_afi [definition, in StlcProp]
STLCProp.manual_grade_for_subject_expansion_stlc [definition, in StlcProp]
STLCProp.not_subject_expansion [lemma, in StlcProp]
STLCProp.preservation [lemma, in StlcProp]
STLCProp.progress [lemma, in StlcProp]
STLCProp.progress' [lemma, in StlcProp]
STLCProp.stuck [definition, in StlcProp]
STLCProp.substitution_preserves_typing_from_typing_ind [lemma, in StlcProp]
STLCProp.substitution_preserves_typing [lemma, in StlcProp]
STLCProp.typable_empty__closed [lemma, in StlcProp]
STLCProp.type_soundness [lemma, in StlcProp]
STLCProp.unique_types [lemma, in StlcProp]
STLCProp.weakening [lemma, in StlcProp]
STLCProp.weakening_empty [lemma, in StlcProp]
STLCRef [module, in References]
STLCRef.assign_pres_store_typing [lemma, in References]
STLCRef.context [definition, in References]
STLCRef.cyclic_store [lemma, in References]
STLCRef.ExampleVariables [module, in References]
STLCRef.ExampleVariables.r [definition, in References]
STLCRef.ExampleVariables.s [definition, in References]
STLCRef.ExampleVariables.x [definition, in References]
STLCRef.ExampleVariables.y [definition, in References]
STLCRef.extends [inductive, in References]
STLCRef.extends_refl [lemma, in References]
STLCRef.extends_app [lemma, in References]
STLCRef.extends_lookup [lemma, in References]
STLCRef.extends_sind [definition, in References]
STLCRef.extends_ind [definition, in References]
STLCRef.extends_cons [constructor, in References]
STLCRef.extends_nil [constructor, in References]
STLCRef.has_type_sind [definition, in References]
STLCRef.has_type_ind [definition, in References]
STLCRef.has_type [inductive, in References]
STLCRef.length_extends [lemma, in References]
STLCRef.length_replace [lemma, in References]
STLCRef.lookup_replace_neq [lemma, in References]
STLCRef.lookup_replace_eq [lemma, in References]
STLCRef.manual_grade_for_preservation_informal [definition, in References]
STLCRef.manual_grade_for_type_safety_violation [definition, in References]
STLCRef.manual_grade_for_compact_update [definition, in References]
STLCRef.multistep [definition, in References]
STLCRef.nth_eq_last [lemma, in References]
STLCRef.preservation [lemma, in References]
STLCRef.preservation_theorem [definition, in References]
STLCRef.preservation_wrong2 [lemma, in References]
STLCRef.preservation_wrong1 [lemma, in References]
STLCRef.progress [lemma, in References]
STLCRef.RefsAndNontermination [module, in References]
STLCRef.RefsAndNontermination.factorial [definition, in References]
STLCRef.RefsAndNontermination.factorial_type [lemma, in References]
STLCRef.RefsAndNontermination.loop [definition, in References]
STLCRef.RefsAndNontermination.loop_fun_step_self [lemma, in References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [lemma, in References]
STLCRef.RefsAndNontermination.loop_typeable [lemma, in References]
STLCRef.RefsAndNontermination.loop_fun [definition, in References]
STLCRef.RefsAndNontermination.multistep1 [definition, in References]
STLCRef.RefsAndNontermination.sc_step [constructor, in References]
STLCRef.RefsAndNontermination.sc_one [constructor, in References]
STLCRef.RefsAndNontermination.step_closure_sind [definition, in References]
STLCRef.RefsAndNontermination.step_closure_ind [definition, in References]
STLCRef.RefsAndNontermination.step_closure [inductive, in References]
_ / _ -->+ _ / _ [notation, in References]
STLCRef.replace [definition, in References]
STLCRef.replace_nil [lemma, in References]
STLCRef.step [inductive, in References]
STLCRef.step_sind [definition, in References]
STLCRef.step_ind [definition, in References]
STLCRef.store [definition, in References]
STLCRef.store_well_typed_app [lemma, in References]
STLCRef.store_weakening [lemma, in References]
STLCRef.store_not_unique [lemma, in References]
STLCRef.store_well_typed [definition, in References]
STLCRef.store_Tlookup [definition, in References]
STLCRef.store_ty [definition, in References]
STLCRef.store_lookup [definition, in References]
STLCRef.ST_Assign2 [constructor, in References]
STLCRef.ST_Assign1 [constructor, in References]
STLCRef.ST_Assign [constructor, in References]
STLCRef.ST_Deref [constructor, in References]
STLCRef.ST_DerefLoc [constructor, in References]
STLCRef.ST_Ref [constructor, in References]
STLCRef.ST_RefValue [constructor, in References]
STLCRef.ST_If0_Nonzero [constructor, in References]
STLCRef.ST_If0_Zero [constructor, in References]
STLCRef.ST_If0 [constructor, in References]
STLCRef.ST_Mult2 [constructor, in References]
STLCRef.ST_Mult1 [constructor, in References]
STLCRef.ST_MultNats [constructor, in References]
STLCRef.ST_Pred [constructor, in References]
STLCRef.ST_PredNat [constructor, in References]
STLCRef.ST_Succ [constructor, in References]
STLCRef.ST_SuccNat [constructor, in References]
STLCRef.ST_App2 [constructor, in References]
STLCRef.ST_App1 [constructor, in References]
STLCRef.ST_AppAbs [constructor, in References]
STLCRef.subst [definition, in References]
STLCRef.substitution_preserves_typing [lemma, in References]
STLCRef.tm [inductive, in References]
STLCRef.tm_sind [definition, in References]
STLCRef.tm_rec [definition, in References]
STLCRef.tm_ind [definition, in References]
STLCRef.tm_rect [definition, in References]
STLCRef.tm_loc [constructor, in References]
STLCRef.tm_assign [constructor, in References]
STLCRef.tm_deref [constructor, in References]
STLCRef.tm_ref [constructor, in References]
STLCRef.tm_unit [constructor, in References]
STLCRef.tm_if0 [constructor, in References]
STLCRef.tm_mult [constructor, in References]
STLCRef.tm_pred [constructor, in References]
STLCRef.tm_succ [constructor, in References]
STLCRef.tm_const [constructor, in References]
STLCRef.tm_abs [constructor, in References]
STLCRef.tm_app [constructor, in References]
STLCRef.tm_var [constructor, in References]
STLCRef.tseq [definition, in References]
STLCRef.ty [inductive, in References]
STLCRef.ty_sind [definition, in References]
STLCRef.ty_rec [definition, in References]
STLCRef.ty_ind [definition, in References]
STLCRef.ty_rect [definition, in References]
STLCRef.Ty_Ref [constructor, in References]
STLCRef.Ty_Arrow [constructor, in References]
STLCRef.Ty_Unit [constructor, in References]
STLCRef.Ty_Nat [constructor, in References]
STLCRef.T_Assign [constructor, in References]
STLCRef.T_Deref [constructor, in References]
STLCRef.T_Ref [constructor, in References]
STLCRef.T_Loc [constructor, in References]
STLCRef.T_Unit [constructor, in References]
STLCRef.T_If0 [constructor, in References]
STLCRef.T_Mult [constructor, in References]
STLCRef.T_Pred [constructor, in References]
STLCRef.T_Succ [constructor, in References]
STLCRef.T_Nat [constructor, in References]
STLCRef.T_App [constructor, in References]
STLCRef.T_Abs [constructor, in References]
STLCRef.T_Var [constructor, in References]
STLCRef.value [inductive, in References]
STLCRef.value_sind [definition, in References]
STLCRef.value_ind [definition, in References]
STLCRef.v_loc [constructor, in References]
STLCRef.v_unit [constructor, in References]
STLCRef.v_nat [constructor, in References]
STLCRef.v_abs [constructor, in References]
STLCRef.weakening [lemma, in References]
STLCRef.weakening_empty [lemma, in References]
STLCRef.x [definition, in References]
STLCRef.y [definition, in References]
STLCRef.z [definition, in References]
stlc_tm:empty (stlc_scope) [notation, in References]
stlc_tm:_ ⊢> _ (stlc_scope) [notation, in References]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [notation, in References]
stlc_tm:_ ; _ (stlc_scope) [notation, in References]
stlc_tm:[ _ := _ ] _ (stlc_scope) [notation, in References]
stlc_tm:_ := _ (stlc_scope) [notation, in References]
stlc_tm:! _ (stlc_scope) [notation, in References]
stlc_tm:ref _ (stlc_scope) [notation, in References]
stlc_tm:loc _ (stlc_scope) [notation, in References]
stlc_ty:Ref _ [notation, in References]
stlc_tm:unit (stlc_scope) [notation, in References]
stlc_ty:Unit (stlc_scope) [notation, in References]
stlc_tm:if0 _ then _ else _ (stlc_scope) [notation, in References]
stlc_tm:_ * _ (stlc_scope) [notation, in References]
stlc_tm:pred _ (stlc_scope) [notation, in References]
stlc_tm:succ _ (stlc_scope) [notation, in References]
stlc_ty:Nat [notation, in References]
stlc_tm:\ _ : _ , _ [notation, in References]
stlc_tm:_ _ (stlc_scope) [notation, in References]
stlc_tm:( _ ) (stlc_scope) [notation, in References]
stlc_tm:_ (stlc_scope) [notation, in References]
stlc_tm:$( _ ) (stlc_scope) [notation, in References]
stlc_ty:$( _ ) (stlc_scope) [notation, in References]
stlc_ty:_ -> _ (stlc_scope) [notation, in References]
stlc_ty:( _ ) (stlc_scope) [notation, in References]
stlc_ty:_ (stlc_scope) [notation, in References]
<{ _ }> (stlc_scope) [notation, in References]
_ / _ -->* _ / _ [notation, in References]
_ / _ --> _ / _ [notation, in References]
<{ _ / _ |-- _ ∈ _ }> [notation, in References]
<{{ _ }}> [notation, in References]
STLCSub [module, in Sub]
STLCSub.abs_arrow [lemma, in Sub]
STLCSub.canonical_forms_of_Bool [lemma, in Sub]
STLCSub.canonical_forms_of_arrow_types [lemma, in Sub]
STLCSub.context [definition, in Sub]
STLCSub.Examples [module, in Sub]
STLCSub.Examples.A [abbreviation, in Sub]
STLCSub.Examples.B [abbreviation, in Sub]
STLCSub.Examples.C [abbreviation, in Sub]
STLCSub.Examples.Employee [definition, in Sub]
STLCSub.Examples.Float [abbreviation, in Sub]
STLCSub.Examples.Integer [abbreviation, in Sub]
STLCSub.Examples.Person [definition, in Sub]
STLCSub.Examples.String [abbreviation, in Sub]
STLCSub.Examples.Student [definition, in Sub]
STLCSub.Examples.subtyping_example_2 [definition, in Sub]
STLCSub.Examples.subtyping_example_1 [definition, in Sub]
STLCSub.Examples.subtyping_example_0 [definition, in Sub]
STLCSub.Examples.sub_employee_person [definition, in Sub]
STLCSub.Examples.sub_student_person [definition, in Sub]
STLCSub.Examples.x [abbreviation, in Sub]
STLCSub.Examples.y [abbreviation, in Sub]
STLCSub.Examples.z [abbreviation, in Sub]
STLCSub.Examples2 [module, in Sub]
STLCSub.FormalThoughtExercises [module, in Sub]
STLCSub.FormalThoughtExercises.a [abbreviation, in Sub]
STLCSub.FormalThoughtExercises.formal_proper_subtypes [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfh [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfg [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tff [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfe [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfd [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfc [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfb [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfa [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2e [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2d [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2b [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2a [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1g [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1f [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1e [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1d [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1c [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1b [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1a [lemma, in Sub]
STLCSub.FormalThoughtExercises.p [abbreviation, in Sub]
STLCSub.FormalThoughtExercises.TF [definition, in Sub]
STLCSub.has_type_sind [definition, in Sub]
STLCSub.has_type_ind [definition, in Sub]
STLCSub.has_type [inductive, in Sub]
STLCSub.manual_grade_for_products_preservation [definition, in Sub]
STLCSub.manual_grade_for_products_progress [definition, in Sub]
STLCSub.manual_grade_for_products_subtype_has_type [definition, in Sub]
STLCSub.manual_grade_for_products_value_step [definition, in Sub]
STLCSub.manual_grade_for_variations [definition, in Sub]
STLCSub.preservation [lemma, in Sub]
STLCSub.progress [lemma, in Sub]
STLCSub.step [inductive, in Sub]
STLCSub.step_sind [definition, in Sub]
STLCSub.step_ind [definition, in Sub]
STLCSub.ST_If [constructor, in Sub]
STLCSub.ST_IfFalse [constructor, in Sub]
STLCSub.ST_IfTrue [constructor, in Sub]
STLCSub.ST_App2 [constructor, in Sub]
STLCSub.ST_App1 [constructor, in Sub]
STLCSub.ST_AppAbs [constructor, in Sub]
STLCSub.subst [definition, in Sub]
STLCSub.substitution_preserves_typing [lemma, in Sub]
STLCSub.subtype [inductive, in Sub]
STLCSub.subtype_sind [definition, in Sub]
STLCSub.subtype_ind [definition, in Sub]
STLCSub.sub_inversion_Top [lemma, in Sub]
STLCSub.sub_inversion_Base [lemma, in Sub]
STLCSub.sub_inversion_Unit [lemma, in Sub]
STLCSub.sub_inversion_arrow [lemma, in Sub]
STLCSub.sub_inversion_Bool [lemma, in Sub]
STLCSub.S_Arrow [constructor, in Sub]
STLCSub.S_Top [constructor, in Sub]
STLCSub.S_Trans [constructor, in Sub]
STLCSub.S_Refl [constructor, in Sub]
STLCSub.tm [inductive, in Sub]
STLCSub.tm_sind [definition, in Sub]
STLCSub.tm_rec [definition, in Sub]
STLCSub.tm_ind [definition, in Sub]
STLCSub.tm_rect [definition, in Sub]
STLCSub.tm_snd [constructor, in Sub]
STLCSub.tm_fst [constructor, in Sub]
STLCSub.tm_pair [constructor, in Sub]
STLCSub.tm_unit [constructor, in Sub]
STLCSub.tm_if [constructor, in Sub]
STLCSub.tm_false [constructor, in Sub]
STLCSub.tm_true [constructor, in Sub]
STLCSub.tm_abs [constructor, in Sub]
STLCSub.tm_app [constructor, in Sub]
STLCSub.tm_var [constructor, in Sub]
STLCSub.ty [inductive, in Sub]
STLCSub.typing_inversion_unit [lemma, in Sub]
STLCSub.typing_inversion_app [lemma, in Sub]
STLCSub.typing_inversion_var [lemma, in Sub]
STLCSub.typing_inversion_abs [lemma, in Sub]
STLCSub.ty_sind [definition, in Sub]
STLCSub.ty_rec [definition, in Sub]
STLCSub.ty_ind [definition, in Sub]
STLCSub.ty_rect [definition, in Sub]
STLCSub.Ty_Prod [constructor, in Sub]
STLCSub.Ty_Unit [constructor, in Sub]
STLCSub.Ty_Arrow [constructor, in Sub]
STLCSub.Ty_Base [constructor, in Sub]
STLCSub.Ty_Bool [constructor, in Sub]
STLCSub.Ty_Top [constructor, in Sub]
STLCSub.T_Sub [constructor, in Sub]
STLCSub.T_Unit [constructor, in Sub]
STLCSub.T_If [constructor, in Sub]
STLCSub.T_False [constructor, in Sub]
STLCSub.T_True [constructor, in Sub]
STLCSub.T_App [constructor, in Sub]
STLCSub.T_Abs [constructor, in Sub]
STLCSub.T_Var [constructor, in Sub]
STLCSub.value [inductive, in Sub]
STLCSub.value_sind [definition, in Sub]
STLCSub.value_ind [definition, in Sub]
STLCSub.v_unit [constructor, in Sub]
STLCSub.v_false [constructor, in Sub]
STLCSub.v_true [constructor, in Sub]
STLCSub.v_abs [constructor, in Sub]
STLCSub.weakening [lemma, in Sub]
STLCSub.weakening_empty [lemma, in Sub]
stlc_tm:empty (stlc_scope) [notation, in Sub]
stlc_tm:_ ⊢> _ (stlc_scope) [notation, in Sub]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [notation, in Sub]
stlc_tm:[ _ := _ ] _ (stlc_scope) [notation, in Sub]
stlc_ty:Top (stlc_scope) [notation, in Sub]
stlc_tm:_ .snd (stlc_scope) [notation, in Sub]
stlc_tm:_ .fst (stlc_scope) [notation, in Sub]
stlc_tm:( _ , _ ) (stlc_scope) [notation, in Sub]
stlc_ty:_ * _ [notation, in Sub]
stlc_tm:unit (stlc_scope) [notation, in Sub]
stlc_ty:Unit (stlc_scope) [notation, in Sub]
stlc_ty:Base _ (stlc_scope) [notation, in Sub]
stlc_tm:false [notation, in Sub]
stlc_tm:true [notation, in Sub]
stlc_tm:if _ then _ else _ [notation, in Sub]
stlc_ty:Bool (stlc_scope) [notation, in Sub]
stlc_tm:\ _ : _ , _ [notation, in Sub]
stlc_tm:_ _ (stlc_scope) [notation, in Sub]
stlc_tm:( _ ) (stlc_scope) [notation, in Sub]
stlc_tm:_ (stlc_scope) [notation, in Sub]
stlc_tm:$( _ ) (stlc_scope) [notation, in Sub]
stlc_ty:$( _ ) (stlc_scope) [notation, in Sub]
stlc_ty:_ -> _ (stlc_scope) [notation, in Sub]
stlc_ty:( _ ) (stlc_scope) [notation, in Sub]
stlc_ty:_ (stlc_scope) [notation, in Sub]
<{ _ |-- _ ∈ _ }> (stlc_scope) [notation, in Sub]
<{ _ }> (stlc_scope) [notation, in Sub]
_ <: _ [notation, in Sub]
_ --> _ [notation, in Sub]
false [notation, in Sub]
true [notation, in Sub]
<{{ _ }}> [notation, in Sub]
STLCTypes [module, in Typechecking]
STLCTypes.eqb_ty__eq [lemma, in Typechecking]
STLCTypes.eqb_ty_refl [lemma, in Typechecking]
STLCTypes.eqb_ty [definition, in Typechecking]
STLC.context [definition, in Stlc]
STLC.has_type_sind [definition, in Stlc]
STLC.has_type_ind [definition, in Stlc]
STLC.has_type [inductive, in Stlc]
STLC.idB [abbreviation, in Stlc]
STLC.idBB [abbreviation, in Stlc]
STLC.idBBBB [abbreviation, in Stlc]
STLC.k [abbreviation, in Stlc]
STLC.multistep [abbreviation, in Stlc]
STLC.notB [abbreviation, in Stlc]
STLC.step [inductive, in Stlc]
STLC.step_example5_with_normalize [lemma, in Stlc]
STLC.step_example5 [lemma, in Stlc]
STLC.step_example4' [lemma, in Stlc]
STLC.step_example3' [lemma, in Stlc]
STLC.step_example2' [lemma, in Stlc]
STLC.step_example1' [lemma, in Stlc]
STLC.step_example4 [lemma, in Stlc]
STLC.step_example3 [lemma, in Stlc]
STLC.step_example2 [lemma, in Stlc]
STLC.step_example1 [lemma, in Stlc]
STLC.step_sind [definition, in Stlc]
STLC.step_ind [definition, in Stlc]
STLC.ST_If [constructor, in Stlc]
STLC.ST_IfFalse [constructor, in Stlc]
STLC.ST_IfTrue [constructor, in Stlc]
STLC.ST_App2 [constructor, in Stlc]
STLC.ST_App1 [constructor, in Stlc]
STLC.ST_AppAbs [constructor, in Stlc]
STLC.subst [definition, in Stlc]
STLC.substi [inductive, in Stlc]
STLC.substi_correct [lemma, in Stlc]
STLC.substi_sind [definition, in Stlc]
STLC.substi_rec [definition, in Stlc]
STLC.substi_ind [definition, in Stlc]
STLC.substi_rect [definition, in Stlc]
STLC.s_var1 [constructor, in Stlc]
STLC.tm [inductive, in Stlc]
STLC.tm_sind [definition, in Stlc]
STLC.tm_rec [definition, in Stlc]
STLC.tm_ind [definition, in Stlc]
STLC.tm_rect [definition, in Stlc]
STLC.tm_if [constructor, in Stlc]
STLC.tm_false [constructor, in Stlc]
STLC.tm_true [constructor, in Stlc]
STLC.tm_abs [constructor, in Stlc]
STLC.tm_app [constructor, in Stlc]
STLC.tm_var [constructor, in Stlc]
STLC.ty [inductive, in Stlc]
STLC.typing_nonexample_3 [definition, in Stlc]
STLC.typing_nonexample_1 [definition, in Stlc]
STLC.typing_example_3 [definition, in Stlc]
STLC.typing_example_2_full [definition, in Stlc]
STLC.typing_example_2 [definition, in Stlc]
STLC.typing_example_1' [definition, in Stlc]
STLC.typing_example_1 [definition, in Stlc]
STLC.ty_sind [definition, in Stlc]
STLC.ty_rec [definition, in Stlc]
STLC.ty_ind [definition, in Stlc]
STLC.ty_rect [definition, in Stlc]
STLC.Ty_Arrow [constructor, in Stlc]
STLC.Ty_Bool [constructor, in Stlc]
STLC.T_If [constructor, in Stlc]
STLC.T_False [constructor, in Stlc]
STLC.T_True [constructor, in Stlc]
STLC.T_App [constructor, in Stlc]
STLC.T_Abs [constructor, in Stlc]
STLC.T_Var [constructor, in Stlc]
STLC.value [inductive, in Stlc]
STLC.value_sind [definition, in Stlc]
STLC.value_ind [definition, in Stlc]
STLC.v_false [constructor, in Stlc]
STLC.v_true [constructor, in Stlc]
STLC.v_abs [constructor, in Stlc]
STLC.x [definition, in Stlc]
STLC.y [definition, in Stlc]
STLC.z [definition, in Stlc]
stlc_tm:empty (stlc_scope) [notation, in Stlc]
stlc_tm:_ ⊢> _ (stlc_scope) [notation, in Stlc]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [notation, in Stlc]
stlc_tm:[ _ := _ ] _ [notation, in Stlc]
stlc_tm:\ _ : _ , _ [notation, in Stlc]
stlc_tm:_ _ (stlc_scope) [notation, in Stlc]
stlc_tm:( _ ) (stlc_scope) [notation, in Stlc]
stlc_tm:_ (stlc_scope) [notation, in Stlc]
stlc_tm:$( _ ) (stlc_scope) [notation, in Stlc]
stlc_tm:false [notation, in Stlc]
stlc_tm:true [notation, in Stlc]
stlc_tm:if _ then _ else _ [notation, in Stlc]
stlc_ty:Bool (stlc_scope) [notation, in Stlc]
stlc_ty:$( _ ) (stlc_scope) [notation, in Stlc]
stlc_ty:_ -> _ (stlc_scope) [notation, in Stlc]
stlc_ty:( _ ) (stlc_scope) [notation, in Stlc]
stlc_ty:_ (stlc_scope) [notation, in Stlc]
<{ _ |-- _ ∈ _ }> (stlc_scope) [notation, in Stlc]
<{ _ }> (stlc_scope) [notation, in Stlc]
_ -->* _ [notation, in Stlc]
_ --> _ [notation, in Stlc]
false [notation, in Stlc]
true [notation, in Stlc]
<{{ _ }}> [notation, in Stlc]
strong_progress [lemma, in Smallstep]
ST_Plus2 [constructor, in Smallstep]
ST_Plus1 [constructor, in Smallstep]
ST_PlusConstConst [constructor, in Smallstep]
ST_SndPair [constructor, in Norm]
ST_Snd1 [constructor, in Norm]
ST_FstPair [constructor, in Norm]
ST_Fst1 [constructor, in Norm]
ST_Pair2 [constructor, in Norm]
ST_Pair1 [constructor, in Norm]
ST_If [constructor, in Norm]
ST_IfFalse [constructor, in Norm]
ST_IfTrue [constructor, in Norm]
ST_App2 [constructor, in Norm]
ST_App1 [constructor, in Norm]
ST_AppAbs [constructor, in Norm]
Sub [library]
subst [definition, in Norm]
substitution_preserves_typing [lemma, in Norm]
subst_inequiv [lemma, in Equiv]
subst_equiv_property [definition, in Equiv]
subst_aexp_ex [definition, in Equiv]
subst_aexp [definition, in Equiv]
subst_msubst [lemma, in Norm]
subst_not_afi [lemma, in Norm]
subst_closed [lemma, in Norm]
subtract_slowly_outer_triple_valid [lemma, in Hoare2]
subtract_slowly_dec [definition, in Hoare2]
subtype [axiom, in UseAuto]
subtype_trans [axiom, in UseAuto]
subtype_refl [axiom, in UseAuto]
SubtypingInversion [module, in UseAuto]
SubtypingInversion.abs_arrow' [lemma, in UseAuto]
SubtypingInversion.abs_arrow [lemma, in UseAuto]
swap_exercise [lemma, in Hoare]
swap_program [definition, in Hoare]
swap_correct [lemma, in Hoare2]
swap_dec [definition, in Hoare2]
swap_noninterfering_assignments [lemma, in Equiv]
swap_if_branches [lemma, in Equiv]
swap_subst [lemma, in Norm]
sym_cequiv [lemma, in Equiv]
sym_bequiv [lemma, in Equiv]
sym_aequiv [lemma, in Equiv]
T
T [definition, in Hoare2]tass [definition, in Norm]
Temp1 [module, in Smallstep]
Temp1.step [inductive, in Smallstep]
Temp1.step_sind [definition, in Smallstep]
Temp1.step_ind [definition, in Smallstep]
Temp1.ST_Plus2 [constructor, in Smallstep]
Temp1.ST_Plus1 [constructor, in Smallstep]
Temp1.ST_PlusConstConst [constructor, in Smallstep]
Temp1.value [inductive, in Smallstep]
Temp1.value_not_same_as_normal_form [lemma, in Smallstep]
Temp1.value_sind [definition, in Smallstep]
Temp1.value_ind [definition, in Smallstep]
Temp1.v_funny [constructor, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, in Smallstep]
Temp2.step_sind [definition, in Smallstep]
Temp2.step_ind [definition, in Smallstep]
Temp2.ST_Plus2 [constructor, in Smallstep]
Temp2.ST_Plus1 [constructor, in Smallstep]
Temp2.ST_PlusConstConst [constructor, in Smallstep]
Temp2.ST_Funny [constructor, in Smallstep]
Temp2.value [inductive, in Smallstep]
Temp2.value_not_same_as_normal_form [lemma, in Smallstep]
Temp2.value_sind [definition, in Smallstep]
Temp2.value_ind [definition, in Smallstep]
Temp2.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, in Smallstep]
Temp3.step_sind [definition, in Smallstep]
Temp3.step_ind [definition, in Smallstep]
Temp3.ST_Plus1 [constructor, in Smallstep]
Temp3.ST_PlusConstConst [constructor, in Smallstep]
Temp3.value [inductive, in Smallstep]
Temp3.value_not_same_as_normal_form [lemma, in Smallstep]
Temp3.value_sind [definition, in Smallstep]
Temp3.value_ind [definition, in Smallstep]
Temp3.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp4 [module, in Smallstep]
Temp4.bool_step_prop3 [definition, in Smallstep]
Temp4.bool_step_prop2 [definition, in Smallstep]
Temp4.bool_step_prop1 [definition, in Smallstep]
Temp4.fls [constructor, in Smallstep]
Temp4.manual_grade_for_smallstep_bools [definition, in Smallstep]
Temp4.step [inductive, in Smallstep]
Temp4.step_deterministic [lemma, in Smallstep]
Temp4.step_sind [definition, in Smallstep]
Temp4.step_ind [definition, in Smallstep]
Temp4.strong_progress_bool [lemma, in Smallstep]
Temp4.ST_If [constructor, in Smallstep]
Temp4.ST_IfFalse [constructor, in Smallstep]
Temp4.ST_IfTrue [constructor, in Smallstep]
Temp4.Temp5 [module, in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [definition, in Smallstep]
Temp4.Temp5.bool_step_prop4 [definition, in Smallstep]
Temp4.Temp5.manual_grade_for_properties_of_altered_step [definition, in Smallstep]
Temp4.Temp5.step [inductive, in Smallstep]
Temp4.Temp5.step_sind [definition, in Smallstep]
Temp4.Temp5.step_ind [definition, in Smallstep]
Temp4.Temp5.ST_If [constructor, in Smallstep]
Temp4.Temp5.ST_IfFalse [constructor, in Smallstep]
Temp4.Temp5.ST_IfTrue [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp4.test [constructor, in Smallstep]
Temp4.tm [inductive, in Smallstep]
Temp4.tm_sind [definition, in Smallstep]
Temp4.tm_rec [definition, in Smallstep]
Temp4.tm_ind [definition, in Smallstep]
Temp4.tm_rect [definition, in Smallstep]
Temp4.tru [constructor, in Smallstep]
Temp4.value [inductive, in Smallstep]
Temp4.value_sind [definition, in Smallstep]
Temp4.value_ind [definition, in Smallstep]
Temp4.v_fls [constructor, in Smallstep]
Temp4.v_tru [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
test_multistep_4 [lemma, in Smallstep]
test_multistep_3 [lemma, in Smallstep]
test_multistep_2 [lemma, in Smallstep]
test_multistep_1' [lemma, in Smallstep]
test_multistep_1 [lemma, in Smallstep]
test_optimize_0plus [definition, in Equiv]
test_pe_bexp2 [definition, in PE]
test_pe_bexp1 [definition, in PE]
test_pe_update [definition, in PE]
test_pe_aexp1 [definition, in PE]
text_pe_aexp2 [definition, in PE]
tm [inductive, in Smallstep]
TM [module, in Types]
tm [inductive, in Norm]
tm_sind [definition, in Smallstep]
tm_rec [definition, in Smallstep]
tm_ind [definition, in Smallstep]
tm_rect [definition, in Smallstep]
tm_sind [definition, in Norm]
tm_rec [definition, in Norm]
tm_ind [definition, in Norm]
tm_rect [definition, in Norm]
tm_snd [constructor, in Norm]
tm_fst [constructor, in Norm]
tm_pair [constructor, in Norm]
tm_if [constructor, in Norm]
tm_false [constructor, in Norm]
tm_true [constructor, in Norm]
tm_abs [constructor, in Norm]
tm_app [constructor, in Norm]
tm_var [constructor, in Norm]
TM.Bool [constructor, in Types]
TM.bool_canonical [lemma, in Types]
TM.bvalue [inductive, in Types]
TM.bvalue_sind [definition, in Types]
TM.bvalue_ind [definition, in Types]
TM.bv_false [constructor, in Types]
TM.bv_true [constructor, in Types]
TM.fls [constructor, in Types]
TM.has_type_not [definition, in Types]
TM.has_type_1 [definition, in Types]
TM.has_type_sind [definition, in Types]
TM.has_type_ind [definition, in Types]
TM.has_type [inductive, in Types]
TM.iszro [constructor, in Types]
TM.ite [constructor, in Types]
TM.manual_grade_for_prog_pres_bigstep [definition, in Types]
TM.manual_grade_for_remove_pred0 [definition, in Types]
TM.manual_grade_for_variation2 [definition, in Types]
TM.manual_grade_for_variation1 [definition, in Types]
TM.manual_grade_for_finish_preservation_informal [definition, in Types]
TM.manual_grade_for_finish_progress_informal [definition, in Types]
TM.multistep [definition, in Types]
TM.Nat [constructor, in Types]
TM.nat_canonical [lemma, in Types]
TM.nvalue [inductive, in Types]
TM.nvalue_sind [definition, in Types]
TM.nvalue_ind [definition, in Types]
TM.nv_succ [constructor, in Types]
TM.nv_0 [constructor, in Types]
TM.prd [constructor, in Types]
TM.preservation [lemma, in Types]
TM.preservation' [lemma, in Types]
TM.progress [lemma, in Types]
TM.scc [constructor, in Types]
TM.some_term_is_stuck [definition, in Types]
TM.soundness [lemma, in Types]
TM.step [inductive, in Types]
TM.step_deterministic [lemma, in Types]
TM.step_normal_form [abbreviation, in Types]
TM.step_sind [definition, in Types]
TM.step_ind [definition, in Types]
TM.stuck [definition, in Types]
TM.ST_Iszero [constructor, in Types]
TM.ST_IszeroSucc [constructor, in Types]
TM.ST_Iszero0 [constructor, in Types]
TM.ST_Pred [constructor, in Types]
TM.ST_PredSucc [constructor, in Types]
TM.ST_Pred0 [constructor, in Types]
TM.ST_Succ [constructor, in Types]
TM.ST_If [constructor, in Types]
TM.ST_IfFalse [constructor, in Types]
TM.ST_IfTrue [constructor, in Types]
TM.subject_expansion [lemma, in Types]
TM.succ_hastype_nat__hastype_nat [definition, in Types]
TM.tm [inductive, in Types]
TM.tm_sind [definition, in Types]
TM.tm_rec [definition, in Types]
TM.tm_ind [definition, in Types]
TM.tm_rect [definition, in Types]
TM.tru [constructor, in Types]
TM.ty [inductive, in Types]
TM.ty_sind [definition, in Types]
TM.ty_rec [definition, in Types]
TM.ty_ind [definition, in Types]
TM.ty_rect [definition, in Types]
TM.T_Iszero [constructor, in Types]
TM.T_Pred [constructor, in Types]
TM.T_Succ [constructor, in Types]
TM.T_0 [constructor, in Types]
TM.T_If [constructor, in Types]
TM.T_False [constructor, in Types]
TM.T_True [constructor, in Types]
TM.value [definition, in Types]
TM.value_is_nf [lemma, in Types]
TM.zro [constructor, in Types]
tm:if _ then _ else _ (tm_scope) [notation, in Types]
tm:iszero _ (tm_scope) [notation, in Types]
tm:pred _ (tm_scope) [notation, in Types]
tm:succ _ (tm_scope) [notation, in Types]
tm:0 (tm_scope) [notation, in Types]
tm:_ (tm_scope) [notation, in Types]
tm:( _ ) (tm_scope) [notation, in Types]
tm:false (tm_scope) [notation, in Types]
tm:true (tm_scope) [notation, in Types]
0 (tm_scope) [notation, in Types]
<{ _ }> (tm_scope) [notation, in Types]
false (tm_scope) [notation, in Types]
true (tm_scope) [notation, in Types]
_ -->* _ [notation, in Types]
_ --> _ [notation, in Types]
|-- _ ∈ _ [notation, in Types]
transitivity_workaround_2 [lemma, in UseAuto]
transitivity_workaround_1 [lemma, in UseAuto]
transitivity_bad_hint_1 [lemma, in UseAuto]
trans_cequiv [lemma, in Equiv]
trans_bequiv [lemma, in Equiv]
trans_aequiv [lemma, in Equiv]
two_loops [lemma, in Hoare2]
two_loops_dec [definition, in Hoare2]
ty [inductive, in Norm]
typ [axiom, in UseAuto]
typable_empty__closed [lemma, in Norm]
TypecheckerExtensions [module, in Typechecking]
TypecheckerExtensions.eqb_ty__eq [lemma, in Typechecking]
TypecheckerExtensions.eqb_ty_refl [lemma, in Typechecking]
TypecheckerExtensions.eqb_ty [definition, in Typechecking]
TypecheckerExtensions.manual_grade_for_type_check_defn [definition, in Typechecking]
TypecheckerExtensions.type_checking_complete [lemma, in Typechecking]
TypecheckerExtensions.type_checking_sound [lemma, in Typechecking]
TypecheckerExtensions.type_check [definition, in Typechecking]
Typechecking [library]
Types [library]
ty_sind [definition, in Norm]
ty_rec [definition, in Norm]
ty_ind [definition, in Norm]
ty_rect [definition, in Norm]
Ty_Prod [constructor, in Norm]
Ty_Arrow [constructor, in Norm]
Ty_Bool [constructor, in Norm]
T_Snd [constructor, in Norm]
T_Fst [constructor, in Norm]
T_Pair [constructor, in Norm]
T_If [constructor, in Norm]
T_False [constructor, in Norm]
T_True [constructor, in Norm]
T_App [constructor, in Norm]
T_Abs [constructor, in Norm]
T_Var [constructor, in Norm]
U
UnfoldsExample [module, in UseTactics]UnfoldsExample.bexp_eval_true [lemma, in UseTactics]
UseAuto [library]
UseTactics [library]
V
vacuous_substitution [lemma, in Norm]valid [definition, in HoareAsLogic]
valid_hoare_triple [definition, in Hoare]
value [inductive, in Smallstep]
value [inductive, in Norm]
value_is_nf [lemma, in Smallstep]
value_sind [definition, in Smallstep]
value_ind [definition, in Smallstep]
value_halts [lemma, in Norm]
value__normal [lemma, in Norm]
value_sind [definition, in Norm]
value_ind [definition, in Norm]
var_not_used_in_aexp_sind [definition, in Equiv]
var_not_used_in_aexp_ind [definition, in Equiv]
var_not_used_in_aexp [inductive, in Equiv]
vc_dec_while [definition, in Hoare2]
verification_conditions_correct [lemma, in Hoare2]
verification_conditions_from [definition, in Hoare2]
verification_correct [lemma, in Hoare2]
verification_conditions [definition, in Hoare2]
VNUId [constructor, in Equiv]
VNUMinus [constructor, in Equiv]
VNUMult [constructor, in Equiv]
VNUNum [constructor, in Equiv]
VNUPlus [constructor, in Equiv]
v_const [constructor, in Smallstep]
V_cons [constructor, in Norm]
V_nil [constructor, in Norm]
v_pair [constructor, in Norm]
v_false [constructor, in Norm]
v_true [constructor, in Norm]
v_abs [constructor, in Norm]
W
weakening [lemma, in Norm]weakening_empty [lemma, in Norm]
while_example [definition, in Hoare]
while_true [lemma, in Equiv]
while_true_nonterm [lemma, in Equiv]
while_false [lemma, in Equiv]
working_of_auto_2 [lemma, in UseAuto]
working_of_auto_1 [lemma, in UseAuto]
wp [definition, in HoareAsLogic]
wp_invariant [lemma, in HoareAsLogic]
wp_seq [lemma, in HoareAsLogic]
wp_is_weakest [lemma, in HoareAsLogic]
wp_is_precondition [lemma, in HoareAsLogic]
Z
zprop [definition, in Equiv]zprop_preserving [lemma, in Equiv]
other
assn:_ [ _ ⊢> _ ] (assertion_scope) [notation, in Hoare]assn:_ (assertion_scope) [notation, in Hoare]
assn:$ _ (assertion_scope) [notation, in Hoare]
assn:( _ ) (assertion_scope) [notation, in Hoare]
assn:_ * _ (assertion_scope) [notation, in Hoare]
assn:_ - _ (assertion_scope) [notation, in Hoare]
assn:_ + _ (assertion_scope) [notation, in Hoare]
assn:False (assertion_scope) [notation, in Hoare]
assn:True (assertion_scope) [notation, in Hoare]
assn:_ > _ (assertion_scope) [notation, in Hoare]
assn:_ >= _ (assertion_scope) [notation, in Hoare]
assn:_ < _ (assertion_scope) [notation, in Hoare]
assn:_ <= _ (assertion_scope) [notation, in Hoare]
assn:_ <> _ (assertion_scope) [notation, in Hoare]
assn:_ = _ (assertion_scope) [notation, in Hoare]
assn:~ _ (assertion_scope) [notation, in Hoare]
assn:_ /\ _ (assertion_scope) [notation, in Hoare]
assn:_ \/ _ (assertion_scope) [notation, in Hoare]
assn:_ <-> _ (assertion_scope) [notation, in Hoare]
assn:_ -> _ (assertion_scope) [notation, in Hoare]
assn:# _ _ .. _ (assertion_scope) [notation, in Hoare]
com:{{ _ }} _ (dcom_scope) [notation, in Hoare2]
com:_ ; _ (dcom_scope) [notation, in Hoare2]
com:_ ->> {{ _ }} (dcom_scope) [notation, in Hoare2]
com:->> {{ _ }} _ (dcom_scope) [notation, in Hoare2]
com:if _ then {{ _ }} _ else {{ _ }} _ end {{ _ }} (dcom_scope) [notation, in Hoare2]
com:while _ do {{ _ }} _ end {{ _ }} (dcom_scope) [notation, in Hoare2]
com:_ := _ {{ _ }} (dcom_scope) [notation, in Hoare2]
com:skip {{ _ }} (dcom_scope) [notation, in Hoare2]
stlc:_ [notation, in Norm]
stlc:_ .snd [notation, in Norm]
stlc:_ .fst [notation, in Norm]
stlc:_ * _ [notation, in Norm]
stlc:_ _ [notation, in Norm]
stlc:_ -> _ [notation, in Norm]
stlc:Bool [notation, in Norm]
stlc:false [notation, in Norm]
stlc:if _ then _ else _ [notation, in Norm]
stlc:true [notation, in Norm]
stlc:( _ , _ ) [notation, in Norm]
stlc:( _ ) [notation, in Norm]
stlc:[ _ := _ ] _ [notation, in Norm]
stlc:\ _ : _ , _ [notation, in Norm]
stlc:{ _ } [notation, in Norm]
{{ _ }} (assertion_scope) [notation, in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [notation, in Hoare]
_ <<->> _ (hoare_spec_scope) [notation, in Hoare]
_ ->> _ (hoare_spec_scope) [notation, in Hoare]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ _ (ltac_scope) [notation, in LibTactics]
>> _ _ (ltac_scope) [notation, in LibTactics]
>> _ (ltac_scope) [notation, in LibTactics]
>> (ltac_scope) [notation, in LibTactics]
___ (ltac_scope) [notation, in LibTactics]
__ (ltac_scope) [notation, in LibTactics]
_ / _ --> _ / _ [notation, in Smallstep]
_ / _ -->b _ [notation, in Smallstep]
_ / _ -->a _ [notation, in Smallstep]
_ -->* _ [notation, in Smallstep]
_ --> _ [notation, in Smallstep]
_ ==> _ [notation, in Smallstep]
_ <- _ ;; _ [notation, in Typechecking]
_ |-- _ ∈ _ [notation, in Norm]
_ -->* _ [notation, in Norm]
_ --> _ [notation, in Norm]
_ =' _ [notation, in LibTactics]
_ / _ / _ ==> _ [notation, in PE]
_ / _ ==> _ / _ [notation, in PE]
fail [notation, in Typechecking]
False [notation, in Hoare]
false [notation, in Norm]
nosimpl _ [notation, in LibTactics]
Register _ _ [notation, in LibTactics]
return _ [notation, in Typechecking]
Something [notation, in LibTactics]
True [notation, in Hoare]
true [notation, in Norm]
<{ _ }> [notation, in Norm]
Notation Index
C
com:_ ; _ [in Smallstep]com:_ := _ [in Smallstep]
com:_ || _ [in Smallstep]
com:if _ then _ else _ end [in Smallstep]
com:skip [in Smallstep]
com:while _ do _ end [in Smallstep]
_ / _ -->* _ / _ [in Smallstep]
_ / _ --> _ / _ [in Smallstep]
_ --> _ [in Smallstep]
H
com:_ ; _ [in Hoare]com:_ := _ [in Hoare]
com:_ ; _ [in Equiv]
com:_ := _ [in Equiv]
com:havoc _ [in Hoare]
com:havoc _ [in Equiv]
com:if _ then _ else _ end [in Hoare]
com:if _ then _ else _ end [in Equiv]
com:skip [in Hoare]
com:skip [in Equiv]
com:while _ do _ end [in Hoare]
com:while _ do _ end [in Equiv]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
_ =[ _ ]=> _ [in Equiv]
com:_ ; _ [in Hoare]
com:_ := _ [in Hoare]
com:assert _ [in Hoare]
com:assume _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
I
com:_ ; _ [in Hoare]com:_ := _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:if1 _ then _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
L
_ / _ / _ / _ ==> _ # _ [in PE]_ / _ ==> _ # _ [in PE]
_ / _ ==> _ / _ / _ [in PE]
R
stlc_ty:Top [in RecordSub]stlc_ty:nil [in RecordSub]
stlc_ty:_ : _ :: _ [in RecordSub]
stlc_ty:Base _ [in RecordSub]
stlc_ty:_ -> _ [in RecordSub]
stlc_ty:_ [in RecordSub]
stlc_ty:( _ ) [in RecordSub]
stlc:_ [in RecordSub]
stlc:_ --> _ [in RecordSub]
stlc:_ := _ :: _ [in RecordSub]
stlc:_ _ [in RecordSub]
stlc:nil [in RecordSub]
stlc:( _ ) [in RecordSub]
stlc:[ _ := _ ] _ [in RecordSub]
stlc:\ _ : _ , _ [in RecordSub]
stlc:{ _ } [in RecordSub]
_ |-- _ ∈ _ [in RecordSub]
_ <: _ [in RecordSub]
_ --> _ [in RecordSub]
<{ _ }> [in RecordSub]
<{{ _ }}> [in RecordSub]
com:_ ; _ [in Hoare]
com:_ := _ [in Hoare]
com:if _ then _ else _ end [in Hoare]
com:repeat _ until _ end [in Hoare]
com:skip [in Hoare]
com:while _ do _ end [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ =[ _ ]=> _ [in Hoare]
S
_ --> _ [in Smallstep]stlc_tm:if0 _ then _ else _ (stlc_scope) [in StlcProp]
stlc_tm:_ * _ (stlc_scope) [in StlcProp]
stlc_tm:pred _ (stlc_scope) [in StlcProp]
stlc_tm:succ _ (stlc_scope) [in StlcProp]
stlc_ty:Nat [in StlcProp]
stlc_tm:\ _ : _ , _ [in StlcProp]
stlc_tm:_ _ (stlc_scope) [in StlcProp]
stlc_tm:( _ ) (stlc_scope) [in StlcProp]
stlc_tm:_ (stlc_scope) [in StlcProp]
stlc_tm:$( _ ) (stlc_scope) [in StlcProp]
stlc_ty:$( _ ) (stlc_scope) [in StlcProp]
stlc_ty:_ -> _ (stlc_scope) [in StlcProp]
stlc_ty:( _ ) (stlc_scope) [in StlcProp]
<{ _ }> (stlc_scope) [in StlcProp]
_ -->* _ [in StlcProp]
_ --> _ [in StlcProp]
<{ _ |-- _ ∈ _ }> [in StlcProp]
<{{ _ }}> [in StlcProp]
stlc_tm:empty (stlc_scope) [in Records]
stlc_tm:_ ⊢> _ (stlc_scope) [in Records]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [in Records]
stlc_tm:[ _ := _ ] _ [in Records]
stlc_tm:_ --> _ [in Records]
stlc_tm:nil [in Records]
stlc_ty:nil [in Records]
stlc_tm:_ := _ :: _ [in Records]
stlc_ty:_ : _ :: _ [in Records]
stlc_ty:Base _ (stlc_scope) [in Records]
stlc_tm:\ _ : _ , _ [in Records]
stlc_tm:_ _ (stlc_scope) [in Records]
stlc_tm:( _ ) (stlc_scope) [in Records]
stlc_tm:_ (stlc_scope) [in Records]
stlc_tm:$( _ ) (stlc_scope) [in Records]
stlc_ty:$( _ ) (stlc_scope) [in Records]
stlc_ty:_ -> _ (stlc_scope) [in Records]
stlc_ty:( _ ) (stlc_scope) [in Records]
stlc_ty:_ (stlc_scope) [in Records]
<{ _ }> (stlc_scope) [in Records]
_ -->* _ [in Records]
_ --> _ [in Records]
<{ _ |-- _ ∈ _ }> [in Records]
<{{ _ }}> [in Records]
stlc_tm:empty (stlc_scope) [in MoreStlc]
stlc_tm:_ ⊢> _ (stlc_scope) [in MoreStlc]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [in MoreStlc]
stlc_tm:[ _ := _ ] _ (stlc_scope) [in MoreStlc]
stlc_tm:fix _ (stlc_scope) [in MoreStlc]
stlc_tm:let _ = _ in _ (stlc_scope) [in MoreStlc]
stlc_tm:unit (stlc_scope) [in MoreStlc]
stlc_ty:Unit (stlc_scope) [in MoreStlc]
stlc_tm:case _ of | nil => _ | _ :: _ => _ (stlc_scope) [in MoreStlc]
stlc_tm:_ :: _ (stlc_scope) [in MoreStlc]
stlc_tm:nil _ (stlc_scope) [in MoreStlc]
stlc_ty:List _ (stlc_scope) [in MoreStlc]
stlc_tm:_ .snd (stlc_scope) [in MoreStlc]
stlc_tm:_ .fst (stlc_scope) [in MoreStlc]
stlc_tm:( _ , _ ) (stlc_scope) [in MoreStlc]
stlc_ty:_ * _ (stlc_scope) [in MoreStlc]
stlc_tm:case _ of | inl _ => _ | inr _ => _ [in MoreStlc]
stlc_tm:inr _ _ [in MoreStlc]
stlc_tm:inl _ _ [in MoreStlc]
stlc_ty:_ + _ [in MoreStlc]
stlc_tm:if0 _ then _ else _ (stlc_scope) [in MoreStlc]
stlc_tm:_ * _ (stlc_scope) [in MoreStlc]
stlc_tm:pred _ (stlc_scope) [in MoreStlc]
stlc_tm:succ _ (stlc_scope) [in MoreStlc]
stlc_ty:Nat [in MoreStlc]
stlc_tm:\ _ : _ , _ [in MoreStlc]
stlc_tm:_ _ (stlc_scope) [in MoreStlc]
stlc_tm:( _ ) (stlc_scope) [in MoreStlc]
stlc_tm:_ (stlc_scope) [in MoreStlc]
stlc_tm:$( _ ) (stlc_scope) [in MoreStlc]
stlc_ty:$( _ ) (stlc_scope) [in MoreStlc]
stlc_ty:_ -> _ (stlc_scope) [in MoreStlc]
stlc_ty:( _ ) (stlc_scope) [in MoreStlc]
stlc_ty:_ (stlc_scope) [in MoreStlc]
List _ (stlc_scope) [in MoreStlc]
<{ _ }> (stlc_scope) [in MoreStlc]
_ -->* _ [in MoreStlc]
_ --> _ [in MoreStlc]
<{ _ |-- _ ∈ _ }> [in MoreStlc]
<{{ _ }}> [in MoreStlc]
_ / _ -->+ _ / _ [in References]
stlc_tm:empty (stlc_scope) [in References]
stlc_tm:_ ⊢> _ (stlc_scope) [in References]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [in References]
stlc_tm:_ ; _ (stlc_scope) [in References]
stlc_tm:[ _ := _ ] _ (stlc_scope) [in References]
stlc_tm:_ := _ (stlc_scope) [in References]
stlc_tm:! _ (stlc_scope) [in References]
stlc_tm:ref _ (stlc_scope) [in References]
stlc_tm:loc _ (stlc_scope) [in References]
stlc_ty:Ref _ [in References]
stlc_tm:unit (stlc_scope) [in References]
stlc_ty:Unit (stlc_scope) [in References]
stlc_tm:if0 _ then _ else _ (stlc_scope) [in References]
stlc_tm:_ * _ (stlc_scope) [in References]
stlc_tm:pred _ (stlc_scope) [in References]
stlc_tm:succ _ (stlc_scope) [in References]
stlc_ty:Nat [in References]
stlc_tm:\ _ : _ , _ [in References]
stlc_tm:_ _ (stlc_scope) [in References]
stlc_tm:( _ ) (stlc_scope) [in References]
stlc_tm:_ (stlc_scope) [in References]
stlc_tm:$( _ ) (stlc_scope) [in References]
stlc_ty:$( _ ) (stlc_scope) [in References]
stlc_ty:_ -> _ (stlc_scope) [in References]
stlc_ty:( _ ) (stlc_scope) [in References]
stlc_ty:_ (stlc_scope) [in References]
<{ _ }> (stlc_scope) [in References]
_ / _ -->* _ / _ [in References]
_ / _ --> _ / _ [in References]
<{ _ / _ |-- _ ∈ _ }> [in References]
<{{ _ }}> [in References]
stlc_tm:empty (stlc_scope) [in Sub]
stlc_tm:_ ⊢> _ (stlc_scope) [in Sub]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [in Sub]
stlc_tm:[ _ := _ ] _ (stlc_scope) [in Sub]
stlc_ty:Top (stlc_scope) [in Sub]
stlc_tm:_ .snd (stlc_scope) [in Sub]
stlc_tm:_ .fst (stlc_scope) [in Sub]
stlc_tm:( _ , _ ) (stlc_scope) [in Sub]
stlc_ty:_ * _ [in Sub]
stlc_tm:unit (stlc_scope) [in Sub]
stlc_ty:Unit (stlc_scope) [in Sub]
stlc_ty:Base _ (stlc_scope) [in Sub]
stlc_tm:false [in Sub]
stlc_tm:true [in Sub]
stlc_tm:if _ then _ else _ [in Sub]
stlc_ty:Bool (stlc_scope) [in Sub]
stlc_tm:\ _ : _ , _ [in Sub]
stlc_tm:_ _ (stlc_scope) [in Sub]
stlc_tm:( _ ) (stlc_scope) [in Sub]
stlc_tm:_ (stlc_scope) [in Sub]
stlc_tm:$( _ ) (stlc_scope) [in Sub]
stlc_ty:$( _ ) (stlc_scope) [in Sub]
stlc_ty:_ -> _ (stlc_scope) [in Sub]
stlc_ty:( _ ) (stlc_scope) [in Sub]
stlc_ty:_ (stlc_scope) [in Sub]
<{ _ |-- _ ∈ _ }> (stlc_scope) [in Sub]
<{ _ }> (stlc_scope) [in Sub]
_ <: _ [in Sub]
_ --> _ [in Sub]
false [in Sub]
true [in Sub]
<{{ _ }}> [in Sub]
stlc_tm:empty (stlc_scope) [in Stlc]
stlc_tm:_ ⊢> _ (stlc_scope) [in Stlc]
stlc_tm:_ ⊢> _ ; _ (stlc_scope) [in Stlc]
stlc_tm:[ _ := _ ] _ [in Stlc]
stlc_tm:\ _ : _ , _ [in Stlc]
stlc_tm:_ _ (stlc_scope) [in Stlc]
stlc_tm:( _ ) (stlc_scope) [in Stlc]
stlc_tm:_ (stlc_scope) [in Stlc]
stlc_tm:$( _ ) (stlc_scope) [in Stlc]
stlc_tm:false [in Stlc]
stlc_tm:true [in Stlc]
stlc_tm:if _ then _ else _ [in Stlc]
stlc_ty:Bool (stlc_scope) [in Stlc]
stlc_ty:$( _ ) (stlc_scope) [in Stlc]
stlc_ty:_ -> _ (stlc_scope) [in Stlc]
stlc_ty:( _ ) (stlc_scope) [in Stlc]
stlc_ty:_ (stlc_scope) [in Stlc]
<{ _ |-- _ ∈ _ }> (stlc_scope) [in Stlc]
<{ _ }> (stlc_scope) [in Stlc]
_ -->* _ [in Stlc]
_ --> _ [in Stlc]
false [in Stlc]
true [in Stlc]
<{{ _ }}> [in Stlc]
T
_ --> _ [in Smallstep]_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
_ --> _ [in Smallstep]
tm:if _ then _ else _ (tm_scope) [in Types]
tm:iszero _ (tm_scope) [in Types]
tm:pred _ (tm_scope) [in Types]
tm:succ _ (tm_scope) [in Types]
tm:0 (tm_scope) [in Types]
tm:_ (tm_scope) [in Types]
tm:( _ ) (tm_scope) [in Types]
tm:false (tm_scope) [in Types]
tm:true (tm_scope) [in Types]
0 (tm_scope) [in Types]
<{ _ }> (tm_scope) [in Types]
false (tm_scope) [in Types]
true (tm_scope) [in Types]
_ -->* _ [in Types]
_ --> _ [in Types]
|-- _ ∈ _ [in Types]
other
assn:_ [ _ ⊢> _ ] (assertion_scope) [in Hoare]assn:_ (assertion_scope) [in Hoare]
assn:$ _ (assertion_scope) [in Hoare]
assn:( _ ) (assertion_scope) [in Hoare]
assn:_ * _ (assertion_scope) [in Hoare]
assn:_ - _ (assertion_scope) [in Hoare]
assn:_ + _ (assertion_scope) [in Hoare]
assn:False (assertion_scope) [in Hoare]
assn:True (assertion_scope) [in Hoare]
assn:_ > _ (assertion_scope) [in Hoare]
assn:_ >= _ (assertion_scope) [in Hoare]
assn:_ < _ (assertion_scope) [in Hoare]
assn:_ <= _ (assertion_scope) [in Hoare]
assn:_ <> _ (assertion_scope) [in Hoare]
assn:_ = _ (assertion_scope) [in Hoare]
assn:~ _ (assertion_scope) [in Hoare]
assn:_ /\ _ (assertion_scope) [in Hoare]
assn:_ \/ _ (assertion_scope) [in Hoare]
assn:_ <-> _ (assertion_scope) [in Hoare]
assn:_ -> _ (assertion_scope) [in Hoare]
assn:# _ _ .. _ (assertion_scope) [in Hoare]
com:{{ _ }} _ (dcom_scope) [in Hoare2]
com:_ ; _ (dcom_scope) [in Hoare2]
com:_ ->> {{ _ }} (dcom_scope) [in Hoare2]
com:->> {{ _ }} _ (dcom_scope) [in Hoare2]
com:if _ then {{ _ }} _ else {{ _ }} _ end {{ _ }} (dcom_scope) [in Hoare2]
com:while _ do {{ _ }} _ end {{ _ }} (dcom_scope) [in Hoare2]
com:_ := _ {{ _ }} (dcom_scope) [in Hoare2]
com:skip {{ _ }} (dcom_scope) [in Hoare2]
stlc:_ [in Norm]
stlc:_ .snd [in Norm]
stlc:_ .fst [in Norm]
stlc:_ * _ [in Norm]
stlc:_ _ [in Norm]
stlc:_ -> _ [in Norm]
stlc:Bool [in Norm]
stlc:false [in Norm]
stlc:if _ then _ else _ [in Norm]
stlc:true [in Norm]
stlc:( _ , _ ) [in Norm]
stlc:( _ ) [in Norm]
stlc:[ _ := _ ] _ [in Norm]
stlc:\ _ : _ , _ [in Norm]
stlc:{ _ } [in Norm]
{{ _ }} (assertion_scope) [in Hoare]
{{ _ }} _ {{ _ }} (hoare_spec_scope) [in Hoare]
_ <<->> _ (hoare_spec_scope) [in Hoare]
_ ->> _ (hoare_spec_scope) [in Hoare]
>> _ _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ _ (ltac_scope) [in LibTactics]
>> _ _ _ (ltac_scope) [in LibTactics]
>> _ _ (ltac_scope) [in LibTactics]
>> _ (ltac_scope) [in LibTactics]
>> (ltac_scope) [in LibTactics]
___ (ltac_scope) [in LibTactics]
__ (ltac_scope) [in LibTactics]
_ / _ --> _ / _ [in Smallstep]
_ / _ -->b _ [in Smallstep]
_ / _ -->a _ [in Smallstep]
_ -->* _ [in Smallstep]
_ --> _ [in Smallstep]
_ ==> _ [in Smallstep]
_ <- _ ;; _ [in Typechecking]
_ |-- _ ∈ _ [in Norm]
_ -->* _ [in Norm]
_ --> _ [in Norm]
_ =' _ [in LibTactics]
_ / _ / _ ==> _ [in PE]
_ / _ ==> _ / _ [in PE]
fail [in Typechecking]
False [in Hoare]
false [in Norm]
nosimpl _ [in LibTactics]
Register _ _ [in LibTactics]
return _ [in Typechecking]
Something [in LibTactics]
True [in Hoare]
true [in Norm]
<{ _ }> [in Norm]
Module Index
C
CImp [in Smallstep]Combined [in Smallstep]
D
DComFirstTry [in Hoare2]DeterministicImp [in UseAuto]
E
EqualityExamples [in UseTactics]ExampleAssertionSub [in Hoare]
ExamplePrettyAssertions [in Hoare]
ExamplesLets [in UseTactics]
ExAssertions [in Hoare]
F
FirstTry [in Typechecking]G
GenExample [in UseTactics]H
Himp [in Hoare]Himp [in Equiv]
Himp2 [in Hoare2]
HoareAssertAssume [in Hoare]
I
If1 [in Hoare]IntrovExamples [in UseTactics]
InvertsExamples [in UseTactics]
InvertsExamples1 [in UseTactics]
L
LibTacticsCompatibility [in LibTactics]Loop [in PE]
N
NaryExamples [in UseTactics]P
PreservationProgressReferences [in UseAuto]PreservationProgressStlc [in UseAuto]
R
RecordSub [in RecordSub]RecordSub.Examples [in RecordSub]
RecordSub.Examples2 [in RecordSub]
RepeatExercise [in Hoare]
RingDemo [in UseAuto]
S
Semantics [in UseAuto]SimpleArith1 [in Smallstep]
SimpleArith2 [in Smallstep]
SimpleArith3 [in Smallstep]
SkipExample [in UseTactics]
SortExamples [in UseTactics]
StepFunction [in Typechecking]
STLC [in Stlc]
STLCArith [in StlcProp]
STLCChecker [in Typechecking]
STLCExtended [in MoreStlc]
STLCExtendedRecords [in Records]
STLCExtendedRecords.FirstTry [in Records]
STLCExtended.Examples [in MoreStlc]
STLCExtended.Examples.FixTest1 [in MoreStlc]
STLCExtended.Examples.FixTest2 [in MoreStlc]
STLCExtended.Examples.FixTest3 [in MoreStlc]
STLCExtended.Examples.FixTest4 [in MoreStlc]
STLCExtended.Examples.LetTest [in MoreStlc]
STLCExtended.Examples.LetTest1 [in MoreStlc]
STLCExtended.Examples.ListTest [in MoreStlc]
STLCExtended.Examples.Numtest [in MoreStlc]
STLCExtended.Examples.ProdTest [in MoreStlc]
STLCExtended.Examples.Sumtest1 [in MoreStlc]
STLCExtended.Examples.Sumtest2 [in MoreStlc]
StlcImpl [in Typechecking]
STLCProp [in StlcProp]
STLCRef [in References]
STLCRef.ExampleVariables [in References]
STLCRef.RefsAndNontermination [in References]
STLCSub [in Sub]
STLCSub.Examples [in Sub]
STLCSub.Examples2 [in Sub]
STLCSub.FormalThoughtExercises [in Sub]
STLCTypes [in Typechecking]
SubtypingInversion [in UseAuto]
T
Temp1 [in Smallstep]Temp2 [in Smallstep]
Temp3 [in Smallstep]
Temp4 [in Smallstep]
Temp4.Temp5 [in Smallstep]
TM [in Types]
TypecheckerExtensions [in Typechecking]
U
UnfoldsExample [in UseTactics]Variable Index
E
equatesLemma.A0 [in LibTactics]equatesLemma.A1 [in LibTactics]
equatesLemma.A2 [in LibTactics]
equatesLemma.A3 [in LibTactics]
equatesLemma.A4 [in LibTactics]
equatesLemma.A5 [in LibTactics]
equatesLemma.A6 [in LibTactics]
F
FuncEq.A1 [in LibTactics]FuncEq.A2 [in LibTactics]
FuncEq.A3 [in LibTactics]
FuncEq.A4 [in LibTactics]
FuncEq.A5 [in LibTactics]
FuncEq.A6 [in LibTactics]
FuncEq.A7 [in LibTactics]
FuncEq.B [in LibTactics]
Library Index
B
BibE
EquivH
HoareHoareAsLogic
Hoare2
L
LibTacticsM
MoreStlcN
NormP
PEPostscript
Preface
R
RecordsRecordSub
References
S
SmallstepStlc
StlcProp
Sub
T
TypecheckingTypes
U
UseAutoUseTactics
Lemma Index
A
aequiv_example [in Equiv]aeval_weakening [in Equiv]
always_loop_hoare [in Hoare]
applys_eq_step [in LibTactics]
applys_eq_step_dep [in LibTactics]
applys_eq_init [in LibTactics]
args_eq_7 [in LibTactics]
args_eq_6 [in LibTactics]
args_eq_5 [in LibTactics]
args_eq_4 [in LibTactics]
args_eq_3 [in LibTactics]
args_eq_2 [in LibTactics]
args_eq_1 [in LibTactics]
assign_aequiv [in Equiv]
assign_removes [in PE]
B
bequiv_example [in Equiv]bexp_eval_false [in Hoare]
C
CAsgn_congruence [in Equiv]ceval_extensionality [in PE]
CIf_congruence [in Equiv]
CImp.par_loop_any_X [in Smallstep]
CImp.par_body_n [in Smallstep]
CImp.par_body_n__Sn [in Smallstep]
cmin_minimal [in Equiv]
Combined.combined_strong_progress [in Smallstep]
Combined.combined_step_deterministic [in Smallstep]
compiler_is_correct [in Smallstep]
congruence_demo_3 [in UseAuto]
congruence_demo_4 [in UseAuto]
congruence_demo_2 [in UseAuto]
congruence_demo_1 [in UseAuto]
context_invariance [in Norm]
CSeq_congruence [in Equiv]
CWhile_congruence [in Equiv]
c3_c4_different [in Equiv]
D
dec_while_correct [in Hoare2]demo_false [in UseAuto]
demo_auto_absurd_2 [in UseAuto]
demo_auto_absurd_1 [in UseAuto]
demo_hint_unfold_context_2 [in UseAuto]
demo_hint_unfold_context_1 [in UseAuto]
demo_hint_unfold_goal_2 [in UseAuto]
demo_hint_unfold_goal_1 [in UseAuto]
demo_tryfalse [in UseTactics]
demo_false_arg [in UseTactics]
demo_false [in UseTactics]
demo_clears_all_and_clears_but [in LibTactics]
DeterministicImp.ceval_deterministic'''' [in UseAuto]
DeterministicImp.ceval_deterministic''' [in UseAuto]
DeterministicImp.ceval_deterministic'' [in UseAuto]
DeterministicImp.ceval_deterministic' [in UseAuto]
DeterministicImp.ceval_deterministic [in UseAuto]
dfib_correct [in Hoare2]
div_mod_outer_triple_valid [in Hoare2]
dpow2_down_correct [in Hoare2]
duplicate_subst [in Norm]
dup_lemma [in LibTactics]
E
EqualityExamples.demo_applys_eq_2 [in UseTactics]EqualityExamples.demo_applys_eq_1 [in UseTactics]
EqualityExamples.demo_fequals [in UseTactics]
EqualityExamples.demo_substs [in UseTactics]
EqualityExamples.mult_0_plus'' [in UseTactics]
EqualityExamples.mult_0_plus [in UseTactics]
equality_by_auto [in UseAuto]
equates_6 [in LibTactics]
equates_5 [in LibTactics]
equates_4 [in LibTactics]
equates_3 [in LibTactics]
equates_2 [in LibTactics]
equates_1 [in LibTactics]
equates_0 [in LibTactics]
evalF_eval [in Smallstep]
eval__multistep [in Smallstep]
eval_assign [in PE]
ExamplesLets.demo_lets_underscore [in UseTactics]
ExamplesLets.demo_lets_5 [in UseTactics]
ExamplesLets.demo_lets_4 [in UseTactics]
ExamplesLets.demo_lets_3 [in UseTactics]
ExamplesLets.demo_lets_2 [in UseTactics]
ExamplesLets.demo_lets_1 [in UseTactics]
F
factorial_correct [in Hoare2]false_eqb_string [in Norm]
false_eqb_string [in PE]
fib_eqn [in Hoare2]
fold_constants_com_sound [in Equiv]
fold_constants_bexp_sound [in Equiv]
fold_constants_aexp_sound [in Equiv]
free_in_context [in Norm]
G
GenExample.substitution_preserves_typing [in UseTactics]H
Himp.havoc_post [in Hoare]Himp.hoare_havoc [in Hoare]
Himp.hoare_consequence_pre [in Hoare]
Himp.ptwice_cequiv_pcopy [in Equiv]
Himp.pXY_cequiv_pYX [in Equiv]
Himp.p1_p2_equiv [in Equiv]
Himp.p1_may_diverge [in Equiv]
Himp.p2_may_diverge [in Equiv]
Himp.p3_p4_inequiv [in Equiv]
Himp.p5_p6_equiv [in Equiv]
Himp2.hoare_havoc_weakest [in Hoare2]
HoareAssertAssume.assert_implies_assume [in Hoare]
HoareAssertAssume.assert_assume_differ [in Hoare]
HoareAssertAssume.hoare_while [in Hoare]
HoareAssertAssume.hoare_if [in Hoare]
HoareAssertAssume.hoare_skip [in Hoare]
HoareAssertAssume.hoare_seq [in Hoare]
HoareAssertAssume.hoare_consequence_post [in Hoare]
HoareAssertAssume.hoare_consequence_pre [in Hoare]
HoareAssertAssume.hoare_asgn [in Hoare]
hoare_while [in Hoare]
hoare_if [in Hoare]
hoare_consequence_post' [in Hoare]
hoare_consequence_pre'''' [in Hoare]
hoare_consequence_pre''' [in Hoare]
hoare_consequence_pre'' [in Hoare]
hoare_consequence_pre' [in Hoare]
hoare_consequence [in Hoare]
hoare_consequence_post [in Hoare]
hoare_consequence_pre [in Hoare]
hoare_asgn_fwd_exists [in Hoare]
hoare_asgn_fwd [in Hoare]
hoare_asgn_wrong [in Hoare]
hoare_asgn [in Hoare]
hoare_seq [in Hoare]
hoare_skip [in Hoare]
hoare_pre_false [in Hoare]
hoare_post_true [in Hoare]
hoare_asgn_weakest [in Hoare2]
hoare_complete [in HoareAsLogic]
hoare_sound [in HoareAsLogic]
H_Consequence_post [in HoareAsLogic]
H_Consequence_pre [in HoareAsLogic]
I
identity_assignment [in Equiv]iff_intro_swap [in LibTactics]
if_minus_plus [in Hoare]
if_minus_plus_correct [in Hoare2]
if_false [in Equiv]
if_true [in Equiv]
if_true_simple [in Equiv]
If1.hoare_if1_good [in Hoare]
If1.hoare_asgn [in Hoare]
If1.hoare_consequence_pre [in Hoare]
inbP [in PE]
induct_height_max2 [in LibTactics]
inequiv_exercise [in Equiv]
instantiation_drop [in Norm]
instantiation_R [in Norm]
instantiation_env_closed [in Norm]
instantiation_domains_match [in Norm]
IntrovExamples.ceval_deterministic' [in UseTactics]
IntrovExamples.ceval_deterministic [in UseTactics]
IntrovExamples.dist_exists_or [in UseTactics]
IntrovExamples.exists_impl [in UseTactics]
invalid_triple [in Hoare]
InvertsExamples.ceval_deterministic' [in UseTactics]
InvertsExamples.ceval_deterministic [in UseTactics]
InvertsExamples.skip_left' [in UseTactics]
InvertsExamples.skip_left [in UseTactics]
is_wp_example [in Hoare2]
L
lia_demo_4 [in UseAuto]lia_demo_3 [in UseAuto]
lia_demo_2 [in UseAuto]
lia_demo_1 [in UseAuto]
loop_unrolling [in Equiv]
Loop.ceval_count_sound [in PE]
Loop.ceval_count_complete [in PE]
Loop.pe_com_correct [in PE]
Loop.pe_com_sound [in PE]
Loop.pe_com_complete [in PE]
Loop.pe_ceval_count_le [in PE]
Loop.pe_compare_nil_update [in PE]
Loop.pe_compare_nil_lookup [in PE]
ltac_something_show [in LibTactics]
ltac_something_hide [in LibTactics]
ltac_something_eq [in LibTactics]
ltac_database_provide [in LibTactics]
M
minimum_correct [in Hoare2]msubst_R [in Norm]
msubst_preserves_typing [in Norm]
msubst_app [in Norm]
msubst_abs [in Norm]
msubst_var [in Norm]
msubst_closed [in Norm]
multistep__eval [in Smallstep]
multistep_congr_2 [in Smallstep]
multistep_congr_1 [in Smallstep]
multistep_App2 [in Norm]
multistep_preserves_R' [in Norm]
multistep_preserves_R [in Norm]
multi_trans [in Smallstep]
multi_R [in Smallstep]
mupdate_drop [in Norm]
mupdate_lookup [in Norm]
N
NaryExamples.demo_branch [in UseTactics]NaryExamples.demo_splits [in UseTactics]
nat_le_refl [in UseAuto]
negation_study_2 [in UseAuto]
negation_study_1 [in UseAuto]
nf_same_as_value [in Smallstep]
nf_is_value [in Smallstep]
normalization [in Norm]
normalize_ex' [in Smallstep]
normalize_ex [in Smallstep]
normal_forms_unique [in Smallstep]
O
optimizer_sound [in Equiv]optimize_0plus_com_sound [in Equiv]
optimize_0plus_bexp_sound [in Equiv]
optimize_0plus_aexp_sound [in Equiv]
order_matters_2 [in UseAuto]
order_matters_1 [in UseAuto]
P
parity_outer_triple_valid [in Hoare2]parity_lt_2 [in Hoare2]
parity_ge_2 [in Hoare2]
pe_program_correct [in PE]
pe_block_correct [in PE]
pe_com_correct [in PE]
pe_com_sound [in PE]
pe_com_complete [in PE]
pe_compare_update [in PE]
pe_compare_removes [in PE]
pe_removes_correct [in PE]
pe_compare_correct [in PE]
pe_unique_correct [in PE]
pe_disagree_domain [in PE]
pe_update_update_add [in PE]
pe_update_update_remove [in PE]
pe_add_correct [in PE]
pe_remove_correct [in PE]
pe_bexp_correct [in PE]
pe_aexp_correct [in PE]
pe_consistent_update [in PE]
pe_update_consistent [in PE]
pe_update_correct [in PE]
pe_aexp_correct_weak [in PE]
pe_domain [in PE]
positive_difference_correct [in Hoare2]
pow2_le_1 [in Hoare2]
pow2_plus_1 [in Hoare2]
preservation [in Norm]
PreservationProgressReferences.nth_eq_last' [in UseAuto]
PreservationProgressReferences.preservation [in UseAuto]
PreservationProgressReferences.preservation_ref [in UseAuto]
PreservationProgressReferences.preservation' [in UseAuto]
PreservationProgressReferences.progress [in UseAuto]
PreservationProgressStlc.preservation [in UseAuto]
PreservationProgressStlc.preservation' [in UseAuto]
PreservationProgressStlc.progress [in UseAuto]
PreservationProgressStlc.progress' [in UseAuto]
provable_false_pre [in HoareAsLogic]
provable_true_post [in HoareAsLogic]
R
RecordSub.abs_arrow [in RecordSub]RecordSub.canonical_forms_of_arrow_types [in RecordSub]
RecordSub.has_type__wf [in RecordSub]
RecordSub.lookup_field_in_value [in RecordSub]
RecordSub.preservation [in RecordSub]
RecordSub.progress [in RecordSub]
RecordSub.rcd_types_match [in RecordSub]
RecordSub.step_preserves_record_tm [in RecordSub]
RecordSub.substitution_preserves_typing [in RecordSub]
RecordSub.subtype__wf [in RecordSub]
RecordSub.sub_inversion_arrow [in RecordSub]
RecordSub.typing_inversion_abs [in RecordSub]
RecordSub.weakening [in RecordSub]
RecordSub.weakening_empty [in RecordSub]
RecordSub.wf_rcd_lookup [in RecordSub]
reduce_to_zero_correct''' [in Hoare2]
reduce_to_zero_correct' [in Hoare2]
refl_cequiv [in Equiv]
refl_bequiv [in Equiv]
refl_aequiv [in Equiv]
RepeatExercise.ex1_repeat_works [in Hoare]
RingDemo.ring_demo [in UseAuto]
R_typable_empty [in Norm]
R_halts [in Norm]
S
search_depth_5 [in UseAuto]search_depth_4 [in UseAuto]
search_depth_3 [in UseAuto]
search_depth_1 [in UseAuto]
search_depth_0 [in UseAuto]
Semantics.multistep__eval'' [in UseAuto]
Semantics.multistep__eval' [in UseAuto]
Semantics.multistep_eval_ind [in UseAuto]
Semantics.multistep__eval [in UseAuto]
seq_assoc [in Equiv]
SimpleArith2.step_deterministic [in Smallstep]
SimpleArith3.step_deterministic_alt [in Smallstep]
SkipExample.ceval_deterministic [in UseTactics]
SkipExample.demo_admits [in UseTactics]
SkipExample.mult_plus_0 [in UseTactics]
skip_right [in Equiv]
skip_left [in Equiv]
slow_assignment [in Hoare2]
solved_by_jauto [in UseAuto]
solving_by_symmetry [in UseAuto]
solving_exists_hyp [in UseAuto]
solving_exists_goal [in UseAuto]
solving_tauto [in UseAuto]
solving_disj_hyp [in UseAuto]
solving_disj_goal [in UseAuto]
solving_conj_hyp_forall [in UseAuto]
solving_conj_more [in UseAuto]
solving_conj_hyp' [in UseAuto]
solving_conj_hyp [in UseAuto]
solving_conj_goal [in UseAuto]
solving_by_eapply [in UseAuto]
solving_by_apply [in UseAuto]
solving_by_reflexivity [in UseAuto]
SortExamples.ceval_deterministic [in UseTactics]
sqrt_correct [in Hoare2]
stack_step_deterministic [in Smallstep]
StepFunction.complete_stepf [in Typechecking]
StepFunction.complete_valuef [in Typechecking]
StepFunction.sound_stepf [in Typechecking]
StepFunction.sound_valuef [in Typechecking]
StepFunction.value_stepf_nf [in Typechecking]
step__eval [in Smallstep]
step_normalizing [in Smallstep]
step_deterministic [in Smallstep]
step_preserves_R' [in Norm]
step_preserves_R [in Norm]
step_preserves_halting [in Norm]
step_deterministic [in Norm]
STLCArith.preservation [in StlcProp]
STLCArith.progress [in StlcProp]
STLCArith.weakening [in StlcProp]
STLCChecker.type_checking_complete [in Typechecking]
STLCChecker.type_checking_sound [in Typechecking]
STLCExtendedRecords.has_type__wf [in Records]
STLCExtendedRecords.lookup_field_in_value [in Records]
STLCExtendedRecords.preservation [in Records]
STLCExtendedRecords.progress [in Records]
STLCExtendedRecords.step_preserves_record_tm [in Records]
STLCExtendedRecords.substitution_preserves_typing [in Records]
STLCExtendedRecords.typing_example_2 [in Records]
STLCExtendedRecords.weakening [in Records]
STLCExtendedRecords.weakening_empty [in Records]
STLCExtendedRecords.wf_rcd_lookup [in Records]
STLCExtendedRecords.wf_ty_example [in Records]
STLCExtended.preservation [in MoreStlc]
STLCExtended.progress [in MoreStlc]
STLCExtended.substitution_preserves_typing [in MoreStlc]
STLCExtended.weakening [in MoreStlc]
STLCExtended.weakening_empty [in MoreStlc]
STLCProp.canonical_forms_fun [in StlcProp]
STLCProp.canonical_forms_bool [in StlcProp]
STLCProp.context_invariance [in StlcProp]
STLCProp.free_in_context [in StlcProp]
STLCProp.not_subject_expansion [in StlcProp]
STLCProp.preservation [in StlcProp]
STLCProp.progress [in StlcProp]
STLCProp.progress' [in StlcProp]
STLCProp.substitution_preserves_typing_from_typing_ind [in StlcProp]
STLCProp.substitution_preserves_typing [in StlcProp]
STLCProp.typable_empty__closed [in StlcProp]
STLCProp.type_soundness [in StlcProp]
STLCProp.unique_types [in StlcProp]
STLCProp.weakening [in StlcProp]
STLCProp.weakening_empty [in StlcProp]
STLCRef.assign_pres_store_typing [in References]
STLCRef.cyclic_store [in References]
STLCRef.extends_refl [in References]
STLCRef.extends_app [in References]
STLCRef.extends_lookup [in References]
STLCRef.length_extends [in References]
STLCRef.length_replace [in References]
STLCRef.lookup_replace_neq [in References]
STLCRef.lookup_replace_eq [in References]
STLCRef.nth_eq_last [in References]
STLCRef.preservation [in References]
STLCRef.preservation_wrong2 [in References]
STLCRef.preservation_wrong1 [in References]
STLCRef.progress [in References]
STLCRef.RefsAndNontermination.factorial_type [in References]
STLCRef.RefsAndNontermination.loop_fun_step_self [in References]
STLCRef.RefsAndNontermination.loop_steps_to_loop_fun [in References]
STLCRef.RefsAndNontermination.loop_typeable [in References]
STLCRef.replace_nil [in References]
STLCRef.store_well_typed_app [in References]
STLCRef.store_weakening [in References]
STLCRef.store_not_unique [in References]
STLCRef.substitution_preserves_typing [in References]
STLCRef.weakening [in References]
STLCRef.weakening_empty [in References]
STLCSub.abs_arrow [in Sub]
STLCSub.canonical_forms_of_Bool [in Sub]
STLCSub.canonical_forms_of_arrow_types [in Sub]
STLCSub.FormalThoughtExercises.formal_proper_subtypes [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfh [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfg [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tff [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfe [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfd [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfc [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfb [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_concepts_tfa [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2e [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2d [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2b [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_2a [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1g [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1f [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1e [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1d [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1c [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1b [in Sub]
STLCSub.FormalThoughtExercises.formal_subtype_instances_tf_1a [in Sub]
STLCSub.preservation [in Sub]
STLCSub.progress [in Sub]
STLCSub.substitution_preserves_typing [in Sub]
STLCSub.sub_inversion_Top [in Sub]
STLCSub.sub_inversion_Base [in Sub]
STLCSub.sub_inversion_Unit [in Sub]
STLCSub.sub_inversion_arrow [in Sub]
STLCSub.sub_inversion_Bool [in Sub]
STLCSub.typing_inversion_unit [in Sub]
STLCSub.typing_inversion_app [in Sub]
STLCSub.typing_inversion_var [in Sub]
STLCSub.typing_inversion_abs [in Sub]
STLCSub.weakening [in Sub]
STLCSub.weakening_empty [in Sub]
STLCTypes.eqb_ty__eq [in Typechecking]
STLCTypes.eqb_ty_refl [in Typechecking]
STLC.step_example5_with_normalize [in Stlc]
STLC.step_example5 [in Stlc]
STLC.step_example4' [in Stlc]
STLC.step_example3' [in Stlc]
STLC.step_example2' [in Stlc]
STLC.step_example1' [in Stlc]
STLC.step_example4 [in Stlc]
STLC.step_example3 [in Stlc]
STLC.step_example2 [in Stlc]
STLC.step_example1 [in Stlc]
STLC.substi_correct [in Stlc]
strong_progress [in Smallstep]
substitution_preserves_typing [in Norm]
subst_inequiv [in Equiv]
subst_msubst [in Norm]
subst_not_afi [in Norm]
subst_closed [in Norm]
subtract_slowly_outer_triple_valid [in Hoare2]
SubtypingInversion.abs_arrow' [in UseAuto]
SubtypingInversion.abs_arrow [in UseAuto]
swap_exercise [in Hoare]
swap_correct [in Hoare2]
swap_noninterfering_assignments [in Equiv]
swap_if_branches [in Equiv]
swap_subst [in Norm]
sym_cequiv [in Equiv]
sym_bequiv [in Equiv]
sym_aequiv [in Equiv]
T
Temp1.value_not_same_as_normal_form [in Smallstep]Temp2.value_not_same_as_normal_form [in Smallstep]
Temp3.value_not_same_as_normal_form [in Smallstep]
Temp4.step_deterministic [in Smallstep]
Temp4.strong_progress_bool [in Smallstep]
test_multistep_4 [in Smallstep]
test_multistep_3 [in Smallstep]
test_multistep_2 [in Smallstep]
test_multistep_1' [in Smallstep]
test_multistep_1 [in Smallstep]
TM.bool_canonical [in Types]
TM.nat_canonical [in Types]
TM.preservation [in Types]
TM.preservation' [in Types]
TM.progress [in Types]
TM.soundness [in Types]
TM.step_deterministic [in Types]
TM.subject_expansion [in Types]
TM.value_is_nf [in Types]
transitivity_workaround_2 [in UseAuto]
transitivity_workaround_1 [in UseAuto]
transitivity_bad_hint_1 [in UseAuto]
trans_cequiv [in Equiv]
trans_bequiv [in Equiv]
trans_aequiv [in Equiv]
two_loops [in Hoare2]
typable_empty__closed [in Norm]
TypecheckerExtensions.eqb_ty__eq [in Typechecking]
TypecheckerExtensions.eqb_ty_refl [in Typechecking]
TypecheckerExtensions.type_checking_complete [in Typechecking]
TypecheckerExtensions.type_checking_sound [in Typechecking]
U
UnfoldsExample.bexp_eval_true [in UseTactics]V
vacuous_substitution [in Norm]value_is_nf [in Smallstep]
value_halts [in Norm]
value__normal [in Norm]
verification_conditions_correct [in Hoare2]
verification_correct [in Hoare2]
W
weakening [in Norm]weakening_empty [in Norm]
while_true [in Equiv]
while_true_nonterm [in Equiv]
while_false [in Equiv]
working_of_auto_2 [in UseAuto]
working_of_auto_1 [in UseAuto]
wp_invariant [in HoareAsLogic]
wp_seq [in HoareAsLogic]
wp_is_weakest [in HoareAsLogic]
wp_is_precondition [in HoareAsLogic]
Z
zprop_preserving [in Equiv]Constructor Index
A
afi_snd [in Norm]afi_fst [in Norm]
afi_pair2 [in Norm]
afi_pair1 [in Norm]
afi_test2 [in Norm]
afi_test1 [in Norm]
afi_test0 [in Norm]
afi_abs [in Norm]
afi_app2 [in Norm]
afi_app1 [in Norm]
afi_var [in Norm]
Assign [in PE]
AS_Mult [in Smallstep]
AS_Mult2 [in Smallstep]
AS_Mult1 [in Smallstep]
AS_Minus [in Smallstep]
AS_Minus2 [in Smallstep]
AS_Minus1 [in Smallstep]
AS_Plus [in Smallstep]
AS_Plus2 [in Smallstep]
AS_Plus1 [in Smallstep]
AS_Id [in Smallstep]
av_num [in Smallstep]
B
body [in PE]boxer [in LibTactics]
BS_AndTrueFalse [in Smallstep]
BS_AndTrueTrue [in Smallstep]
BS_AndFalse [in Smallstep]
BS_AndTrueStep [in Smallstep]
BS_AndStep [in Smallstep]
BS_NotFalse [in Smallstep]
BS_NotTrue [in Smallstep]
BS_NotStep [in Smallstep]
BS_LtEq [in Smallstep]
BS_LtEq2 [in Smallstep]
BS_LtEq1 [in Smallstep]
BS_Eq [in Smallstep]
BS_Eq2 [in Smallstep]
BS_Eq1 [in Smallstep]
C
C [in Smallstep]CImp.CAsgn [in Smallstep]
CImp.CIf [in Smallstep]
CImp.CPar [in Smallstep]
CImp.CSeq [in Smallstep]
CImp.CSkip [in Smallstep]
CImp.CS_ParDone [in Smallstep]
CImp.CS_Par2 [in Smallstep]
CImp.CS_Par1 [in Smallstep]
CImp.CS_While [in Smallstep]
CImp.CS_IfFalse [in Smallstep]
CImp.CS_IfTrue [in Smallstep]
CImp.CS_IfStep [in Smallstep]
CImp.CS_SeqFinish [in Smallstep]
CImp.CS_SeqStep [in Smallstep]
CImp.CS_Asgn [in Smallstep]
CImp.CS_AsgnStep [in Smallstep]
CImp.CWhile [in Smallstep]
Combined.C [in Smallstep]
Combined.fls [in Smallstep]
Combined.P [in Smallstep]
Combined.ST_If [in Smallstep]
Combined.ST_IfFalse [in Smallstep]
Combined.ST_IfTrue [in Smallstep]
Combined.ST_Plus2 [in Smallstep]
Combined.ST_Plus1 [in Smallstep]
Combined.ST_PlusConstConst [in Smallstep]
Combined.test [in Smallstep]
Combined.tru [in Smallstep]
Combined.v_fls [in Smallstep]
Combined.v_tru [in Smallstep]
Combined.v_const [in Smallstep]
CS_While [in Smallstep]
CS_IfFalse [in Smallstep]
CS_IfTrue [in Smallstep]
CS_IfStep [in Smallstep]
CS_SeqFinish [in Smallstep]
CS_SeqStep [in Smallstep]
CS_Asgn [in Smallstep]
CS_AsgnStep [in Smallstep]
D
DCAsgn [in Hoare2]DCIf [in Hoare2]
DComFirstTry.DCAsgn [in Hoare2]
DComFirstTry.DCIf [in Hoare2]
DComFirstTry.DCPost [in Hoare2]
DComFirstTry.DCPre [in Hoare2]
DComFirstTry.DCSeq [in Hoare2]
DComFirstTry.DCSkip [in Hoare2]
DComFirstTry.DCWhile [in Hoare2]
DCPost [in Hoare2]
DCPre [in Hoare2]
DCSeq [in Hoare2]
DCSkip [in Hoare2]
DCWhile [in Hoare2]
Decorated [in Hoare2]
done [in PE]
E
entry [in PE]E_Plus [in Smallstep]
E_Const [in Smallstep]
E_Some [in PE]
E_None [in PE]
G
Goto [in PE]H
Himp.CAsgn [in Hoare]Himp.CAsgn [in Equiv]
Himp.CHavoc [in Hoare]
Himp.CHavoc [in Equiv]
Himp.CIf [in Hoare]
Himp.CIf [in Equiv]
Himp.CSeq [in Hoare]
Himp.CSeq [in Equiv]
Himp.CSkip [in Hoare]
Himp.CSkip [in Equiv]
Himp.CWhile [in Hoare]
Himp.CWhile [in Equiv]
Himp.E_Havoc [in Hoare]
Himp.E_WhileTrue [in Hoare]
Himp.E_WhileFalse [in Hoare]
Himp.E_IfFalse [in Hoare]
Himp.E_IfTrue [in Hoare]
Himp.E_Seq [in Hoare]
Himp.E_Asgn [in Hoare]
Himp.E_Skip [in Hoare]
Himp.E_WhileTrue [in Equiv]
Himp.E_WhileFalse [in Equiv]
Himp.E_IfFalse [in Equiv]
Himp.E_IfTrue [in Equiv]
Himp.E_Seq [in Equiv]
Himp.E_Asgn [in Equiv]
Himp.E_Skip [in Equiv]
HoareAssertAssume.CAsgn [in Hoare]
HoareAssertAssume.CAssert [in Hoare]
HoareAssertAssume.CAssume [in Hoare]
HoareAssertAssume.CIf [in Hoare]
HoareAssertAssume.CSeq [in Hoare]
HoareAssertAssume.CSkip [in Hoare]
HoareAssertAssume.CWhile [in Hoare]
HoareAssertAssume.E_Assume [in Hoare]
HoareAssertAssume.E_AssertFalse [in Hoare]
HoareAssertAssume.E_AssertTrue [in Hoare]
HoareAssertAssume.E_WhileTrueError [in Hoare]
HoareAssertAssume.E_WhileTrueNormal [in Hoare]
HoareAssertAssume.E_WhileFalse [in Hoare]
HoareAssertAssume.E_IfFalse [in Hoare]
HoareAssertAssume.E_IfTrue [in Hoare]
HoareAssertAssume.E_SeqError [in Hoare]
HoareAssertAssume.E_SeqNormal [in Hoare]
HoareAssertAssume.E_Asgn [in Hoare]
HoareAssertAssume.E_Skip [in Hoare]
HoareAssertAssume.RError [in Hoare]
HoareAssertAssume.RNormal [in Hoare]
H_Consequence [in HoareAsLogic]
H_While [in HoareAsLogic]
H_If [in HoareAsLogic]
H_Seq [in HoareAsLogic]
H_Asgn [in HoareAsLogic]
H_Skip [in HoareAsLogic]
I
If [in PE]If1.CAsgn [in Hoare]
If1.CIf [in Hoare]
If1.CIf1 [in Hoare]
If1.CSeq [in Hoare]
If1.CSkip [in Hoare]
If1.CWhile [in Hoare]
If1.E_WhileTrue [in Hoare]
If1.E_WhileFalse [in Hoare]
If1.E_IfFalse [in Hoare]
If1.E_IfTrue [in Hoare]
If1.E_Seq [in Hoare]
If1.E_Asgn [in Hoare]
If1.E_Skip [in Hoare]
L
loop [in PE]Loop.E'Asgn [in PE]
Loop.E'IfFalse [in PE]
Loop.E'IfTrue [in PE]
Loop.E'Seq [in PE]
Loop.E'Skip [in PE]
Loop.E'WhileFalse [in PE]
Loop.E'WhileTrue [in PE]
Loop.pe_ceval_count_intro [in PE]
Loop.PE_WhileFixed [in PE]
Loop.PE_WhileFixedLoop [in PE]
Loop.PE_WhileFixedEnd [in PE]
Loop.PE_While [in PE]
Loop.PE_WhileTrue [in PE]
Loop.PE_WhileFalse [in PE]
Loop.PE_If [in PE]
Loop.PE_IfFalse [in PE]
Loop.PE_IfTrue [in PE]
Loop.PE_Seq [in PE]
Loop.PE_AsgnDynamic [in PE]
Loop.PE_AsgnStatic [in PE]
Loop.PE_Skip [in PE]
ltac_goal_to_discard_intro [in LibTactics]
ltac_database_token [in LibTactics]
ltac_mark [in LibTactics]
ltac_wilds [in LibTactics]
ltac_wild [in LibTactics]
ltac_no_arg [in LibTactics]
M
multi_step [in Smallstep]multi_refl [in Smallstep]
P
P [in Smallstep]pe_peval_intro [in PE]
pe_ceval_intro [in PE]
PE_If [in PE]
PE_IfFalse [in PE]
PE_IfTrue [in PE]
PE_Seq [in PE]
PE_AsgnDynamic [in PE]
PE_AsgnStatic [in PE]
PE_Skip [in PE]
R
RecordSub.rtcons [in RecordSub]RecordSub.RTcons [in RecordSub]
RecordSub.rtnil [in RecordSub]
RecordSub.RTnil [in RecordSub]
RecordSub.ST_Rcd_Tail [in RecordSub]
RecordSub.ST_Rcd_Head [in RecordSub]
RecordSub.ST_ProjRcd [in RecordSub]
RecordSub.ST_Proj1 [in RecordSub]
RecordSub.ST_App2 [in RecordSub]
RecordSub.ST_App1 [in RecordSub]
RecordSub.ST_AppAbs [in RecordSub]
RecordSub.S_RcdPerm [in RecordSub]
RecordSub.S_RcdDepth [in RecordSub]
RecordSub.S_RcdWidth [in RecordSub]
RecordSub.S_Arrow [in RecordSub]
RecordSub.S_Top [in RecordSub]
RecordSub.S_Trans [in RecordSub]
RecordSub.S_Refl [in RecordSub]
RecordSub.tm_rcons [in RecordSub]
RecordSub.tm_rnil [in RecordSub]
RecordSub.tm_rproj [in RecordSub]
RecordSub.tm_abs [in RecordSub]
RecordSub.tm_app [in RecordSub]
RecordSub.tm_var [in RecordSub]
RecordSub.Ty_RCons [in RecordSub]
RecordSub.Ty_RNil [in RecordSub]
RecordSub.Ty_Arrow [in RecordSub]
RecordSub.Ty_Base [in RecordSub]
RecordSub.Ty_Top [in RecordSub]
RecordSub.T_RCons [in RecordSub]
RecordSub.T_RNil [in RecordSub]
RecordSub.T_Sub [in RecordSub]
RecordSub.T_Proj [in RecordSub]
RecordSub.T_App [in RecordSub]
RecordSub.T_Abs [in RecordSub]
RecordSub.T_Var [in RecordSub]
RecordSub.v_rcons [in RecordSub]
RecordSub.v_rnil [in RecordSub]
RecordSub.v_abs [in RecordSub]
RecordSub.wfArrow [in RecordSub]
RecordSub.wfBase [in RecordSub]
RecordSub.wfRCons [in RecordSub]
RecordSub.wfRNil [in RecordSub]
RecordSub.wfTop [in RecordSub]
RepeatExercise.CAsgn [in Hoare]
RepeatExercise.CIf [in Hoare]
RepeatExercise.CRepeat [in Hoare]
RepeatExercise.CSeq [in Hoare]
RepeatExercise.CSkip [in Hoare]
RepeatExercise.CWhile [in Hoare]
RepeatExercise.E_WhileTrue [in Hoare]
RepeatExercise.E_WhileFalse [in Hoare]
RepeatExercise.E_IfFalse [in Hoare]
RepeatExercise.E_IfTrue [in Hoare]
RepeatExercise.E_Seq [in Hoare]
RepeatExercise.E_Asgn [in Hoare]
RepeatExercise.E_Skip [in Hoare]
S
SimpleArith1.ST_Plus2 [in Smallstep]SimpleArith1.ST_Plus1 [in Smallstep]
SimpleArith1.ST_PlusConstConst [in Smallstep]
SS_Mult [in Smallstep]
SS_Minus [in Smallstep]
SS_Plus [in Smallstep]
SS_Load [in Smallstep]
SS_Push [in Smallstep]
STLCArith.tm_if0 [in StlcProp]
STLCArith.tm_mult [in StlcProp]
STLCArith.tm_pred [in StlcProp]
STLCArith.tm_succ [in StlcProp]
STLCArith.tm_const [in StlcProp]
STLCArith.tm_abs [in StlcProp]
STLCArith.tm_app [in StlcProp]
STLCArith.tm_var [in StlcProp]
STLCArith.Ty_Nat [in StlcProp]
STLCArith.Ty_Arrow [in StlcProp]
STLCExtendedRecords.FirstTry.Arrow [in Records]
STLCExtendedRecords.FirstTry.Base [in Records]
STLCExtendedRecords.FirstTry.TRcd [in Records]
STLCExtendedRecords.rtcons [in Records]
STLCExtendedRecords.RTcons [in Records]
STLCExtendedRecords.rtnil [in Records]
STLCExtendedRecords.RTnil [in Records]
STLCExtendedRecords.ST_Rcd_Tail [in Records]
STLCExtendedRecords.ST_Rcd_Head [in Records]
STLCExtendedRecords.ST_ProjRcd [in Records]
STLCExtendedRecords.ST_Proj1 [in Records]
STLCExtendedRecords.ST_App2 [in Records]
STLCExtendedRecords.ST_App1 [in Records]
STLCExtendedRecords.ST_AppAbs [in Records]
STLCExtendedRecords.tm_rcons [in Records]
STLCExtendedRecords.tm_rnil [in Records]
STLCExtendedRecords.tm_rproj [in Records]
STLCExtendedRecords.tm_abs [in Records]
STLCExtendedRecords.tm_app [in Records]
STLCExtendedRecords.tm_var [in Records]
STLCExtendedRecords.Ty_RCons [in Records]
STLCExtendedRecords.Ty_RNil [in Records]
STLCExtendedRecords.Ty_Arrow [in Records]
STLCExtendedRecords.Ty_Base [in Records]
STLCExtendedRecords.T_RCons [in Records]
STLCExtendedRecords.T_RNil [in Records]
STLCExtendedRecords.T_Proj [in Records]
STLCExtendedRecords.T_App [in Records]
STLCExtendedRecords.T_Abs [in Records]
STLCExtendedRecords.T_Var [in Records]
STLCExtendedRecords.v_rcons [in Records]
STLCExtendedRecords.v_rnil [in Records]
STLCExtendedRecords.v_abs [in Records]
STLCExtendedRecords.wfArrow [in Records]
STLCExtendedRecords.wfBase [in Records]
STLCExtendedRecords.wfRCons [in Records]
STLCExtendedRecords.wfRNil [in Records]
STLCExtended.ST_LcaseCons [in MoreStlc]
STLCExtended.ST_LcaseNil [in MoreStlc]
STLCExtended.ST_Lcase1 [in MoreStlc]
STLCExtended.ST_Cons2 [in MoreStlc]
STLCExtended.ST_Cons1 [in MoreStlc]
STLCExtended.ST_CaseInr [in MoreStlc]
STLCExtended.ST_CaseInl [in MoreStlc]
STLCExtended.ST_Case [in MoreStlc]
STLCExtended.ST_Inr [in MoreStlc]
STLCExtended.ST_Inl [in MoreStlc]
STLCExtended.ST_If0_Nonzero [in MoreStlc]
STLCExtended.ST_If0_Zero [in MoreStlc]
STLCExtended.ST_If0 [in MoreStlc]
STLCExtended.ST_Mult2 [in MoreStlc]
STLCExtended.ST_Mult1 [in MoreStlc]
STLCExtended.ST_Mulconsts [in MoreStlc]
STLCExtended.ST_PredNat [in MoreStlc]
STLCExtended.ST_Pred [in MoreStlc]
STLCExtended.ST_SuccNat [in MoreStlc]
STLCExtended.ST_Succ [in MoreStlc]
STLCExtended.ST_App2 [in MoreStlc]
STLCExtended.ST_App1 [in MoreStlc]
STLCExtended.ST_AppAbs [in MoreStlc]
STLCExtended.tm_fix [in MoreStlc]
STLCExtended.tm_let [in MoreStlc]
STLCExtended.tm_snd [in MoreStlc]
STLCExtended.tm_fst [in MoreStlc]
STLCExtended.tm_pair [in MoreStlc]
STLCExtended.tm_unit [in MoreStlc]
STLCExtended.tm_lcase [in MoreStlc]
STLCExtended.tm_cons [in MoreStlc]
STLCExtended.tm_nil [in MoreStlc]
STLCExtended.tm_case [in MoreStlc]
STLCExtended.tm_inr [in MoreStlc]
STLCExtended.tm_inl [in MoreStlc]
STLCExtended.tm_if0 [in MoreStlc]
STLCExtended.tm_mult [in MoreStlc]
STLCExtended.tm_pred [in MoreStlc]
STLCExtended.tm_succ [in MoreStlc]
STLCExtended.tm_const [in MoreStlc]
STLCExtended.tm_abs [in MoreStlc]
STLCExtended.tm_app [in MoreStlc]
STLCExtended.tm_var [in MoreStlc]
STLCExtended.Ty_Prod [in MoreStlc]
STLCExtended.Ty_Unit [in MoreStlc]
STLCExtended.Ty_List [in MoreStlc]
STLCExtended.Ty_Sum [in MoreStlc]
STLCExtended.Ty_Nat [in MoreStlc]
STLCExtended.Ty_Arrow [in MoreStlc]
STLCExtended.T_Unit [in MoreStlc]
STLCExtended.T_Lcase [in MoreStlc]
STLCExtended.T_Cons [in MoreStlc]
STLCExtended.T_Nil [in MoreStlc]
STLCExtended.T_Case [in MoreStlc]
STLCExtended.T_Inr [in MoreStlc]
STLCExtended.T_Inl [in MoreStlc]
STLCExtended.T_If0 [in MoreStlc]
STLCExtended.T_Mult [in MoreStlc]
STLCExtended.T_Pred [in MoreStlc]
STLCExtended.T_Succ [in MoreStlc]
STLCExtended.T_Nat [in MoreStlc]
STLCExtended.T_App [in MoreStlc]
STLCExtended.T_Abs [in MoreStlc]
STLCExtended.T_Var [in MoreStlc]
STLCExtended.v_pair [in MoreStlc]
STLCExtended.v_unit [in MoreStlc]
STLCExtended.v_lcons [in MoreStlc]
STLCExtended.v_lnil [in MoreStlc]
STLCExtended.v_inr [in MoreStlc]
STLCExtended.v_inl [in MoreStlc]
STLCExtended.v_nat [in MoreStlc]
STLCExtended.v_abs [in MoreStlc]
STLCProp.afi_if3 [in StlcProp]
STLCProp.afi_if2 [in StlcProp]
STLCProp.afi_if1 [in StlcProp]
STLCProp.afi_abs [in StlcProp]
STLCProp.afi_app2 [in StlcProp]
STLCProp.afi_app1 [in StlcProp]
STLCProp.afi_var [in StlcProp]
STLCRef.extends_cons [in References]
STLCRef.extends_nil [in References]
STLCRef.RefsAndNontermination.sc_step [in References]
STLCRef.RefsAndNontermination.sc_one [in References]
STLCRef.ST_Assign2 [in References]
STLCRef.ST_Assign1 [in References]
STLCRef.ST_Assign [in References]
STLCRef.ST_Deref [in References]
STLCRef.ST_DerefLoc [in References]
STLCRef.ST_Ref [in References]
STLCRef.ST_RefValue [in References]
STLCRef.ST_If0_Nonzero [in References]
STLCRef.ST_If0_Zero [in References]
STLCRef.ST_If0 [in References]
STLCRef.ST_Mult2 [in References]
STLCRef.ST_Mult1 [in References]
STLCRef.ST_MultNats [in References]
STLCRef.ST_Pred [in References]
STLCRef.ST_PredNat [in References]
STLCRef.ST_Succ [in References]
STLCRef.ST_SuccNat [in References]
STLCRef.ST_App2 [in References]
STLCRef.ST_App1 [in References]
STLCRef.ST_AppAbs [in References]
STLCRef.tm_loc [in References]
STLCRef.tm_assign [in References]
STLCRef.tm_deref [in References]
STLCRef.tm_ref [in References]
STLCRef.tm_unit [in References]
STLCRef.tm_if0 [in References]
STLCRef.tm_mult [in References]
STLCRef.tm_pred [in References]
STLCRef.tm_succ [in References]
STLCRef.tm_const [in References]
STLCRef.tm_abs [in References]
STLCRef.tm_app [in References]
STLCRef.tm_var [in References]
STLCRef.Ty_Ref [in References]
STLCRef.Ty_Arrow [in References]
STLCRef.Ty_Unit [in References]
STLCRef.Ty_Nat [in References]
STLCRef.T_Assign [in References]
STLCRef.T_Deref [in References]
STLCRef.T_Ref [in References]
STLCRef.T_Loc [in References]
STLCRef.T_Unit [in References]
STLCRef.T_If0 [in References]
STLCRef.T_Mult [in References]
STLCRef.T_Pred [in References]
STLCRef.T_Succ [in References]
STLCRef.T_Nat [in References]
STLCRef.T_App [in References]
STLCRef.T_Abs [in References]
STLCRef.T_Var [in References]
STLCRef.v_loc [in References]
STLCRef.v_unit [in References]
STLCRef.v_nat [in References]
STLCRef.v_abs [in References]
STLCSub.ST_If [in Sub]
STLCSub.ST_IfFalse [in Sub]
STLCSub.ST_IfTrue [in Sub]
STLCSub.ST_App2 [in Sub]
STLCSub.ST_App1 [in Sub]
STLCSub.ST_AppAbs [in Sub]
STLCSub.S_Arrow [in Sub]
STLCSub.S_Top [in Sub]
STLCSub.S_Trans [in Sub]
STLCSub.S_Refl [in Sub]
STLCSub.tm_snd [in Sub]
STLCSub.tm_fst [in Sub]
STLCSub.tm_pair [in Sub]
STLCSub.tm_unit [in Sub]
STLCSub.tm_if [in Sub]
STLCSub.tm_false [in Sub]
STLCSub.tm_true [in Sub]
STLCSub.tm_abs [in Sub]
STLCSub.tm_app [in Sub]
STLCSub.tm_var [in Sub]
STLCSub.Ty_Prod [in Sub]
STLCSub.Ty_Unit [in Sub]
STLCSub.Ty_Arrow [in Sub]
STLCSub.Ty_Base [in Sub]
STLCSub.Ty_Bool [in Sub]
STLCSub.Ty_Top [in Sub]
STLCSub.T_Sub [in Sub]
STLCSub.T_Unit [in Sub]
STLCSub.T_If [in Sub]
STLCSub.T_False [in Sub]
STLCSub.T_True [in Sub]
STLCSub.T_App [in Sub]
STLCSub.T_Abs [in Sub]
STLCSub.T_Var [in Sub]
STLCSub.v_unit [in Sub]
STLCSub.v_false [in Sub]
STLCSub.v_true [in Sub]
STLCSub.v_abs [in Sub]
STLC.ST_If [in Stlc]
STLC.ST_IfFalse [in Stlc]
STLC.ST_IfTrue [in Stlc]
STLC.ST_App2 [in Stlc]
STLC.ST_App1 [in Stlc]
STLC.ST_AppAbs [in Stlc]
STLC.s_var1 [in Stlc]
STLC.tm_if [in Stlc]
STLC.tm_false [in Stlc]
STLC.tm_true [in Stlc]
STLC.tm_abs [in Stlc]
STLC.tm_app [in Stlc]
STLC.tm_var [in Stlc]
STLC.Ty_Arrow [in Stlc]
STLC.Ty_Bool [in Stlc]
STLC.T_If [in Stlc]
STLC.T_False [in Stlc]
STLC.T_True [in Stlc]
STLC.T_App [in Stlc]
STLC.T_Abs [in Stlc]
STLC.T_Var [in Stlc]
STLC.v_false [in Stlc]
STLC.v_true [in Stlc]
STLC.v_abs [in Stlc]
ST_Plus2 [in Smallstep]
ST_Plus1 [in Smallstep]
ST_PlusConstConst [in Smallstep]
ST_SndPair [in Norm]
ST_Snd1 [in Norm]
ST_FstPair [in Norm]
ST_Fst1 [in Norm]
ST_Pair2 [in Norm]
ST_Pair1 [in Norm]
ST_If [in Norm]
ST_IfFalse [in Norm]
ST_IfTrue [in Norm]
ST_App2 [in Norm]
ST_App1 [in Norm]
ST_AppAbs [in Norm]
T
Temp1.ST_Plus2 [in Smallstep]Temp1.ST_Plus1 [in Smallstep]
Temp1.ST_PlusConstConst [in Smallstep]
Temp1.v_funny [in Smallstep]
Temp1.v_const [in Smallstep]
Temp2.ST_Plus2 [in Smallstep]
Temp2.ST_Plus1 [in Smallstep]
Temp2.ST_PlusConstConst [in Smallstep]
Temp2.ST_Funny [in Smallstep]
Temp2.v_const [in Smallstep]
Temp3.ST_Plus1 [in Smallstep]
Temp3.ST_PlusConstConst [in Smallstep]
Temp3.v_const [in Smallstep]
Temp4.fls [in Smallstep]
Temp4.ST_If [in Smallstep]
Temp4.ST_IfFalse [in Smallstep]
Temp4.ST_IfTrue [in Smallstep]
Temp4.Temp5.ST_If [in Smallstep]
Temp4.Temp5.ST_IfFalse [in Smallstep]
Temp4.Temp5.ST_IfTrue [in Smallstep]
Temp4.test [in Smallstep]
Temp4.tru [in Smallstep]
Temp4.v_fls [in Smallstep]
Temp4.v_tru [in Smallstep]
tm_snd [in Norm]
tm_fst [in Norm]
tm_pair [in Norm]
tm_if [in Norm]
tm_false [in Norm]
tm_true [in Norm]
tm_abs [in Norm]
tm_app [in Norm]
tm_var [in Norm]
TM.Bool [in Types]
TM.bv_false [in Types]
TM.bv_true [in Types]
TM.fls [in Types]
TM.iszro [in Types]
TM.ite [in Types]
TM.Nat [in Types]
TM.nv_succ [in Types]
TM.nv_0 [in Types]
TM.prd [in Types]
TM.scc [in Types]
TM.ST_Iszero [in Types]
TM.ST_IszeroSucc [in Types]
TM.ST_Iszero0 [in Types]
TM.ST_Pred [in Types]
TM.ST_PredSucc [in Types]
TM.ST_Pred0 [in Types]
TM.ST_Succ [in Types]
TM.ST_If [in Types]
TM.ST_IfFalse [in Types]
TM.ST_IfTrue [in Types]
TM.tru [in Types]
TM.T_Iszero [in Types]
TM.T_Pred [in Types]
TM.T_Succ [in Types]
TM.T_0 [in Types]
TM.T_If [in Types]
TM.T_False [in Types]
TM.T_True [in Types]
TM.zro [in Types]
Ty_Prod [in Norm]
Ty_Arrow [in Norm]
Ty_Bool [in Norm]
T_Snd [in Norm]
T_Fst [in Norm]
T_Pair [in Norm]
T_If [in Norm]
T_False [in Norm]
T_True [in Norm]
T_App [in Norm]
T_Abs [in Norm]
T_Var [in Norm]
V
VNUId [in Equiv]VNUMinus [in Equiv]
VNUMult [in Equiv]
VNUNum [in Equiv]
VNUPlus [in Equiv]
v_const [in Smallstep]
V_cons [in Norm]
V_nil [in Norm]
v_pair [in Norm]
v_false [in Norm]
v_true [in Norm]
v_abs [in Norm]
Axiom Index
E
EqualityExamples.big_expression_using [in UseTactics]ExamplesLets.typing_inversion_var [in UseTactics]
G
gt_not_le [in UseAuto]I
inj_pair2 [in LibTactics]L
le_gt_false [in UseAuto]le_not_gt [in UseAuto]
P
P [in UseAuto]S
skip_axiom [in LibTactics]subtype [in UseAuto]
subtype_trans [in UseAuto]
subtype_refl [in UseAuto]
T
typ [in UseAuto]Inductive Index
A
appears_free_in [in Norm]astep [in Smallstep]
aval [in Smallstep]
B
block [in PE]Boxer [in LibTactics]
bstep [in Smallstep]
C
CImp.com [in Smallstep]CImp.cstep [in Smallstep]
Combined.step [in Smallstep]
Combined.tm [in Smallstep]
Combined.value [in Smallstep]
cstep [in Smallstep]
D
dcom [in Hoare2]DComFirstTry.dcom [in Hoare2]
decorated [in Hoare2]
derivable [in HoareAsLogic]
E
eval [in Smallstep]H
has_type [in Norm]Himp.ceval [in Hoare]
Himp.ceval [in Equiv]
Himp.com [in Hoare]
Himp.com [in Equiv]
HoareAssertAssume.ceval [in Hoare]
HoareAssertAssume.com [in Hoare]
HoareAssertAssume.result [in Hoare]
I
If1.ceval [in Hoare]If1.com [in Hoare]
instantiation [in Norm]
L
Loop.ceval_count [in PE]Loop.pe_ceval_count [in PE]
Loop.pe_com [in PE]
ltac_goal_to_discard [in LibTactics]
Ltac_database_token [in LibTactics]
ltac_Mark [in LibTactics]
ltac_Wilds [in LibTactics]
ltac_Wild [in LibTactics]
ltac_No_arg [in LibTactics]
M
multi [in Smallstep]P
parity_label [in PE]peval [in PE]
pe_peval [in PE]
pe_ceval [in PE]
pe_com [in PE]
R
RecordSub.has_type [in RecordSub]RecordSub.record_tm [in RecordSub]
RecordSub.record_ty [in RecordSub]
RecordSub.step [in RecordSub]
RecordSub.subtype [in RecordSub]
RecordSub.tm [in RecordSub]
RecordSub.ty [in RecordSub]
RecordSub.value [in RecordSub]
RecordSub.well_formed_ty [in RecordSub]
RepeatExercise.ceval [in Hoare]
RepeatExercise.com [in Hoare]
S
SimpleArith1.step [in Smallstep]stack_step [in Smallstep]
step [in Smallstep]
step [in Norm]
STLCArith.has_type [in StlcProp]
STLCArith.step [in StlcProp]
STLCArith.tm [in StlcProp]
STLCArith.ty [in StlcProp]
STLCArith.value [in StlcProp]
STLCExtendedRecords.FirstTry.ty [in Records]
STLCExtendedRecords.has_type [in Records]
STLCExtendedRecords.record_tm [in Records]
STLCExtendedRecords.record_ty [in Records]
STLCExtendedRecords.step [in Records]
STLCExtendedRecords.tm [in Records]
STLCExtendedRecords.ty [in Records]
STLCExtendedRecords.value [in Records]
STLCExtendedRecords.well_formed_ty [in Records]
STLCExtended.has_type [in MoreStlc]
STLCExtended.step [in MoreStlc]
STLCExtended.tm [in MoreStlc]
STLCExtended.ty [in MoreStlc]
STLCExtended.value [in MoreStlc]
STLCProp.appears_free_in [in StlcProp]
STLCRef.extends [in References]
STLCRef.has_type [in References]
STLCRef.RefsAndNontermination.step_closure [in References]
STLCRef.step [in References]
STLCRef.tm [in References]
STLCRef.ty [in References]
STLCRef.value [in References]
STLCSub.has_type [in Sub]
STLCSub.step [in Sub]
STLCSub.subtype [in Sub]
STLCSub.tm [in Sub]
STLCSub.ty [in Sub]
STLCSub.value [in Sub]
STLC.has_type [in Stlc]
STLC.step [in Stlc]
STLC.substi [in Stlc]
STLC.tm [in Stlc]
STLC.ty [in Stlc]
STLC.value [in Stlc]
T
Temp1.step [in Smallstep]Temp1.value [in Smallstep]
Temp2.step [in Smallstep]
Temp2.value [in Smallstep]
Temp3.step [in Smallstep]
Temp3.value [in Smallstep]
Temp4.step [in Smallstep]
Temp4.Temp5.step [in Smallstep]
Temp4.tm [in Smallstep]
Temp4.value [in Smallstep]
tm [in Smallstep]
tm [in Norm]
TM.bvalue [in Types]
TM.has_type [in Types]
TM.nvalue [in Types]
TM.step [in Types]
TM.tm [in Types]
TM.ty [in Types]
ty [in Norm]
V
value [in Smallstep]value [in Norm]
var_not_used_in_aexp [in Equiv]
Section Index
D
DemoAbsurd1 [in UseAuto]E
equatesLemma [in LibTactics]F
FuncEq [in LibTactics]H
HintsTransitivity [in UseAuto]Abbreviation Index
M
multistep [in Norm]R
RecordSub.Examples.A [in RecordSub]RecordSub.Examples.B [in RecordSub]
RecordSub.Examples.C [in RecordSub]
RecordSub.Examples.i [in RecordSub]
RecordSub.Examples.j [in RecordSub]
RecordSub.Examples.k [in RecordSub]
RecordSub.Examples.x [in RecordSub]
RecordSub.Examples.y [in RecordSub]
RecordSub.Examples.z [in RecordSub]
S
step_normal_form [in Norm]STLCArith.multistep [in StlcProp]
STLCExtendedRecords.A [in Records]
STLCExtendedRecords.a [in Records]
STLCExtendedRecords.B [in Records]
STLCExtendedRecords.f [in Records]
STLCExtendedRecords.g [in Records]
STLCExtendedRecords.i1 [in Records]
STLCExtendedRecords.i2 [in Records]
STLCExtendedRecords.k [in Records]
STLCExtendedRecords.l [in Records]
STLCExtendedRecords.multistep [in Records]
STLCExtended.Examples.a [in MoreStlc]
STLCExtended.Examples.eo [in MoreStlc]
STLCExtended.Examples.eq [in MoreStlc]
STLCExtended.Examples.even [in MoreStlc]
STLCExtended.Examples.evenodd [in MoreStlc]
STLCExtended.Examples.f [in MoreStlc]
STLCExtended.Examples.g [in MoreStlc]
STLCExtended.Examples.i1 [in MoreStlc]
STLCExtended.Examples.i2 [in MoreStlc]
STLCExtended.Examples.k [in MoreStlc]
STLCExtended.Examples.l [in MoreStlc]
STLCExtended.Examples.m [in MoreStlc]
STLCExtended.Examples.n [in MoreStlc]
STLCExtended.Examples.odd [in MoreStlc]
STLCExtended.Examples.processSum [in MoreStlc]
STLCExtended.Examples.x [in MoreStlc]
STLCExtended.Examples.y [in MoreStlc]
STLCExtended.multistep [in MoreStlc]
STLCSub.Examples.A [in Sub]
STLCSub.Examples.B [in Sub]
STLCSub.Examples.C [in Sub]
STLCSub.Examples.Float [in Sub]
STLCSub.Examples.Integer [in Sub]
STLCSub.Examples.String [in Sub]
STLCSub.Examples.x [in Sub]
STLCSub.Examples.y [in Sub]
STLCSub.Examples.z [in Sub]
STLCSub.FormalThoughtExercises.a [in Sub]
STLCSub.FormalThoughtExercises.p [in Sub]
STLC.idB [in Stlc]
STLC.idBB [in Stlc]
STLC.idBBBB [in Stlc]
STLC.k [in Stlc]
STLC.multistep [in Stlc]
STLC.notB [in Stlc]
T
TM.step_normal_form [in Types]Definition Index
A
aequiv [in Equiv]Aexp [in Hoare]
Aexp_of_aexp [in Hoare]
Aexp_of_nat [in Hoare]
appears_free_in_sind [in Norm]
appears_free_in_ind [in Norm]
Assertion [in Hoare]
assertion_sub_ex2' [in Hoare]
assertion_sub_ex1' [in Hoare]
assertion_sub_example2'' [in Hoare]
assertion_sub_example2' [in Hoare]
assertion_sub_example2 [in Hoare]
assertion_sub_example [in Hoare]
assertion_sub [in Hoare]
assert_implies [in Hoare]
assert_of_Prop [in Hoare]
assign [in PE]
assigned [in PE]
astep_sind [in Smallstep]
astep_ind [in Smallstep]
atrans_sound [in Equiv]
aval_sind [in Smallstep]
aval_ind [in Smallstep]
B
bassertion [in Hoare]bequiv [in Equiv]
block_sind [in PE]
block_rec [in PE]
block_ind [in PE]
block_rect [in PE]
Boxer_sind [in LibTactics]
Boxer_rec [in LibTactics]
Boxer_ind [in LibTactics]
Boxer_rect [in LibTactics]
bstep_sind [in Smallstep]
bstep_ind [in Smallstep]
btrans_sound [in Equiv]
C
capprox [in Equiv]cequiv [in Equiv]
CImp.cmultistep [in Smallstep]
CImp.com_sind [in Smallstep]
CImp.com_rec [in Smallstep]
CImp.com_ind [in Smallstep]
CImp.com_rect [in Smallstep]
CImp.cstep_sind [in Smallstep]
CImp.cstep_ind [in Smallstep]
CImp.par_loop_example_2 [in Smallstep]
CImp.par_loop_example_0 [in Smallstep]
CImp.par_loop [in Smallstep]
closed [in Norm]
closed_env [in Norm]
cmin [in Equiv]
COIND [in LibTactics]
Combined.step_sind [in Smallstep]
Combined.step_ind [in Smallstep]
Combined.tm_sind [in Smallstep]
Combined.tm_rec [in Smallstep]
Combined.tm_ind [in Smallstep]
Combined.tm_rect [in Smallstep]
Combined.value_sind [in Smallstep]
Combined.value_ind [in Smallstep]
compiler_is_correct_statement [in Smallstep]
congruence_example [in Equiv]
context [in Norm]
cstep_sind [in Smallstep]
cstep_ind [in Smallstep]
ctrans_sound [in Equiv]
c3 [in Equiv]
c4 [in Equiv]
D
DComFirstTry.dcom_sind [in Hoare2]DComFirstTry.dcom_rec [in Hoare2]
DComFirstTry.dcom_ind [in Hoare2]
DComFirstTry.dcom_rect [in Hoare2]
dcom_sind [in Hoare2]
dcom_rec [in Hoare2]
dcom_ind [in Hoare2]
dcom_rect [in Hoare2]
decorated_sind [in Hoare2]
decorated_rec [in Hoare2]
decorated_ind [in Hoare2]
decorated_rect [in Hoare2]
dec_while_triple_correct [in Hoare2]
dec_while [in Hoare2]
dec0 [in Hoare2]
dec1 [in Hoare2]
def_with_exists [in LibTactics]
derivable_sind [in HoareAsLogic]
derivable_rec [in HoareAsLogic]
derivable_ind [in HoareAsLogic]
derivable_rect [in HoareAsLogic]
deterministic [in Smallstep]
dfib [in Hoare2]
div_mod_dec [in Hoare2]
dpow2_dec [in Hoare2]
drop [in Norm]
E
empty_pe_state [in PE]env [in Norm]
equiv_classes [in Equiv]
eq' [in LibTactics]
erase [in Hoare2]
erase_while_ex [in Hoare2]
erase_d [in Hoare2]
evalF [in Smallstep]
eval_sind [in Smallstep]
eval_ind [in Smallstep]
ExampleAssertionSub.equivalent_assertion2 [in Hoare]
ExampleAssertionSub.equivalent_assertion1 [in Hoare]
ExamplePrettyAssertions.assertion1 [in Hoare]
ExamplePrettyAssertions.assertion2 [in Hoare]
ExamplePrettyAssertions.assertion3 [in Hoare]
ExamplePrettyAssertions.assertion4 [in Hoare]
ExamplePrettyAssertions.assertion5 [in Hoare]
ExamplePrettyAssertions.assertion6 [in Hoare]
ExamplePrettyAssertions.assertion7 [in Hoare]
ExamplePrettyAssertions.assertion8 [in Hoare]
ExamplePrettyAssertions.assertion9 [in Hoare]
ExAssertions.assertion1 [in Hoare]
ExAssertions.assertion2 [in Hoare]
ExAssertions.assertion3 [in Hoare]
ExAssertions.assertion4 [in Hoare]
F
factorial_dec [in Hoare2]fib [in Hoare2]
FILL_IN_HERE [in Smallstep]
FILL_IN_HERE [in Hoare2]
FirstTry.type_check [in Typechecking]
fold_com_ex1 [in Equiv]
fold_constants_com [in Equiv]
fold_bexp_ex2 [in Equiv]
fold_bexp_ex1 [in Equiv]
fold_constants_bexp [in Equiv]
fold_aexp_ex2 [in Equiv]
fold_aexp_ex1 [in Equiv]
fold_constants_aexp [in Equiv]
H
halts [in Norm]has_type_sind [in Norm]
has_type_ind [in Norm]
Himp.cequiv [in Equiv]
Himp.ceval_sind [in Hoare]
Himp.ceval_ind [in Hoare]
Himp.ceval_sind [in Equiv]
Himp.ceval_ind [in Equiv]
Himp.com_sind [in Hoare]
Himp.com_rec [in Hoare]
Himp.com_ind [in Hoare]
Himp.com_rect [in Hoare]
Himp.com_sind [in Equiv]
Himp.com_rec [in Equiv]
Himp.com_ind [in Equiv]
Himp.com_rect [in Equiv]
Himp.havoc_pre [in Hoare]
Himp.havoc_example2 [in Equiv]
Himp.havoc_example1 [in Equiv]
Himp.manual_grade_for_Check_rule_for_HAVOC [in Equiv]
Himp.pcopy [in Equiv]
Himp.ptwice [in Equiv]
Himp.pXY [in Equiv]
Himp.pYX [in Equiv]
Himp.p1 [in Equiv]
Himp.p2 [in Equiv]
Himp.p3 [in Equiv]
Himp.p4 [in Equiv]
Himp.p5 [in Equiv]
Himp.p6 [in Equiv]
Himp.valid_hoare_triple [in Hoare]
HoareAssertAssume.assert_assume_example [in Hoare]
HoareAssertAssume.ceval_sind [in Hoare]
HoareAssertAssume.ceval_ind [in Hoare]
HoareAssertAssume.com_sind [in Hoare]
HoareAssertAssume.com_rec [in Hoare]
HoareAssertAssume.com_ind [in Hoare]
HoareAssertAssume.com_rect [in Hoare]
HoareAssertAssume.result_sind [in Hoare]
HoareAssertAssume.result_rec [in Hoare]
HoareAssertAssume.result_ind [in Hoare]
HoareAssertAssume.result_rect [in Hoare]
HoareAssertAssume.valid_hoare_triple [in Hoare]
hoare_asgn_example4 [in Hoare]
hoare_asgn_example3 [in Hoare]
hoare_asgn_example1''' [in Hoare]
hoare_asgn_example1'' [in Hoare]
hoare_asgn_example1' [in Hoare]
hoare_asgn_example1 [in Hoare]
hoare_asgn_examples2 [in Hoare]
hoare_asgn_examples1 [in Hoare]
I
if_example''' [in Hoare]if_example'' [in Hoare]
if_example [in Hoare]
if_minus_plus_dec [in Hoare2]
If1.ceval_sind [in Hoare]
If1.ceval_ind [in Hoare]
If1.com_sind [in Hoare]
If1.com_rec [in Hoare]
If1.com_ind [in Hoare]
If1.com_rect [in Hoare]
If1.if1false_test [in Hoare]
If1.if1true_test [in Hoare]
If1.manual_grade_for_hoare_if1 [in Hoare]
If1.valid_hoare_triple [in Hoare]
inb [in PE]
instantiation_sind [in Norm]
instantiation_ind [in Norm]
InvertsExamples1.typing_nonexample_1 [in UseTactics]
is_wp [in Hoare2]
K
keval [in PE]keval_example [in PE]
L
lookup [in Norm]Loop.ceval_count_sind [in PE]
Loop.ceval_count_ind [in PE]
Loop.pe_ceval_count_sind [in PE]
Loop.pe_ceval_count_ind [in PE]
Loop.pe_loop_example4 [in PE]
Loop.pe_loop_example3 [in PE]
Loop.pe_loop_example2 [in PE]
Loop.pe_loop_example1 [in PE]
Loop.pe_com_sind [in PE]
Loop.pe_com_ind [in PE]
Loop.square_loop [in PE]
ltac_goal_to_discard_sind [in LibTactics]
ltac_goal_to_discard_rec [in LibTactics]
ltac_goal_to_discard_ind [in LibTactics]
ltac_goal_to_discard_rect [in LibTactics]
ltac_something [in LibTactics]
ltac_to_generalize [in LibTactics]
ltac_tag_subst [in LibTactics]
ltac_int_to_nat [in LibTactics]
ltac_database [in LibTactics]
Ltac_database_token_sind [in LibTactics]
Ltac_database_token_rec [in LibTactics]
Ltac_database_token_ind [in LibTactics]
Ltac_database_token_rect [in LibTactics]
ltac_Mark_sind [in LibTactics]
ltac_Mark_rec [in LibTactics]
ltac_Mark_ind [in LibTactics]
ltac_Mark_rect [in LibTactics]
ltac_Wilds_sind [in LibTactics]
ltac_Wilds_rec [in LibTactics]
ltac_Wilds_ind [in LibTactics]
ltac_Wilds_rect [in LibTactics]
ltac_Wild_sind [in LibTactics]
ltac_Wild_rec [in LibTactics]
ltac_Wild_ind [in LibTactics]
ltac_Wild_rect [in LibTactics]
ltac_No_arg_sind [in LibTactics]
ltac_No_arg_rec [in LibTactics]
ltac_No_arg_ind [in LibTactics]
ltac_No_arg_rect [in LibTactics]
M
manual_grade_for_eval__multistep_inf [in Smallstep]manual_grade_for_hoare_repeat [in Hoare]
manual_grade_for_not_congr [in Equiv]
manual_grade_for_equiv_classes [in Equiv]
manual_grade_for_norm [in Norm]
manual_grade_for_norm_fail [in Norm]
manual_grade_for_pair_permutation [in Sub]
manual_grade_for_smallest_2 [in Sub]
manual_grade_for_smallest_1 [in Sub]
manual_grade_for_small_large_4 [in Sub]
manual_grade_for_small_large_2 [in Sub]
manual_grade_for_small_large_1 [in Sub]
manual_grade_for_proper_subtypes [in Sub]
manual_grade_for_subtype_concepts_tf [in Sub]
manual_grade_for_subtype_instances_tf_2 [in Sub]
manual_grade_for_subtype_order [in Sub]
manual_grade_for_arrow_sub_wrong [in Sub]
minimum_dec [in Hoare2]
msubst [in Norm]
multi_sind [in Smallstep]
multi_ind [in Smallstep]
mupdate [in Norm]
myFact [in UseAuto]
N
normalizing [in Smallstep]normal_form_of [in Smallstep]
normal_form [in Smallstep]
O
optimizer [in Equiv]optimize_0plus_com [in Equiv]
optimize_0plus_bexp [in Equiv]
optimize_0plus_aexp [in Equiv]
outer_triple_valid [in Hoare2]
P
parity [in Hoare2]parity [in PE]
parity_dec [in Hoare2]
parity_eval [in PE]
parity_body [in PE]
parity_label_sind [in PE]
parity_label_rec [in PE]
parity_label_ind [in PE]
parity_label_rect [in PE]
peval_sind [in PE]
peval_ind [in PE]
pe_peval_sind [in PE]
pe_peval_ind [in PE]
pe_program [in PE]
pe_block_example [in PE]
pe_block [in PE]
pe_ceval_sind [in PE]
pe_ceval_ind [in PE]
pe_example3 [in PE]
pe_example2 [in PE]
pe_example1 [in PE]
pe_com_sind [in PE]
pe_com_ind [in PE]
pe_removes [in PE]
pe_compare [in PE]
pe_unique [in PE]
pe_disagree_at [in PE]
pe_add [in PE]
pe_remove [in PE]
pe_bexp [in PE]
pe_update [in PE]
pe_consistent [in PE]
pe_aexp [in PE]
pe_lookup [in PE]
pe_state [in PE]
positive_difference_dec [in Hoare2]
post [in Hoare2]
postcondition_from_while [in Hoare2]
postcondition_from [in Hoare2]
pow2 [in Hoare2]
precondition_from_while [in Hoare2]
precondition_from [in Hoare2]
prog [in Smallstep]
program [in PE]
prog_i [in Equiv]
prog_h [in Equiv]
prog_g [in Equiv]
prog_f [in Equiv]
prog_e [in Equiv]
prog_d [in Equiv]
prog_c [in Equiv]
prog_b [in Equiv]
prog_a [in Equiv]
R
R [in Norm]RecordSub.context [in RecordSub]
RecordSub.Examples.subtyping_example_4 [in RecordSub]
RecordSub.Examples.subtyping_example_3 [in RecordSub]
RecordSub.Examples.subtyping_example_2 [in RecordSub]
RecordSub.Examples.subtyping_example_1 [in RecordSub]
RecordSub.Examples.subtyping_example_0 [in RecordSub]
RecordSub.Examples.TRcd_kj [in RecordSub]
RecordSub.Examples.TRcd_j [in RecordSub]
RecordSub.Examples2.trcd_kj [in RecordSub]
RecordSub.Examples2.typing_example_2 [in RecordSub]
RecordSub.Examples2.typing_example_1 [in RecordSub]
RecordSub.Examples2.typing_example_0 [in RecordSub]
RecordSub.has_type_sind [in RecordSub]
RecordSub.has_type_ind [in RecordSub]
RecordSub.manual_grade_for_rcd_types_match_informal [in RecordSub]
RecordSub.record_tm_sind [in RecordSub]
RecordSub.record_tm_ind [in RecordSub]
RecordSub.record_ty_sind [in RecordSub]
RecordSub.record_ty_ind [in RecordSub]
RecordSub.step_sind [in RecordSub]
RecordSub.step_ind [in RecordSub]
RecordSub.subst [in RecordSub]
RecordSub.subtype_sind [in RecordSub]
RecordSub.subtype_ind [in RecordSub]
RecordSub.tlookup [in RecordSub]
RecordSub.Tlookup [in RecordSub]
RecordSub.tm_sind [in RecordSub]
RecordSub.tm_rec [in RecordSub]
RecordSub.tm_ind [in RecordSub]
RecordSub.tm_rect [in RecordSub]
RecordSub.ty_sind [in RecordSub]
RecordSub.ty_rec [in RecordSub]
RecordSub.ty_ind [in RecordSub]
RecordSub.ty_rect [in RecordSub]
RecordSub.value_sind [in RecordSub]
RecordSub.value_ind [in RecordSub]
RecordSub.well_formed_ty_sind [in RecordSub]
RecordSub.well_formed_ty_ind [in RecordSub]
reduce_to_zero [in Hoare2]
refines [in Equiv]
relation [in Smallstep]
RepeatExercise.ceval_sind [in Hoare]
RepeatExercise.ceval_ind [in Hoare]
RepeatExercise.com_sind [in Hoare]
RepeatExercise.com_rec [in Hoare]
RepeatExercise.com_ind [in Hoare]
RepeatExercise.com_rect [in Hoare]
RepeatExercise.ex1_repeat [in Hoare]
RepeatExercise.valid_hoare_triple [in Hoare]
rm [in LibTactics]
S
sample_proof [in HoareAsLogic]SimpleArith1.step_sind [in Smallstep]
SimpleArith1.step_ind [in Smallstep]
SimpleArith1.test_step_2 [in Smallstep]
SimpleArith1.test_step_1 [in Smallstep]
slow_assignment_dec [in Hoare2]
sqrt_dec [in Hoare2]
stack [in Smallstep]
stack_multistep [in Smallstep]
stack_step_sind [in Smallstep]
stack_step_ind [in Smallstep]
StepFunction.assert [in Typechecking]
StepFunction.manual_grade_for_stepf_defn [in Typechecking]
StepFunction.manual_grade_for_valuef_defn [in Typechecking]
StepFunction.stepf [in Typechecking]
StepFunction.valuef [in Typechecking]
step_example1''' [in Smallstep]
step_example1'' [in Smallstep]
step_example1' [in Smallstep]
step_example1 [in Smallstep]
step_normal_form [in Smallstep]
step_sind [in Smallstep]
step_ind [in Smallstep]
step_sind [in Norm]
step_ind [in Norm]
STLCArith.context [in StlcProp]
STLCArith.has_type_sind [in StlcProp]
STLCArith.has_type_rec [in StlcProp]
STLCArith.has_type_ind [in StlcProp]
STLCArith.has_type_rect [in StlcProp]
STLCArith.Nat_typing_example [in StlcProp]
STLCArith.Nat_step_example [in StlcProp]
STLCArith.step_sind [in StlcProp]
STLCArith.step_rec [in StlcProp]
STLCArith.step_ind [in StlcProp]
STLCArith.step_rect [in StlcProp]
STLCArith.subst [in StlcProp]
STLCArith.tm_sind [in StlcProp]
STLCArith.tm_rec [in StlcProp]
STLCArith.tm_ind [in StlcProp]
STLCArith.tm_rect [in StlcProp]
STLCArith.ty_sind [in StlcProp]
STLCArith.ty_rec [in StlcProp]
STLCArith.ty_ind [in StlcProp]
STLCArith.ty_rect [in StlcProp]
STLCArith.value_sind [in StlcProp]
STLCArith.value_rec [in StlcProp]
STLCArith.value_ind [in StlcProp]
STLCArith.value_rect [in StlcProp]
STLCChecker.type_check [in Typechecking]
STLCExtendedRecords.context [in Records]
STLCExtendedRecords.FirstTry.alist [in Records]
STLCExtendedRecords.FirstTry.ty_sind [in Records]
STLCExtendedRecords.FirstTry.ty_rec [in Records]
STLCExtendedRecords.FirstTry.ty_ind [in Records]
STLCExtendedRecords.FirstTry.ty_rect [in Records]
STLCExtendedRecords.has_type_sind [in Records]
STLCExtendedRecords.has_type_ind [in Records]
STLCExtendedRecords.record_tm_sind [in Records]
STLCExtendedRecords.record_tm_ind [in Records]
STLCExtendedRecords.record_ty_sind [in Records]
STLCExtendedRecords.record_ty_ind [in Records]
STLCExtendedRecords.step_sind [in Records]
STLCExtendedRecords.step_ind [in Records]
STLCExtendedRecords.subst [in Records]
STLCExtendedRecords.Tlookup [in Records]
STLCExtendedRecords.tlookup [in Records]
STLCExtendedRecords.tm_sind [in Records]
STLCExtendedRecords.tm_rec [in Records]
STLCExtendedRecords.tm_ind [in Records]
STLCExtendedRecords.tm_rect [in Records]
STLCExtendedRecords.typing_nonexample_2 [in Records]
STLCExtendedRecords.typing_nonexample [in Records]
STLCExtendedRecords.ty_sind [in Records]
STLCExtendedRecords.ty_rec [in Records]
STLCExtendedRecords.ty_ind [in Records]
STLCExtendedRecords.ty_rect [in Records]
STLCExtendedRecords.value_sind [in Records]
STLCExtendedRecords.value_ind [in Records]
STLCExtendedRecords.weird_type [in Records]
STLCExtendedRecords.well_formed_ty_sind [in Records]
STLCExtendedRecords.well_formed_ty_ind [in Records]
STLCExtended.context [in MoreStlc]
STLCExtended.Examples.FixTest1.fact [in MoreStlc]
STLCExtended.Examples.FixTest1.reduces [in MoreStlc]
STLCExtended.Examples.FixTest1.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest2.map [in MoreStlc]
STLCExtended.Examples.FixTest2.reduces [in MoreStlc]
STLCExtended.Examples.FixTest2.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest3.equal [in MoreStlc]
STLCExtended.Examples.FixTest3.reduces [in MoreStlc]
STLCExtended.Examples.FixTest3.reduces2 [in MoreStlc]
STLCExtended.Examples.FixTest3.typechecks [in MoreStlc]
STLCExtended.Examples.FixTest4.eotest [in MoreStlc]
STLCExtended.Examples.FixTest4.reduces [in MoreStlc]
STLCExtended.Examples.FixTest4.typechecks [in MoreStlc]
STLCExtended.Examples.LetTest.reduces [in MoreStlc]
STLCExtended.Examples.LetTest.tm_test [in MoreStlc]
STLCExtended.Examples.LetTest.typechecks [in MoreStlc]
STLCExtended.Examples.LetTest1.reduces [in MoreStlc]
STLCExtended.Examples.LetTest1.tm_test [in MoreStlc]
STLCExtended.Examples.LetTest1.typechecks [in MoreStlc]
STLCExtended.Examples.ListTest.reduces [in MoreStlc]
STLCExtended.Examples.ListTest.tm_test [in MoreStlc]
STLCExtended.Examples.ListTest.typechecks [in MoreStlc]
STLCExtended.Examples.Numtest.reduces [in MoreStlc]
STLCExtended.Examples.Numtest.tm_test [in MoreStlc]
STLCExtended.Examples.Numtest.typechecks [in MoreStlc]
STLCExtended.Examples.ProdTest.reduces [in MoreStlc]
STLCExtended.Examples.ProdTest.tm_test [in MoreStlc]
STLCExtended.Examples.ProdTest.typechecks [in MoreStlc]
STLCExtended.Examples.Sumtest1.reduces [in MoreStlc]
STLCExtended.Examples.Sumtest1.tm_test [in MoreStlc]
STLCExtended.Examples.Sumtest1.typechecks [in MoreStlc]
STLCExtended.Examples.Sumtest2.reduces [in MoreStlc]
STLCExtended.Examples.Sumtest2.tm_test [in MoreStlc]
STLCExtended.Examples.Sumtest2.typechecks [in MoreStlc]
STLCExtended.has_type_sind [in MoreStlc]
STLCExtended.has_type_ind [in MoreStlc]
STLCExtended.step_sind [in MoreStlc]
STLCExtended.step_ind [in MoreStlc]
STLCExtended.subst [in MoreStlc]
STLCExtended.substeg1 [in MoreStlc]
STLCExtended.substeg2 [in MoreStlc]
STLCExtended.substeg3 [in MoreStlc]
STLCExtended.tm_sind [in MoreStlc]
STLCExtended.tm_rec [in MoreStlc]
STLCExtended.tm_ind [in MoreStlc]
STLCExtended.tm_rect [in MoreStlc]
STLCExtended.ty_sind [in MoreStlc]
STLCExtended.ty_rec [in MoreStlc]
STLCExtended.ty_ind [in MoreStlc]
STLCExtended.ty_rect [in MoreStlc]
STLCExtended.value_sind [in MoreStlc]
STLCExtended.value_ind [in MoreStlc]
STLCExtended.w [in MoreStlc]
STLCExtended.x [in MoreStlc]
STLCExtended.y [in MoreStlc]
STLCExtended.z [in MoreStlc]
STLCProp.appears_free_in_sind [in StlcProp]
STLCProp.appears_free_in_ind [in StlcProp]
STLCProp.closed [in StlcProp]
STLCProp.manual_grade_for_stlc_variation3 [in StlcProp]
STLCProp.manual_grade_for_stlc_variation2 [in StlcProp]
STLCProp.manual_grade_for_stlc_variation1 [in StlcProp]
STLCProp.manual_grade_for_progress_preservation_statement [in StlcProp]
STLCProp.manual_grade_for_afi [in StlcProp]
STLCProp.manual_grade_for_subject_expansion_stlc [in StlcProp]
STLCProp.stuck [in StlcProp]
STLCRef.context [in References]
STLCRef.ExampleVariables.r [in References]
STLCRef.ExampleVariables.s [in References]
STLCRef.ExampleVariables.x [in References]
STLCRef.ExampleVariables.y [in References]
STLCRef.extends_sind [in References]
STLCRef.extends_ind [in References]
STLCRef.has_type_sind [in References]
STLCRef.has_type_ind [in References]
STLCRef.manual_grade_for_preservation_informal [in References]
STLCRef.manual_grade_for_type_safety_violation [in References]
STLCRef.manual_grade_for_compact_update [in References]
STLCRef.multistep [in References]
STLCRef.preservation_theorem [in References]
STLCRef.RefsAndNontermination.factorial [in References]
STLCRef.RefsAndNontermination.loop [in References]
STLCRef.RefsAndNontermination.loop_fun [in References]
STLCRef.RefsAndNontermination.multistep1 [in References]
STLCRef.RefsAndNontermination.step_closure_sind [in References]
STLCRef.RefsAndNontermination.step_closure_ind [in References]
STLCRef.replace [in References]
STLCRef.step_sind [in References]
STLCRef.step_ind [in References]
STLCRef.store [in References]
STLCRef.store_well_typed [in References]
STLCRef.store_Tlookup [in References]
STLCRef.store_ty [in References]
STLCRef.store_lookup [in References]
STLCRef.subst [in References]
STLCRef.tm_sind [in References]
STLCRef.tm_rec [in References]
STLCRef.tm_ind [in References]
STLCRef.tm_rect [in References]
STLCRef.tseq [in References]
STLCRef.ty_sind [in References]
STLCRef.ty_rec [in References]
STLCRef.ty_ind [in References]
STLCRef.ty_rect [in References]
STLCRef.value_sind [in References]
STLCRef.value_ind [in References]
STLCRef.x [in References]
STLCRef.y [in References]
STLCRef.z [in References]
STLCSub.context [in Sub]
STLCSub.Examples.Employee [in Sub]
STLCSub.Examples.Person [in Sub]
STLCSub.Examples.Student [in Sub]
STLCSub.Examples.subtyping_example_2 [in Sub]
STLCSub.Examples.subtyping_example_1 [in Sub]
STLCSub.Examples.subtyping_example_0 [in Sub]
STLCSub.Examples.sub_employee_person [in Sub]
STLCSub.Examples.sub_student_person [in Sub]
STLCSub.FormalThoughtExercises.TF [in Sub]
STLCSub.has_type_sind [in Sub]
STLCSub.has_type_ind [in Sub]
STLCSub.manual_grade_for_products_preservation [in Sub]
STLCSub.manual_grade_for_products_progress [in Sub]
STLCSub.manual_grade_for_products_subtype_has_type [in Sub]
STLCSub.manual_grade_for_products_value_step [in Sub]
STLCSub.manual_grade_for_variations [in Sub]
STLCSub.step_sind [in Sub]
STLCSub.step_ind [in Sub]
STLCSub.subst [in Sub]
STLCSub.subtype_sind [in Sub]
STLCSub.subtype_ind [in Sub]
STLCSub.tm_sind [in Sub]
STLCSub.tm_rec [in Sub]
STLCSub.tm_ind [in Sub]
STLCSub.tm_rect [in Sub]
STLCSub.ty_sind [in Sub]
STLCSub.ty_rec [in Sub]
STLCSub.ty_ind [in Sub]
STLCSub.ty_rect [in Sub]
STLCSub.value_sind [in Sub]
STLCSub.value_ind [in Sub]
STLCTypes.eqb_ty [in Typechecking]
STLC.context [in Stlc]
STLC.has_type_sind [in Stlc]
STLC.has_type_ind [in Stlc]
STLC.step_sind [in Stlc]
STLC.step_ind [in Stlc]
STLC.subst [in Stlc]
STLC.substi_sind [in Stlc]
STLC.substi_rec [in Stlc]
STLC.substi_ind [in Stlc]
STLC.substi_rect [in Stlc]
STLC.tm_sind [in Stlc]
STLC.tm_rec [in Stlc]
STLC.tm_ind [in Stlc]
STLC.tm_rect [in Stlc]
STLC.typing_nonexample_3 [in Stlc]
STLC.typing_nonexample_1 [in Stlc]
STLC.typing_example_3 [in Stlc]
STLC.typing_example_2_full [in Stlc]
STLC.typing_example_2 [in Stlc]
STLC.typing_example_1' [in Stlc]
STLC.typing_example_1 [in Stlc]
STLC.ty_sind [in Stlc]
STLC.ty_rec [in Stlc]
STLC.ty_ind [in Stlc]
STLC.ty_rect [in Stlc]
STLC.value_sind [in Stlc]
STLC.value_ind [in Stlc]
STLC.x [in Stlc]
STLC.y [in Stlc]
STLC.z [in Stlc]
subst [in Norm]
subst_equiv_property [in Equiv]
subst_aexp_ex [in Equiv]
subst_aexp [in Equiv]
subtract_slowly_dec [in Hoare2]
swap_program [in Hoare]
swap_dec [in Hoare2]
T
T [in Hoare2]tass [in Norm]
Temp1.step_sind [in Smallstep]
Temp1.step_ind [in Smallstep]
Temp1.value_sind [in Smallstep]
Temp1.value_ind [in Smallstep]
Temp2.step_sind [in Smallstep]
Temp2.step_ind [in Smallstep]
Temp2.value_sind [in Smallstep]
Temp2.value_ind [in Smallstep]
Temp3.step_sind [in Smallstep]
Temp3.step_ind [in Smallstep]
Temp3.value_sind [in Smallstep]
Temp3.value_ind [in Smallstep]
Temp4.bool_step_prop3 [in Smallstep]
Temp4.bool_step_prop2 [in Smallstep]
Temp4.bool_step_prop1 [in Smallstep]
Temp4.manual_grade_for_smallstep_bools [in Smallstep]
Temp4.step_sind [in Smallstep]
Temp4.step_ind [in Smallstep]
Temp4.Temp5.bool_step_prop4_holds [in Smallstep]
Temp4.Temp5.bool_step_prop4 [in Smallstep]
Temp4.Temp5.manual_grade_for_properties_of_altered_step [in Smallstep]
Temp4.Temp5.step_sind [in Smallstep]
Temp4.Temp5.step_ind [in Smallstep]
Temp4.tm_sind [in Smallstep]
Temp4.tm_rec [in Smallstep]
Temp4.tm_ind [in Smallstep]
Temp4.tm_rect [in Smallstep]
Temp4.value_sind [in Smallstep]
Temp4.value_ind [in Smallstep]
test_optimize_0plus [in Equiv]
test_pe_bexp2 [in PE]
test_pe_bexp1 [in PE]
test_pe_update [in PE]
test_pe_aexp1 [in PE]
text_pe_aexp2 [in PE]
tm_sind [in Smallstep]
tm_rec [in Smallstep]
tm_ind [in Smallstep]
tm_rect [in Smallstep]
tm_sind [in Norm]
tm_rec [in Norm]
tm_ind [in Norm]
tm_rect [in Norm]
TM.bvalue_sind [in Types]
TM.bvalue_ind [in Types]
TM.has_type_not [in Types]
TM.has_type_1 [in Types]
TM.has_type_sind [in Types]
TM.has_type_ind [in Types]
TM.manual_grade_for_prog_pres_bigstep [in Types]
TM.manual_grade_for_remove_pred0 [in Types]
TM.manual_grade_for_variation2 [in Types]
TM.manual_grade_for_variation1 [in Types]
TM.manual_grade_for_finish_preservation_informal [in Types]
TM.manual_grade_for_finish_progress_informal [in Types]
TM.multistep [in Types]
TM.nvalue_sind [in Types]
TM.nvalue_ind [in Types]
TM.some_term_is_stuck [in Types]
TM.step_sind [in Types]
TM.step_ind [in Types]
TM.stuck [in Types]
TM.succ_hastype_nat__hastype_nat [in Types]
TM.tm_sind [in Types]
TM.tm_rec [in Types]
TM.tm_ind [in Types]
TM.tm_rect [in Types]
TM.ty_sind [in Types]
TM.ty_rec [in Types]
TM.ty_ind [in Types]
TM.ty_rect [in Types]
TM.value [in Types]
two_loops_dec [in Hoare2]
TypecheckerExtensions.eqb_ty [in Typechecking]
TypecheckerExtensions.manual_grade_for_type_check_defn [in Typechecking]
TypecheckerExtensions.type_check [in Typechecking]
ty_sind [in Norm]
ty_rec [in Norm]
ty_ind [in Norm]
ty_rect [in Norm]
V
valid [in HoareAsLogic]valid_hoare_triple [in Hoare]
value_sind [in Smallstep]
value_ind [in Smallstep]
value_sind [in Norm]
value_ind [in Norm]
var_not_used_in_aexp_sind [in Equiv]
var_not_used_in_aexp_ind [in Equiv]
vc_dec_while [in Hoare2]
verification_conditions_from [in Hoare2]
verification_conditions [in Hoare2]
W
while_example [in Hoare]wp [in HoareAsLogic]
Z
zprop [in Equiv]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2515 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (352 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (73 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (500 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (622 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (119 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (58 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (738 entries) |
This page has been generated by coqdoc