| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5472 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (309 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (3342 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (70 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (504 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (615 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (118 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (60 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (401 entries) |
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]
ap [definition, in Hoare]
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]
ap2 [definition, in Hoare]
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]
assert [abbreviation, in Hoare]
Assertion [definition, in Hoare]
assert_of_Prop [definition, in Hoare]
assert_implies [definition, in Hoare]
Assign [constructor, in PE]
assign [definition, in PE]
assigned [definition, in PE]
assign_aequiv [lemma, in Equiv]
assign_removes [lemma, in PE]
assn_sub_ex2' [definition, in Hoare]
assn_sub_ex1' [definition, in Hoare]
assn_sub_example2'' [definition, in Hoare]
assn_sub_example2' [definition, in Hoare]
assn_sub_example2 [definition, in Hoare]
assn_sub_example [definition, in Hoare]
assn_sub [definition, in Hoare]
astep [inductive, in Smallstep]
AS_Mult [constructor, in Smallstep]
AS_Mult2 [constructor, in Smallstep]
AS_Mult1 [constructor, in Smallstep]
AS_Minus [constructor, in Smallstep]
AS_Minus2 [constructor, in Smallstep]
AS_Minus1 [constructor, in Smallstep]
AS_Plus [constructor, in Smallstep]
AS_Plus2 [constructor, in Smallstep]
AS_Plus1 [constructor, in Smallstep]
AS_Id [constructor, in Smallstep]
atrans_sound [definition, in Equiv]
atrans:91 [binder, in Equiv]
aval [inductive, in Smallstep]
av_num [constructor, in Smallstep]
a':64 [binder, in Equiv]
a1':136 [binder, in PE]
a1':195 [binder, in Smallstep]
a1':203 [binder, in Smallstep]
a1':210 [binder, in PE]
a1':211 [binder, in Smallstep]
a1':222 [binder, in Smallstep]
a1':230 [binder, in Smallstep]
a1':250 [binder, in Smallstep]
a1':282 [binder, in Smallstep]
a1:1 [binder, in Equiv]
a1:120 [binder, in Equiv]
a1:125 [binder, in Hoare]
a1:127 [binder, in Equiv]
a1:129 [binder, in Equiv]
a1:131 [binder, in Equiv]
a1:131 [binder, in PE]
a1:135 [binder, in PE]
a1:16 [binder, in PE]
a1:173 [binder, in Hoare]
a1:179 [binder, in Equiv]
a1:194 [binder, in Smallstep]
a1:202 [binder, in Smallstep]
a1:205 [binder, in PE]
a1:209 [binder, in PE]
a1:210 [binder, in Smallstep]
a1:210 [binder, in Hoare]
a1:221 [binder, in Smallstep]
a1:229 [binder, in Smallstep]
a1:249 [binder, in Smallstep]
a1:265 [binder, in Hoare]
a1:281 [binder, in Smallstep]
a1:324 [binder, in PE]
a1:45 [binder, in Equiv]
a1:47 [binder, in Equiv]
a2':199 [binder, in Smallstep]
a2':207 [binder, in Smallstep]
a2':215 [binder, in Smallstep]
a2':226 [binder, in Smallstep]
a2':234 [binder, in Smallstep]
a2:121 [binder, in Equiv]
a2:128 [binder, in Equiv]
a2:130 [binder, in Equiv]
a2:132 [binder, in Equiv]
a2:17 [binder, in PE]
a2:180 [binder, in Equiv]
a2:196 [binder, in Smallstep]
a2:198 [binder, in Smallstep]
a2:2 [binder, in Equiv]
a2:204 [binder, in Smallstep]
a2:206 [binder, in Smallstep]
a2:212 [binder, in Smallstep]
a2:214 [binder, in Smallstep]
a2:223 [binder, in Smallstep]
a2:225 [binder, in Smallstep]
a2:231 [binder, in Smallstep]
a2:233 [binder, in Smallstep]
a2:46 [binder, in Equiv]
a2:48 [binder, in Equiv]
a3:49 [binder, in Equiv]
a:10 [binder, in Hoare]
a:10 [binder, in PE]
a:106 [binder, in Hoare]
a:106 [binder, in Equiv]
a:108 [binder, in Hoare]
A:108 [binder, in LibTactics]
a:11 [binder, in HoareAsLogic]
A:112 [binder, in LibTactics]
a:115 [binder, in Equiv]
A:117 [binder, in UseAuto]
a:135 [binder, in Equiv]
A:14 [binder, in PE]
a:143 [binder, in Equiv]
A:16 [binder, in LibTactics]
a:162 [binder, in Hoare]
A:17 [binder, in LibTactics]
a:18 [binder, in PE]
A:20 [binder, in LibTactics]
a:208 [binder, in UseAuto]
A:21 [binder, in References]
a:21 [binder, in PE]
a:211 [binder, in UseAuto]
a:216 [binder, in UseAuto]
A:237 [binder, in References]
A:25 [binder, in LibTactics]
A:27 [binder, in LibTactics]
A:28 [binder, in References]
a:29 [binder, in LibTactics]
A:3 [binder, in LibTactics]
a:30 [binder, in LibTactics]
a:30 [binder, in PE]
A:31 [binder, in References]
a:31 [binder, in LibTactics]
a:317 [binder, in Hoare]
a:32 [binder, in LibTactics]
a:42 [binder, in UseAuto]
a:43 [binder, in UseAuto]
a:43 [binder, in Equiv]
a:44 [binder, in UseTactics]
a:44 [binder, in Equiv]
a:46 [binder, in UseTactics]
a:46 [binder, in PE]
a:51 [binder, in Hoare2]
a:51 [binder, in UseTactics]
a:53 [binder, in Hoare2]
a:55 [binder, in Hoare]
a:60 [binder, in Hoare]
a:63 [binder, in Equiv]
a:64 [binder, in Hoare]
a:68 [binder, in Hoare]
a:7 [binder, in Hoare2]
a:72 [binder, in Hoare2]
a:73 [binder, in Typechecking]
a:74 [binder, in Hoare2]
a:76 [binder, in Hoare2]
a:79 [binder, in Hoare2]
A:8 [binder, in PE]
a:84 [binder, in UseTactics]
a:85 [binder, in UseTactics]
a:92 [binder, in Equiv]
a:95 [binder, in Hoare2]
a:97 [binder, in Equiv]
B
bassn [definition, in Hoare]bequiv [definition, in Equiv]
bequiv_example [lemma, in Equiv]
bexp_eval_false [lemma, in Hoare]
Bib [library]
block [inductive, in PE]
body [constructor, in PE]
boxer [constructor, in LibTactics]
Boxer [inductive, in LibTactics]
bstep [inductive, 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]
btrans:93 [binder, in Equiv]
b':66 [binder, in Equiv]
b':70 [binder, in Equiv]
b':76 [binder, in Equiv]
b':86 [binder, in Equiv]
b1':238 [binder, in Smallstep]
b1':240 [binder, in Smallstep]
b1':263 [binder, in Smallstep]
b1':295 [binder, in Smallstep]
b1:148 [binder, in PE]
b1:154 [binder, in PE]
b1:161 [binder, in PE]
b1:223 [binder, in PE]
b1:230 [binder, in PE]
b1:237 [binder, in Smallstep]
b1:238 [binder, in PE]
b1:239 [binder, in Smallstep]
b1:245 [binder, in PE]
b1:250 [binder, in PE]
b1:258 [binder, in PE]
b1:262 [binder, in Smallstep]
b1:264 [binder, in PE]
b1:269 [binder, in PE]
b1:273 [binder, in Smallstep]
b1:276 [binder, in PE]
b1:294 [binder, in Smallstep]
b1:305 [binder, in Smallstep]
b1:336 [binder, in PE]
b1:342 [binder, in PE]
b1:346 [binder, in PE]
b1:352 [binder, in PE]
b1:4 [binder, in Equiv]
b1:51 [binder, in Equiv]
b1:53 [binder, in Equiv]
b2':243 [binder, in Smallstep]
b2:241 [binder, in Smallstep]
b2:242 [binder, in Smallstep]
b2:244 [binder, in Smallstep]
b2:5 [binder, in Equiv]
b2:52 [binder, in Equiv]
b2:54 [binder, in Equiv]
b3:55 [binder, in Equiv]
b:100 [binder, in Equiv]
B:107 [binder, in LibTactics]
b:108 [binder, in Equiv]
b:110 [binder, in Hoare]
b:112 [binder, in Hoare]
B:113 [binder, in LibTactics]
b:116 [binder, in Hoare]
b:135 [binder, in Hoare]
b:140 [binder, in Hoare]
b:143 [binder, in Hoare]
b:149 [binder, in Hoare]
b:15 [binder, in Hoare2]
b:153 [binder, in Equiv]
b:158 [binder, in Equiv]
b:161 [binder, in Equiv]
b:164 [binder, in Hoare]
b:167 [binder, in Equiv]
b:183 [binder, in Hoare]
b:188 [binder, in Hoare]
b:19 [binder, in Equiv]
b:19 [binder, in HoareAsLogic]
b:191 [binder, in Hoare]
b:197 [binder, in Hoare]
b:22 [binder, in Equiv]
b:220 [binder, in Hoare]
b:225 [binder, in Hoare]
b:228 [binder, in Hoare]
b:234 [binder, in Hoare]
b:25 [binder, in Equiv]
b:25 [binder, in HoareAsLogic]
b:278 [binder, in Hoare]
b:28 [binder, in Equiv]
b:283 [binder, in Hoare]
b:286 [binder, in Hoare]
b:292 [binder, in Hoare]
b:295 [binder, in Hoare]
b:298 [binder, in Hoare]
b:30 [binder, in Equiv]
b:300 [binder, in Hoare]
b:302 [binder, in Hoare]
b:310 [binder, in Hoare]
b:313 [binder, in Hoare]
b:336 [binder, in Hoare]
b:34 [binder, in Equiv]
b:340 [binder, in Hoare]
b:36 [binder, in Equiv]
b:45 [binder, in UseTactics]
b:47 [binder, in UseTactics]
b:49 [binder, in PE]
b:50 [binder, in Equiv]
b:52 [binder, in Hoare2]
b:52 [binder, in UseTactics]
b:52 [binder, in PE]
b:54 [binder, in Hoare2]
b:54 [binder, in PE]
b:65 [binder, in Equiv]
b:67 [binder, in UseTactics]
b:68 [binder, in HoareAsLogic]
b:69 [binder, in Equiv]
b:72 [binder, in Typechecking]
b:73 [binder, in Hoare2]
b:75 [binder, in Hoare2]
b:75 [binder, in Equiv]
b:77 [binder, in Hoare2]
b:80 [binder, in Hoare2]
b:85 [binder, in Equiv]
b:9 [binder, in Hoare2]
b:94 [binder, 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.CPar [constructor, in Smallstep]
CImp.CSeq [constructor, in Smallstep]
CImp.CSkip [constructor, in Smallstep]
CImp.cstep [inductive, 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.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.tru [constructor, in Smallstep]
Combined.value [inductive, 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]
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]
ctrans:95 [binder, in Equiv]
CWhile_congruence [lemma, in Equiv]
c'':220 [binder, in PE]
c'':227 [binder, in PE]
c'':234 [binder, in PE]
c'':243 [binder, in PE]
c'':372 [binder, in PE]
c'':382 [binder, in PE]
c'':391 [binder, in PE]
c'':399 [binder, in PE]
c':16 [binder, in Types]
c':176 [binder, in PE]
c':186 [binder, in PE]
c':188 [binder, in Equiv]
c':192 [binder, in PE]
c':198 [binder, in PE]
c':370 [binder, in PE]
c':380 [binder, in PE]
c':390 [binder, in PE]
c':398 [binder, in PE]
c':406 [binder, in PE]
c':68 [binder, in Equiv]
c':72 [binder, in Equiv]
c':78 [binder, in Equiv]
c1':144 [binder, in PE]
c1':151 [binder, in PE]
c1':164 [binder, in PE]
c1':218 [binder, in PE]
c1':226 [binder, in PE]
c1':241 [binder, in PE]
c1':252 [binder, in PE]
c1':256 [binder, in Smallstep]
c1':260 [binder, in PE]
c1':271 [binder, in PE]
c1':278 [binder, in PE]
c1':288 [binder, in Smallstep]
c1':309 [binder, in Smallstep]
c1':82 [binder, in Equiv]
c1':88 [binder, in Equiv]
c1:11 [binder, in Equiv]
c1:117 [binder, in Hoare]
c1:128 [binder, in Hoare]
c1:136 [binder, in Hoare]
c1:141 [binder, in Hoare]
c1:142 [binder, in PE]
c1:146 [binder, in Equiv]
c1:149 [binder, in PE]
c1:154 [binder, in Equiv]
c1:155 [binder, in PE]
c1:159 [binder, in Equiv]
c1:162 [binder, in PE]
c1:169 [binder, in Equiv]
c1:17 [binder, in Equiv]
c1:176 [binder, in Hoare]
c1:181 [binder, in Equiv]
c1:184 [binder, in Hoare]
c1:189 [binder, in Hoare]
c1:20 [binder, in Equiv]
c1:20 [binder, in HoareAsLogic]
c1:213 [binder, in Hoare]
c1:216 [binder, in PE]
c1:221 [binder, in Hoare]
c1:224 [binder, in PE]
c1:226 [binder, in Hoare]
c1:23 [binder, in Equiv]
c1:231 [binder, in PE]
c1:239 [binder, in PE]
c1:246 [binder, in PE]
c1:251 [binder, in PE]
c1:255 [binder, in Smallstep]
c1:259 [binder, in PE]
c1:26 [binder, in Equiv]
c1:264 [binder, in Smallstep]
c1:265 [binder, in PE]
c1:267 [binder, in Smallstep]
c1:268 [binder, in Hoare]
c1:270 [binder, in Smallstep]
c1:270 [binder, in PE]
c1:273 [binder, in Hoare]
c1:274 [binder, in Smallstep]
c1:277 [binder, in PE]
c1:279 [binder, in Hoare]
c1:284 [binder, in Hoare]
c1:287 [binder, in Smallstep]
c1:296 [binder, in Smallstep]
c1:299 [binder, in Smallstep]
c1:302 [binder, in Smallstep]
c1:306 [binder, in Smallstep]
c1:308 [binder, in Smallstep]
c1:313 [binder, in Smallstep]
c1:327 [binder, in PE]
c1:331 [binder, in Hoare]
c1:337 [binder, in Hoare]
c1:337 [binder, in PE]
c1:343 [binder, in PE]
c1:348 [binder, in PE]
c1:353 [binder, in PE]
c1:38 [binder, in Equiv]
c1:52 [binder, in Hoare]
c1:57 [binder, in Equiv]
c1:59 [binder, in Equiv]
c1:66 [binder, in HoareAsLogic]
c1:7 [binder, in Equiv]
c1:81 [binder, in Equiv]
c1:87 [binder, in Equiv]
c2'':254 [binder, in PE]
c2'':262 [binder, in PE]
c2':145 [binder, in PE]
c2':157 [binder, in PE]
c2':165 [binder, in PE]
c2':219 [binder, in PE]
c2':233 [binder, in PE]
c2':242 [binder, in PE]
c2':253 [binder, in PE]
c2':261 [binder, in PE]
c2':272 [binder, in PE]
c2':279 [binder, in PE]
c2':315 [binder, in Smallstep]
c2':84 [binder, in Equiv]
c2':90 [binder, in Equiv]
c2:118 [binder, in Hoare]
c2:12 [binder, in Equiv]
c2:129 [binder, in Hoare]
c2:137 [binder, in Hoare]
c2:142 [binder, in Hoare]
c2:143 [binder, in PE]
c2:147 [binder, in Equiv]
c2:150 [binder, in PE]
c2:155 [binder, in Equiv]
c2:156 [binder, in PE]
c2:160 [binder, in Equiv]
c2:163 [binder, in PE]
c2:170 [binder, in Equiv]
c2:177 [binder, in Hoare]
c2:18 [binder, in Equiv]
c2:182 [binder, in Equiv]
c2:185 [binder, in Hoare]
c2:190 [binder, in Hoare]
c2:21 [binder, in Equiv]
c2:21 [binder, in HoareAsLogic]
c2:214 [binder, in Hoare]
c2:217 [binder, in PE]
c2:222 [binder, in Hoare]
c2:225 [binder, in PE]
c2:227 [binder, in Hoare]
c2:232 [binder, in PE]
c2:24 [binder, in Equiv]
c2:240 [binder, in PE]
c2:258 [binder, in Smallstep]
c2:260 [binder, in Smallstep]
c2:265 [binder, in Smallstep]
c2:268 [binder, in Smallstep]
c2:269 [binder, in Hoare]
c2:27 [binder, in Equiv]
c2:271 [binder, in Smallstep]
c2:274 [binder, in Hoare]
c2:280 [binder, in Hoare]
c2:285 [binder, in Hoare]
c2:290 [binder, in Smallstep]
c2:292 [binder, in Smallstep]
c2:297 [binder, in Smallstep]
c2:300 [binder, in Smallstep]
c2:303 [binder, in Smallstep]
c2:310 [binder, in Smallstep]
c2:314 [binder, in Smallstep]
c2:328 [binder, in PE]
c2:332 [binder, in Hoare]
c2:338 [binder, in Hoare]
c2:338 [binder, in PE]
c2:344 [binder, in PE]
c2:39 [binder, in Equiv]
c2:53 [binder, in Hoare]
c2:58 [binder, in Equiv]
c2:60 [binder, in Equiv]
c2:67 [binder, in HoareAsLogic]
c2:8 [binder, in Equiv]
c2:83 [binder, in Equiv]
c2:89 [binder, in Equiv]
c3 [definition, in Equiv]
c3_c4_different [lemma, in Equiv]
c3:40 [binder, in Equiv]
c3:61 [binder, in Equiv]
c4 [definition, in Equiv]
c:1 [binder, in UseTactics]
c:101 [binder, in Hoare]
c:103 [binder, in Equiv]
c:105 [binder, in Hoare]
c:11 [binder, in UseTactics]
c:110 [binder, in Equiv]
c:112 [binder, in Equiv]
c:119 [binder, in PE]
c:13 [binder, in HoareAsLogic]
c:145 [binder, in Hoare]
c:15 [binder, in Types]
c:15 [binder, in Equiv]
c:150 [binder, in Hoare]
c:152 [binder, in Hoare]
c:159 [binder, in Hoare]
c:16 [binder, in Equiv]
c:163 [binder, in Equiv]
c:165 [binder, in Hoare]
c:166 [binder, in PE]
c:168 [binder, in Equiv]
c:168 [binder, in PE]
c:170 [binder, in PE]
c:172 [binder, in PE]
c:174 [binder, in PE]
c:183 [binder, in PE]
c:185 [binder, in Equiv]
c:186 [binder, in Equiv]
c:187 [binder, in Equiv]
c:189 [binder, in PE]
c:193 [binder, in Hoare]
c:195 [binder, in PE]
c:198 [binder, in Hoare]
c:2 [binder, in HoareAsLogic]
c:200 [binder, in Hoare]
c:203 [binder, in Norm]
c:21 [binder, in UseTactics]
c:22 [binder, in UseTactics]
c:230 [binder, in Hoare]
c:235 [binder, in Hoare]
c:240 [binder, in Hoare]
c:241 [binder, in Norm]
c:243 [binder, in Norm]
c:247 [binder, in Hoare]
c:247 [binder, in Norm]
c:252 [binder, in Norm]
c:254 [binder, in Norm]
c:259 [binder, in Norm]
c:26 [binder, in UseTactics]
c:26 [binder, in HoareAsLogic]
c:265 [binder, in Norm]
c:270 [binder, in Norm]
c:280 [binder, in PE]
c:282 [binder, in PE]
c:284 [binder, in PE]
c:286 [binder, in PE]
c:288 [binder, in Hoare]
c:288 [binder, in PE]
c:29 [binder, in Equiv]
c:290 [binder, in PE]
c:292 [binder, in PE]
c:293 [binder, in Hoare]
c:294 [binder, in PE]
c:296 [binder, in Hoare]
c:296 [binder, in PE]
c:298 [binder, in PE]
c:30 [binder, in UseTactics]
c:300 [binder, in PE]
c:302 [binder, in PE]
c:304 [binder, in Hoare]
c:304 [binder, in PE]
c:306 [binder, in PE]
c:308 [binder, in PE]
c:31 [binder, in Equiv]
c:310 [binder, in PE]
c:312 [binder, in PE]
c:314 [binder, in PE]
c:316 [binder, in PE]
c:318 [binder, in PE]
c:321 [binder, in Hoare]
c:325 [binder, in Hoare]
c:33 [binder, in HoareAsLogic]
c:341 [binder, in Hoare]
c:35 [binder, in Equiv]
c:356 [binder, in PE]
c:36 [binder, in Hoare]
c:360 [binder, in PE]
c:37 [binder, in Equiv]
c:387 [binder, in PE]
c:39 [binder, in HoareAsLogic]
c:395 [binder, in PE]
c:403 [binder, in PE]
c:42 [binder, in Hoare]
c:44 [binder, in HoareAsLogic]
c:46 [binder, in Hoare]
c:48 [binder, in HoareAsLogic]
c:50 [binder, in HoareAsLogic]
c:53 [binder, in UseTactics]
c:53 [binder, in HoareAsLogic]
c:55 [binder, in HoareAsLogic]
c:56 [binder, in Equiv]
c:59 [binder, in HoareAsLogic]
c:61 [binder, in HoareAsLogic]
c:66 [binder, in UseAuto]
c:67 [binder, in Equiv]
c:69 [binder, in HoareAsLogic]
c:70 [binder, in UseAuto]
c:71 [binder, in Equiv]
c:72 [binder, in HoareAsLogic]
c:74 [binder, in UseAuto]
c:76 [binder, in Hoare]
c:77 [binder, in Equiv]
c:78 [binder, in UseAuto]
c:78 [binder, in Hoare2]
c:80 [binder, in Hoare]
c:81 [binder, in Hoare2]
c:82 [binder, in UseAuto]
c:85 [binder, in Hoare]
c:86 [binder, in UseTactics]
c:89 [binder, in Hoare]
c:90 [binder, in Hoare2]
c:90 [binder, in UseTactics]
c:93 [binder, in Hoare]
c:96 [binder, in Equiv]
c:97 [binder, in Hoare]
D
DCAsgn [constructor, in Hoare2]DCIf [constructor, in Hoare2]
dcom [inductive, 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]
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]
dec:28 [binder, in Hoare2]
dec:30 [binder, in Hoare2]
dec:35 [binder, in Hoare2]
dec:37 [binder, in Hoare2]
dec:44 [binder, in Hoare2]
dec:46 [binder, in Hoare2]
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]
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]
d1:11 [binder, in Hoare2]
d1:4 [binder, in Hoare2]
d2:13 [binder, in Hoare2]
d2:5 [binder, in Hoare2]
d:120 [binder, in UseAuto]
D:14 [binder, in LibTactics]
d:15 [binder, in HoareAsLogic]
d:17 [binder, in Hoare2]
D:18 [binder, in LibTactics]
d:20 [binder, in Hoare2]
d:21 [binder, in Hoare2]
d:240 [binder, in References]
d:25 [binder, in Hoare2]
d:32 [binder, in Hoare2]
d:39 [binder, in Hoare2]
d:42 [binder, in Hoare2]
d:54 [binder, in UseTactics]
E
empty_pe_state [definition, in PE]entry [constructor, in PE]
env [definition, in Norm]
env:225 [binder, in Norm]
env:228 [binder, in Norm]
env:260 [binder, in Norm]
env:271 [binder, in Norm]
eqb:15 [binder, in PE]
eqb:9 [binder, in PE]
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]
eval [inductive, in Smallstep]
evalF [definition, in Smallstep]
evalF_eval [lemma, in Smallstep]
eval__multistep [lemma, in Smallstep]
eval_assign [lemma, in PE]
ExamplePrettyAssertions [module, in Hoare]
ExamplePrettyAssertions.assn1 [definition, in Hoare]
ExamplePrettyAssertions.assn2 [definition, in Hoare]
ExamplePrettyAssertions.assn3 [definition, in Hoare]
ExamplePrettyAssertions.assn4 [definition, in Hoare]
ExamplePrettyAssertions.ex1 [definition, in Hoare]
ExamplePrettyAssertions.ex2 [definition, in Hoare]
ExamplePrettyAssertions.ex3 [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.assn1 [definition, in Hoare]
ExAssertions.assn2 [definition, in Hoare]
ExAssertions.assn3 [definition, in Hoare]
ExAssertions.assn4 [definition, in Hoare]
extract [definition, in Hoare2]
extract_while_ex [definition, in Hoare2]
extract_dec [definition, in Hoare2]
E_Plus [constructor, in Smallstep]
E_Const [constructor, in Smallstep]
E_Some [constructor, in PE]
E_None [constructor, in PE]
e':350 [binder, in Smallstep]
e':351 [binder, in Smallstep]
e':352 [binder, in Smallstep]
e:204 [binder, in Norm]
e:248 [binder, in Norm]
e:253 [binder, in Norm]
e:255 [binder, in Norm]
e:266 [binder, in Norm]
e:278 [binder, in LibTactics]
e:279 [binder, in LibTactics]
e:280 [binder, in LibTactics]
e:281 [binder, in LibTactics]
e:43 [binder, in StlcProp]
e:55 [binder, in UseTactics]
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]
F':13 [binder, in UseAuto]
F':15 [binder, in UseAuto]
F':31 [binder, in UseAuto]
F':33 [binder, in UseAuto]
F1:34 [binder, in UseAuto]
F2:35 [binder, in UseAuto]
F3:36 [binder, in UseAuto]
F:10 [binder, in UseAuto]
F:12 [binder, in UseAuto]
f:126 [binder, in LibTactics]
f:129 [binder, in LibTactics]
f:134 [binder, in LibTactics]
F:14 [binder, in UseAuto]
f:141 [binder, in LibTactics]
f:150 [binder, in LibTactics]
f:161 [binder, in LibTactics]
f:174 [binder, in LibTactics]
f:188 [binder, in Sub]
F:19 [binder, in UseAuto]
f:192 [binder, in Sub]
f:196 [binder, in UseAuto]
f:202 [binder, in UseAuto]
f:209 [binder, in UseAuto]
f:212 [binder, in UseAuto]
F:27 [binder, in UseAuto]
f:27 [binder, in Hoare]
F:30 [binder, in UseAuto]
f:31 [binder, in Hoare]
F:32 [binder, in UseAuto]
f:37 [binder, in UseAuto]
f:39 [binder, in UseAuto]
f:48 [binder, in UseAuto]
f:50 [binder, in UseTactics]
f:56 [binder, in UseTactics]
G
Gamma':115 [binder, in Records]Gamma':118 [binder, in Sub]
Gamma':14 [binder, in StlcProp]
Gamma':141 [binder, in Norm]
Gamma':172 [binder, in RecordSub]
Gamma':172 [binder, in MoreStlc]
Gamma':209 [binder, in References]
Gamma':75 [binder, in StlcProp]
Gamma':88 [binder, in Norm]
Gamma':95 [binder, in StlcProp]
Gamma:101 [binder, in Sub]
Gamma:103 [binder, in Records]
Gamma:105 [binder, in Sub]
Gamma:109 [binder, in MoreStlc]
Gamma:110 [binder, in Sub]
Gamma:111 [binder, in RecordSub]
Gamma:112 [binder, in MoreStlc]
Gamma:114 [binder, in RecordSub]
Gamma:114 [binder, in Records]
Gamma:117 [binder, in Sub]
Gamma:118 [binder, in Records]
Gamma:119 [binder, in MoreStlc]
Gamma:121 [binder, in RecordSub]
Gamma:121 [binder, in Records]
Gamma:121 [binder, in Sub]
Gamma:122 [binder, in MoreStlc]
Gamma:124 [binder, in RecordSub]
Gamma:124 [binder, in MoreStlc]
Gamma:124 [binder, in Sub]
Gamma:126 [binder, in MoreStlc]
Gamma:128 [binder, in References]
Gamma:128 [binder, in MoreStlc]
Gamma:129 [binder, in RecordSub]
Gamma:13 [binder, in Typechecking]
Gamma:13 [binder, in StlcProp]
Gamma:131 [binder, in References]
Gamma:131 [binder, in MoreStlc]
Gamma:133 [binder, in RecordSub]
Gamma:134 [binder, in RecordSub]
Gamma:136 [binder, in MoreStlc]
Gamma:138 [binder, in References]
Gamma:140 [binder, in RecordSub]
Gamma:140 [binder, in MoreStlc]
Gamma:140 [binder, in Norm]
Gamma:141 [binder, in References]
Gamma:143 [binder, in References]
Gamma:144 [binder, in MoreStlc]
Gamma:145 [binder, in References]
Gamma:147 [binder, in References]
Gamma:150 [binder, in References]
Gamma:150 [binder, in RecordSub]
Gamma:150 [binder, in Norm]
Gamma:153 [binder, in MoreStlc]
Gamma:155 [binder, in References]
Gamma:155 [binder, in MoreStlc]
Gamma:156 [binder, in References]
Gamma:158 [binder, in References]
Gamma:159 [binder, in MoreStlc]
Gamma:160 [binder, in RecordSub]
Gamma:161 [binder, in References]
Gamma:164 [binder, in References]
Gamma:167 [binder, in MoreStlc]
Gamma:17 [binder, in StlcProp]
Gamma:171 [binder, in RecordSub]
Gamma:171 [binder, in MoreStlc]
Gamma:175 [binder, in RecordSub]
Gamma:175 [binder, in MoreStlc]
Gamma:178 [binder, in RecordSub]
Gamma:178 [binder, in MoreStlc]
Gamma:184 [binder, in Norm]
Gamma:20 [binder, in StlcProp]
Gamma:208 [binder, in References]
Gamma:213 [binder, in References]
Gamma:217 [binder, in References]
Gamma:228 [binder, in References]
Gamma:244 [binder, in Norm]
Gamma:25 [binder, in Typechecking]
Gamma:26 [binder, in StlcProp]
Gamma:267 [binder, in Norm]
Gamma:28 [binder, in Typechecking]
Gamma:39 [binder, in Typechecking]
Gamma:42 [binder, in StlcProp]
Gamma:45 [binder, in Stlc]
Gamma:48 [binder, in Stlc]
Gamma:48 [binder, in Sub]
Gamma:51 [binder, in Sub]
Gamma:54 [binder, in Norm]
Gamma:55 [binder, in Stlc]
Gamma:57 [binder, in Norm]
Gamma:58 [binder, in Stlc]
Gamma:58 [binder, in Sub]
Gamma:59 [binder, in Stlc]
Gamma:61 [binder, in Sub]
Gamma:62 [binder, in Sub]
Gamma:63 [binder, in Typechecking]
Gamma:64 [binder, in Stlc]
Gamma:64 [binder, in Norm]
Gamma:66 [binder, in Typechecking]
Gamma:67 [binder, in Norm]
Gamma:67 [binder, in Sub]
Gamma:68 [binder, in Norm]
Gamma:68 [binder, in Sub]
Gamma:69 [binder, in Sub]
Gamma:70 [binder, in StlcProp]
Gamma:72 [binder, in UseTactics]
Gamma:73 [binder, in Norm]
Gamma:73 [binder, in Records]
Gamma:74 [binder, in StlcProp]
Gamma:74 [binder, in Norm]
Gamma:79 [binder, in Norm]
Gamma:83 [binder, in Norm]
Gamma:83 [binder, in Sub]
Gamma:87 [binder, in Norm]
Gamma:9 [binder, in Typechecking]
Gamma:90 [binder, in Sub]
Gamma:91 [binder, in Norm]
Gamma:94 [binder, in StlcProp]
Gamma:94 [binder, in UseTactics]
Gamma:94 [binder, in Norm]
Gamma:95 [binder, in Sub]
GenExample [module, in UseTactics]
GenExample.substitution_preserves_typing [lemma, in UseTactics]
Goto [constructor, in PE]
gt_not_le [axiom, in UseAuto]
G:102 [binder, in UseTactics]
g:197 [binder, in UseAuto]
g:203 [binder, in UseAuto]
g:210 [binder, in UseAuto]
g:213 [binder, in UseAuto]
g:40 [binder, in UseAuto]
g:49 [binder, in UseAuto]
G:99 [binder, in UseTactics]
H
halts [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.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.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.hoare_triple [definition, 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]
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.CIf [constructor, in Hoare]
HoareAssertAssume.com [inductive, 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.hoare_triple [definition, in Hoare]
HoareAssertAssume.RError [constructor, in Hoare]
HoareAssertAssume.result [inductive, in Hoare]
HoareAssertAssume.RNormal [constructor, 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_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_triple [definition, in Hoare]
hoare_asgn_weakest [lemma, in Hoare2]
hoare_complete [lemma, in HoareAsLogic]
hoare_sound [lemma, in HoareAsLogic]
Hoare2 [library]
HT:199 [binder, in Sub]
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]
h:198 [binder, in UseAuto]
h:204 [binder, in UseAuto]
h:214 [binder, in UseAuto]
I
identity_assignment [lemma, in Equiv]ids:100 [binder, in PE]
ids:109 [binder, in PE]
ids:113 [binder, in PE]
ids:117 [binder, in PE]
ids:125 [binder, in PE]
ids:96 [binder, in PE]
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.CIf [constructor, in Hoare]
If1.CIf1 [constructor, in Hoare]
If1.com [inductive, 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.hoare_triple [definition, in Hoare]
If1.if1false_test [definition, in Hoare]
If1.if1true_test [definition, in Hoare]
If1.manual_grade_for_hoare_if1 [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]
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]
i1:89 [binder, in RecordSub]
i2:90 [binder, in RecordSub]
i:10 [binder, in Records]
i:101 [binder, in RecordSub]
i:108 [binder, in Records]
i:12 [binder, in RecordSub]
i:125 [binder, in RecordSub]
i:135 [binder, in RecordSub]
i:147 [binder, in RecordSub]
i:15 [binder, in Records]
i:17 [binder, in RecordSub]
i:18 [binder, in Records]
i:189 [binder, in Sub]
i:191 [binder, in Sub]
i:193 [binder, in Smallstep]
i:193 [binder, in Sub]
i:195 [binder, in Sub]
i:20 [binder, in RecordSub]
i:23 [binder, in Records]
i:248 [binder, in Smallstep]
i:252 [binder, in Smallstep]
i:280 [binder, in Smallstep]
i:284 [binder, in Smallstep]
i:33 [binder, in RecordSub]
i:334 [binder, in Smallstep]
i:36 [binder, in RecordSub]
i:36 [binder, in Records]
i:39 [binder, in Records]
i:40 [binder, in RecordSub]
i:57 [binder, in Records]
i:58 [binder, in RecordSub]
i:59 [binder, in Records]
i:60 [binder, in RecordSub]
i:61 [binder, in Records]
i:62 [binder, in RecordSub]
i:65 [binder, in Records]
i:66 [binder, in RecordSub]
i:69 [binder, in Records]
i:7 [binder, in RecordSub]
i:81 [binder, in RecordSub]
i:84 [binder, in RecordSub]
i:86 [binder, in Records]
i:90 [binder, in Records]
i:96 [binder, in RecordSub]
i:98 [binder, in Records]
J
j:190 [binder, in Sub]j:194 [binder, in Sub]
K
keval [definition, in PE]keval_example [definition, in PE]
k:189 [binder, in Norm]
k:417 [binder, in PE]
k:431 [binder, in PE]
k:442 [binder, in PE]
k:448 [binder, in PE]
k:53 [binder, in UseAuto]
k:55 [binder, in UseAuto]
k:57 [binder, in UseAuto]
k:59 [binder, in UseAuto]
k:60 [binder, in UseAuto]
k:62 [binder, in UseAuto]
k:63 [binder, in UseAuto]
L
Label:410 [binder, in PE]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 [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_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_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_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 [constructor, in LibTactics]
Ltac_database_token [inductive, in LibTactics]
ltac_mark [constructor, in LibTactics]
ltac_Mark [inductive, in LibTactics]
ltac_wilds [constructor, in LibTactics]
ltac_Wilds [inductive, in LibTactics]
ltac_wild [constructor, in LibTactics]
ltac_Wild [inductive, in LibTactics]
ltac_no_arg [constructor, in LibTactics]
ltac_No_arg [inductive, in LibTactics]
l'':435 [binder, in PE]
l':433 [binder, in PE]
l':451 [binder, in PE]
l':462 [binder, in PE]
l':473 [binder, in PE]
l1:177 [binder, in Equiv]
l1:38 [binder, in References]
l2:178 [binder, in Equiv]
l2:39 [binder, in References]
l:104 [binder, in References]
l:11 [binder, in References]
l:11 [binder, in PE]
l:110 [binder, in References]
l:118 [binder, in UseAuto]
l:133 [binder, in PE]
l:137 [binder, in PE]
l:157 [binder, in References]
l:176 [binder, in References]
l:19 [binder, in PE]
l:190 [binder, in Norm]
l:192 [binder, in References]
l:195 [binder, in References]
l:207 [binder, in PE]
l:211 [binder, in PE]
l:226 [binder, in References]
l:238 [binder, in References]
l:24 [binder, in References]
l:326 [binder, in PE]
l:34 [binder, in References]
l:35 [binder, in References]
L:415 [binder, in PE]
L:420 [binder, in PE]
l:421 [binder, in PE]
L:423 [binder, in PE]
l:428 [binder, in PE]
l:430 [binder, in PE]
L:440 [binder, in PE]
L:445 [binder, in PE]
L:452 [binder, in PE]
L:456 [binder, in PE]
l:460 [binder, in PE]
L:467 [binder, in PE]
l:471 [binder, in PE]
l:84 [binder, in PE]
l:88 [binder, in PE]
M
manual_grade_for_eval__multistep_inf [definition, in Smallstep]manual_grade_for_hoare_repeat [definition, in Hoare]
manual_grade_for_hoare_asgn_wrong [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]
mkAexp [abbreviation, in Hoare]
MoreStlc [library]
msubst [definition, in Norm]
msubst_R [lemma, in Norm]
msubst_preserves_typing [lemma, in Norm]
msubst_app [lemma, in Norm]
msubst_abs [lemma, in Norm]
msubst_var [lemma, in Norm]
msubst_closed [lemma, in Norm]
multi [inductive, in Smallstep]
multistep [abbreviation, in Norm]
multistep__eval [lemma, in Smallstep]
multistep_congr_2 [lemma, in Smallstep]
multistep_congr_1 [lemma, in Smallstep]
multistep_App2 [lemma, in Norm]
multistep_preserves_R' [lemma, in Norm]
multistep_preserves_R [lemma, in Norm]
multi_trans [lemma, in Smallstep]
multi_R [lemma, in Smallstep]
multi_step [constructor, in Smallstep]
multi_refl [constructor, in Smallstep]
mupdate [definition, in Norm]
mupdate_drop [lemma, in Norm]
mupdate_lookup [lemma, in Norm]
myFact [definition, in UseAuto]
m:107 [binder, in UseTactics]
m:150 [binder, in UseAuto]
m:153 [binder, in UseAuto]
m:21 [binder, in UseAuto]
m:33 [binder, in UseTactics]
m:338 [binder, in Smallstep]
m:342 [binder, in Smallstep]
m:346 [binder, in Smallstep]
m:35 [binder, in UseTactics]
m:37 [binder, in UseTactics]
m:47 [binder, in Hoare2]
m:49 [binder, in Hoare2]
m:55 [binder, in Hoare2]
m:57 [binder, in Hoare2]
m:59 [binder, in Hoare2]
m:60 [binder, in Hoare2]
m:63 [binder, in Hoare]
m:64 [binder, in Hoare2]
m:67 [binder, in Hoare2]
m:68 [binder, in Hoare2]
m:69 [binder, in Hoare2]
m:70 [binder, in Hoare2]
m:71 [binder, in Hoare2]
m:72 [binder, in Hoare]
m:79 [binder, in UseTactics]
m:8 [binder, in UseAuto]
m:81 [binder, in UseTactics]
m:83 [binder, in UseTactics]
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]
ni:136 [binder, in Equiv]
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]
nxs:195 [binder, in Norm]
n':379 [binder, in PE]
n':386 [binder, in PE]
n1:132 [binder, in PE]
n1:195 [binder, in LibTactics]
n1:206 [binder, in PE]
n1:332 [binder, in PE]
n1:354 [binder, in PE]
n1:43 [binder, in MoreStlc]
n1:71 [binder, in References]
n2:196 [binder, in LibTactics]
n2:333 [binder, in PE]
n2:355 [binder, in PE]
n2:44 [binder, in MoreStlc]
n2:72 [binder, in References]
n:10 [binder, in References]
n:100 [binder, in UseAuto]
n:103 [binder, in UseAuto]
n:103 [binder, in Hoare2]
n:104 [binder, in Hoare2]
n:105 [binder, in Hoare2]
n:106 [binder, in UseAuto]
n:106 [binder, in UseTactics]
n:107 [binder, in Hoare]
n:109 [binder, in UseAuto]
n:109 [binder, in Hoare]
n:11 [binder, in UseAuto]
n:121 [binder, in UseAuto]
n:123 [binder, in References]
n:123 [binder, in MoreStlc]
n:125 [binder, in Equiv]
n:126 [binder, in Hoare]
n:138 [binder, in PE]
n:142 [binder, in References]
n:144 [binder, in Equiv]
n:149 [binder, in UseAuto]
n:15 [binder, in MoreStlc]
n:151 [binder, in Smallstep]
n:152 [binder, in UseAuto]
n:154 [binder, in Smallstep]
n:157 [binder, in Smallstep]
n:159 [binder, in Smallstep]
n:164 [binder, in Smallstep]
n:174 [binder, in Hoare]
n:189 [binder, in Smallstep]
n:19 [binder, in References]
n:194 [binder, in Norm]
n:197 [binder, in Sub]
n:197 [binder, in LibTactics]
n:20 [binder, in UseAuto]
n:211 [binder, in Hoare]
n:212 [binder, in PE]
n:22 [binder, in References]
n:238 [binder, in Hoare]
n:24 [binder, in UseAuto]
n:253 [binder, in Smallstep]
n:256 [binder, in Hoare]
n:266 [binder, in Hoare]
n:27 [binder, in PE]
n:28 [binder, in UseAuto]
n:285 [binder, in Smallstep]
n:29 [binder, in UseAuto]
n:29 [binder, in References]
n:3 [binder, in UseAuto]
n:31 [binder, in Smallstep]
n:32 [binder, in References]
n:32 [binder, in UseTactics]
n:320 [binder, in Smallstep]
n:322 [binder, in Smallstep]
n:325 [binder, in Smallstep]
n:325 [binder, in PE]
n:331 [binder, in Smallstep]
n:337 [binder, in Smallstep]
n:339 [binder, in PE]
n:34 [binder, in UseTactics]
n:341 [binder, in Smallstep]
n:345 [binder, in Smallstep]
n:345 [binder, in PE]
n:359 [binder, in PE]
n:36 [binder, in UseTactics]
n:363 [binder, in PE]
n:375 [binder, in PE]
n:385 [binder, in PE]
n:39 [binder, in MoreStlc]
n:394 [binder, in PE]
n:4 [binder, in UseAuto]
n:402 [binder, in PE]
n:42 [binder, in MoreStlc]
n:48 [binder, in Hoare2]
n:50 [binder, in Hoare2]
n:55 [binder, in Smallstep]
n:57 [binder, in MoreStlc]
n:59 [binder, in References]
n:65 [binder, in UseAuto]
n:65 [binder, in References]
n:65 [binder, in PE]
n:68 [binder, in PE]
n:69 [binder, in UseTactics]
n:7 [binder, in UseAuto]
n:7 [binder, in PE]
n:70 [binder, in UseTactics]
n:71 [binder, in Smallstep]
n:71 [binder, in UseTactics]
n:73 [binder, in PE]
n:74 [binder, in Smallstep]
n:77 [binder, in PE]
n:78 [binder, in UseTactics]
n:8 [binder, in Smallstep]
n:80 [binder, in UseTactics]
n:82 [binder, in Hoare2]
n:82 [binder, in UseTactics]
n:85 [binder, in Hoare2]
n:86 [binder, in Smallstep]
n:86 [binder, in Hoare2]
n:87 [binder, in Hoare2]
n:88 [binder, in Hoare2]
n:9 [binder, in Hoare]
n:93 [binder, in References]
n:99 [binder, in Hoare2]
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 [inductive, in PE]
PE [library]
peval [inductive, in PE]
pe_st:470 [binder, in PE]
pe_program_correct [lemma, in PE]
pe_st':466 [binder, in PE]
pe_st:459 [binder, in PE]
pe_peval_intro [constructor, in PE]
pe_peval [inductive, in PE]
pe_l:454 [binder, in PE]
pe_program [definition, in PE]
pe_st':450 [binder, in PE]
pe_st:447 [binder, in PE]
pe_block_correct [lemma, in PE]
pe_block_example [definition, in PE]
pe_st:441 [binder, in PE]
pe_block [definition, in PE]
pe_st':405 [binder, in PE]
pe_st:404 [binder, in PE]
pe_st':397 [binder, in PE]
pe_st:396 [binder, in PE]
pe_st':389 [binder, in PE]
pe_st:388 [binder, in PE]
pe_st':381 [binder, in PE]
pe_st':371 [binder, in PE]
pe_st2:368 [binder, in PE]
pe_st1:367 [binder, in PE]
pe_st2:365 [binder, in PE]
pe_st1:364 [binder, in PE]
pe_st'':275 [binder, in PE]
pe_st':274 [binder, in PE]
pe_st:273 [binder, in PE]
pe_st'':268 [binder, in PE]
pe_st':267 [binder, in PE]
pe_st:266 [binder, in PE]
pe_st:263 [binder, in PE]
pe_st'':257 [binder, in PE]
pe_st':256 [binder, in PE]
pe_st:255 [binder, in PE]
pe_st'':249 [binder, in PE]
pe_st':248 [binder, in PE]
pe_st:247 [binder, in PE]
pe_st:244 [binder, in PE]
pe_st2:237 [binder, in PE]
pe_st1:236 [binder, in PE]
pe_st:235 [binder, in PE]
pe_st':229 [binder, in PE]
pe_st:228 [binder, in PE]
pe_st':222 [binder, in PE]
pe_st:221 [binder, in PE]
pe_st'':215 [binder, in PE]
pe_st':214 [binder, in PE]
pe_st:213 [binder, in PE]
pe_st:208 [binder, in PE]
pe_st:204 [binder, in PE]
pe_st:203 [binder, in PE]
pe_st':197 [binder, in PE]
pe_st:196 [binder, in PE]
pe_com_correct [lemma, in PE]
pe_st':191 [binder, in PE]
pe_st:190 [binder, in PE]
pe_com_sound [lemma, in PE]
pe_st':185 [binder, in PE]
pe_st:184 [binder, in PE]
pe_com_complete [lemma, in PE]
pe_st':177 [binder, 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_st2:160 [binder, in PE]
pe_st1:159 [binder, in PE]
pe_st:158 [binder, in PE]
pe_st':153 [binder, in PE]
pe_st:152 [binder, in PE]
pe_st':147 [binder, in PE]
pe_st:146 [binder, in PE]
pe_st'':141 [binder, in PE]
pe_st':140 [binder, in PE]
pe_st:139 [binder, in PE]
pe_st:134 [binder, in PE]
pe_st:130 [binder, in PE]
pe_st:129 [binder, 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_st:124 [binder, in PE]
pe_st:116 [binder, in PE]
pe_st:112 [binder, in PE]
pe_st:108 [binder, in PE]
pe_st2:106 [binder, in PE]
pe_st1:105 [binder, in PE]
pe_compare_update [lemma, in PE]
pe_st2:103 [binder, in PE]
pe_st1:102 [binder, in PE]
pe_compare_removes [lemma, in PE]
pe_st:99 [binder, in PE]
pe_removes_correct [lemma, in PE]
pe_st:95 [binder, in PE]
pe_removes [definition, in PE]
pe_st2:93 [binder, in PE]
pe_st1:92 [binder, in PE]
pe_compare_correct [lemma, in PE]
pe_st2:91 [binder, in PE]
pe_st1:90 [binder, in PE]
pe_compare [definition, in PE]
pe_unique_correct [lemma, in PE]
pe_unique [definition, in PE]
pe_st2:82 [binder, in PE]
pe_st1:81 [binder, in PE]
pe_disagree_domain [lemma, in PE]
pe_st2:79 [binder, in PE]
pe_st1:78 [binder, in PE]
pe_disagree_at [definition, in PE]
pe_st:75 [binder, in PE]
pe_update_update_add [lemma, in PE]
pe_st:71 [binder, in PE]
pe_update_update_remove [lemma, in PE]
pe_st:66 [binder, in PE]
pe_add_correct [lemma, in PE]
pe_st:63 [binder, in PE]
pe_add [definition, in PE]
pe_st:60 [binder, in PE]
pe_remove_correct [lemma, in PE]
pe_st:56 [binder, in PE]
pe_remove [definition, in PE]
pe_st:53 [binder, in PE]
pe_bexp_correct [lemma, in PE]
pe_st:48 [binder, in PE]
pe_bexp [definition, in PE]
pe_st:45 [binder, in PE]
pe_aexp_correct [lemma, in PE]
pe_st:43 [binder, in PE]
pe_consistent_update [lemma, in PE]
pe_st:41 [binder, in PE]
pe_update_consistent [lemma, in PE]
pe_st:38 [binder, in PE]
pe_update_correct [lemma, in PE]
pe_st:32 [binder, in PE]
pe_update [definition, in PE]
pe_st:29 [binder, in PE]
pe_aexp_correct_weak [lemma, in PE]
pe_st:25 [binder, in PE]
pe_consistent [definition, in PE]
pe_st:20 [binder, in PE]
pe_aexp [definition, in PE]
pe_st:5 [binder, in PE]
pe_domain [lemma, in PE]
pe_st:1 [binder, 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]
Postscript [library]
post_dec_while [definition, in Hoare2]
post_dec [definition, in Hoare2]
pow2 [definition, in Hoare2]
pow2_le_1 [lemma, in Hoare2]
pow2_plus_1 [lemma, in Hoare2]
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]
pre_dec_while [definition, in Hoare2]
pre_dec [definition, in Hoare2]
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]
P':157 [binder, in Hoare]
P':245 [binder, in Hoare]
P':31 [binder, in HoareAsLogic]
P':319 [binder, in Hoare]
P':38 [binder, in HoareAsLogic]
P':63 [binder, in HoareAsLogic]
P':74 [binder, in Hoare]
P':82 [binder, in Hoare]
P':87 [binder, in Hoare]
P':91 [binder, in Hoare]
P':92 [binder, in Hoare2]
P':95 [binder, in Hoare]
P':99 [binder, in Hoare]
P1:10 [binder, in Hoare2]
P2:12 [binder, in Hoare2]
P:1 [binder, in UseAuto]
P:1 [binder, in HoareAsLogic]
P:102 [binder, in Hoare]
P:105 [binder, in LibTactics]
P:109 [binder, in LibTactics]
P:114 [binder, in Hoare]
P:114 [binder, in LibTactics]
P:12 [binder, in HoareAsLogic]
P:133 [binder, in Sub]
P:148 [binder, in UseAuto]
P:151 [binder, in UseAuto]
P:151 [binder, in Hoare]
P:156 [binder, in Hoare]
P:16 [binder, in UseAuto]
P:16 [binder, in Hoare2]
P:16 [binder, in UseTactics]
P:163 [binder, in Hoare]
P:17 [binder, in HoareAsLogic]
P:19 [binder, in Hoare2]
P:190 [binder, in LibTactics]
p:191 [binder, in LibTactics]
P:192 [binder, in UseAuto]
P:198 [binder, in LibTactics]
P:199 [binder, in Hoare]
P:199 [binder, in LibTactics]
P:22 [binder, in UseAuto]
P:220 [binder, in Sub]
P:239 [binder, in Hoare]
P:24 [binder, in LibTactics]
P:24 [binder, in HoareAsLogic]
P:244 [binder, in Hoare]
P:25 [binder, in UseAuto]
P:253 [binder, in Hoare]
P:277 [binder, in LibTactics]
P:29 [binder, in HoareAsLogic]
P:303 [binder, in Hoare]
P:309 [binder, in Hoare]
P:312 [binder, in Hoare]
P:318 [binder, in Hoare]
P:322 [binder, in Hoare]
P:328 [binder, in Hoare]
p:332 [binder, in Smallstep]
P:333 [binder, in Hoare]
P:334 [binder, in Hoare]
p:335 [binder, in Smallstep]
p:339 [binder, in Smallstep]
P:339 [binder, in Hoare]
p:343 [binder, in Smallstep]
p:347 [binder, in Smallstep]
P:35 [binder, in Hoare]
P:36 [binder, in HoareAsLogic]
P:38 [binder, in Hoare2]
P:40 [binder, in Hoare]
P:41 [binder, in HoareAsLogic]
p:424 [binder, in PE]
P:43 [binder, in Hoare2]
P:44 [binder, in UseAuto]
P:44 [binder, in Hoare]
p:453 [binder, in PE]
p:457 [binder, in PE]
P:46 [binder, in UseAuto]
p:468 [binder, in PE]
P:48 [binder, in Hoare]
P:49 [binder, in Hoare]
P:49 [binder, in HoareAsLogic]
P:5 [binder, in UseAuto]
P:5 [binder, in Hoare]
P:51 [binder, in UseAuto]
P:52 [binder, in UseAuto]
P:52 [binder, in HoareAsLogic]
P:54 [binder, in UseAuto]
P:55 [binder, in LibTactics]
P:56 [binder, in UseAuto]
P:56 [binder, in Hoare]
p:56 [binder, in Hoare2]
P:57 [binder, in LibTactics]
P:58 [binder, in UseAuto]
p:58 [binder, in Hoare2]
P:58 [binder, in UseTactics]
P:6 [binder, in UseTactics]
P:61 [binder, in UseAuto]
P:61 [binder, in Hoare]
P:62 [binder, in Hoare]
P:62 [binder, in UseTactics]
P:62 [binder, in LibTactics]
P:64 [binder, in HoareAsLogic]
P:65 [binder, in Hoare]
P:68 [binder, in LibTactics]
P:69 [binder, in Hoare]
P:71 [binder, in HoareAsLogic]
P:73 [binder, in Hoare]
P:76 [binder, in LibTactics]
P:77 [binder, in Hoare]
P:8 [binder, in Hoare]
P:8 [binder, in HoareAsLogic]
P:81 [binder, in Hoare]
P:86 [binder, in Hoare]
P:86 [binder, in LibTactics]
P:89 [binder, in Hoare2]
P:9 [binder, in UseAuto]
P:90 [binder, in Hoare]
P:94 [binder, in Hoare]
P:96 [binder, in Hoare2]
P:98 [binder, in Hoare]
P:98 [binder, in LibTactics]
Q
Q':104 [binder, in Hoare]Q':32 [binder, in HoareAsLogic]
Q':324 [binder, in Hoare]
Q':43 [binder, in HoareAsLogic]
Q':79 [binder, in Hoare]
Q':84 [binder, in Hoare]
Q:100 [binder, in Hoare]
Q:103 [binder, in Hoare]
Q:106 [binder, in LibTactics]
Q:110 [binder, in LibTactics]
Q:115 [binder, in Hoare]
Q:115 [binder, in LibTactics]
Q:14 [binder, in Hoare2]
Q:14 [binder, in HoareAsLogic]
Q:153 [binder, in Hoare]
Q:158 [binder, in Hoare]
Q:160 [binder, in Hoare]
Q:166 [binder, in Hoare]
Q:17 [binder, in UseAuto]
Q:17 [binder, in UseTactics]
Q:18 [binder, in Hoare2]
Q:18 [binder, in HoareAsLogic]
Q:2 [binder, in UseAuto]
Q:200 [binder, in LibTactics]
Q:201 [binder, in Hoare]
Q:22 [binder, in Hoare2]
Q:23 [binder, in UseAuto]
Q:241 [binder, in Hoare]
Q:246 [binder, in Hoare]
Q:249 [binder, in Hoare]
Q:251 [binder, in Hoare]
Q:26 [binder, in UseAuto]
Q:3 [binder, in Hoare2]
Q:3 [binder, in HoareAsLogic]
Q:30 [binder, in HoareAsLogic]
Q:305 [binder, in Hoare]
Q:311 [binder, in Hoare]
Q:314 [binder, in Hoare]
Q:315 [binder, in Hoare]
Q:320 [binder, in Hoare]
Q:323 [binder, in Hoare]
Q:329 [binder, in Hoare]
Q:335 [binder, in Hoare]
Q:37 [binder, in Hoare]
Q:37 [binder, in HoareAsLogic]
Q:41 [binder, in Hoare]
Q:42 [binder, in HoareAsLogic]
Q:45 [binder, in Hoare]
Q:50 [binder, in Hoare]
Q:51 [binder, in HoareAsLogic]
Q:54 [binder, in HoareAsLogic]
Q:56 [binder, in LibTactics]
Q:56 [binder, in HoareAsLogic]
Q:58 [binder, in Hoare]
Q:6 [binder, in UseAuto]
Q:6 [binder, in Hoare]
Q:60 [binder, in HoareAsLogic]
Q:62 [binder, in HoareAsLogic]
Q:65 [binder, in HoareAsLogic]
Q:7 [binder, in UseTactics]
Q:70 [binder, in HoareAsLogic]
Q:73 [binder, in HoareAsLogic]
Q:75 [binder, in Hoare]
Q:78 [binder, in Hoare]
Q:8 [binder, in Hoare2]
Q:83 [binder, in Hoare]
Q:88 [binder, in Hoare]
Q:9 [binder, in HoareAsLogic]
Q:91 [binder, in Hoare2]
Q:92 [binder, in Hoare]
Q:93 [binder, in Hoare2]
Q:96 [binder, in Hoare]
Q:97 [binder, in Hoare2]
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 [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 [inductive, 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.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.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_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_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.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 [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.CIf [constructor, in Hoare]
RepeatExercise.com [inductive, 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.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]
_ =[ _ ]=> _ [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]
R:122 [binder, in Smallstep]
R:130 [binder, in Smallstep]
R:134 [binder, in Smallstep]
R:141 [binder, in Smallstep]
R:16 [binder, in HoareAsLogic]
R:18 [binder, in UseAuto]
R:18 [binder, in UseTactics]
R:25 [binder, in Smallstep]
R:256 [binder, in References]
r:272 [binder, in Hoare]
r:277 [binder, in Hoare]
r:282 [binder, in Hoare]
r:291 [binder, in Hoare]
r:307 [binder, in Hoare]
R:330 [binder, in Hoare]
R:45 [binder, in Smallstep]
R:51 [binder, in Hoare]
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.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]
Si:103 [binder, in RecordSub]
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]
Sr2:87 [binder, in RecordSub]
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]
ss:180 [binder, in Norm]
ss:224 [binder, in Norm]
ss:232 [binder, in Norm]
ss:234 [binder, in Norm]
ss:238 [binder, in Norm]
stack [definition, in Smallstep]
stack_multistep [definition, in Smallstep]
stack_step_deterministic [lemma, 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_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]
stk:330 [binder, in Smallstep]
stk:333 [binder, in Smallstep]
stk:336 [binder, in Smallstep]
stk:340 [binder, in Smallstep]
stk:344 [binder, in Smallstep]
STLC [module, in Stlc]
Stlc [library]
STLCArith [module, in StlcProp]
STLCArith.context [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.subst [definition, in StlcProp]
STLCArith.tm [inductive, 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_Nat [constructor, in StlcProp]
STLCArith.Ty_Arrow [constructor, in StlcProp]
STLCArith.value [inductive, in StlcProp]
STLCArith.weakening [lemma, in StlcProp]
stlc:_ [notation, in StlcProp]
stlc:_ * _ [notation, in StlcProp]
stlc:_ _ [notation, in StlcProp]
stlc:_ -> _ [notation, in StlcProp]
stlc:if0 _ then _ else _ [notation, in StlcProp]
stlc:Nat [notation, in StlcProp]
stlc:pred _ [notation, in StlcProp]
stlc:succ _ [notation, in StlcProp]
stlc:( _ ) [notation, in StlcProp]
stlc:\ _ : _ , _ [notation, in StlcProp]
stlc:{ _ } [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.g [abbreviation, in Records]
STLCExtendedRecords.has_type__wf [lemma, 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 [inductive, 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.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_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_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.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 [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]
stlc_ty:nil [notation, in Records]
stlc_ty:_ : _ :: _ [notation, in Records]
stlc_ty:Base _ [notation, in Records]
stlc_ty:_ -> _ [notation, in Records]
stlc_ty:_ [notation, in Records]
stlc_ty:( _ ) [notation, in Records]
stlc:_ [notation, in Records]
stlc:_ --> _ [notation, in Records]
stlc:_ := _ :: _ [notation, in Records]
stlc:_ _ [notation, in Records]
stlc:nil [notation, in Records]
stlc:( _ ) [notation, in Records]
stlc:[ _ := _ ] _ [notation, in Records]
stlc:\ _ : _ , _ [notation, in Records]
stlc:{ _ } [notation, in Records]
_ ⊢ _ ∈ _ [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.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 [inductive, in MoreStlc]
STLCExtended.multistep [abbreviation, in MoreStlc]
STLCExtended.preservation [lemma, in MoreStlc]
STLCExtended.progress [lemma, in MoreStlc]
STLCExtended.step [inductive, 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.substitution_preserves_typing [lemma, in MoreStlc]
STLCExtended.tm [inductive, 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_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.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.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_ty:Unit [notation, in MoreStlc]
stlc_ty:List _ [notation, in MoreStlc]
stlc_ty:_ * _ [notation, in MoreStlc]
stlc_ty:_ + _ [notation, in MoreStlc]
stlc_ty:Nat [notation, in MoreStlc]
stlc_ty:_ -> _ [notation, in MoreStlc]
stlc_ty:_ [notation, in MoreStlc]
stlc_ty:( _ ) [notation, in MoreStlc]
stlc:_ [notation, in MoreStlc]
stlc:_ :: _ [notation, in MoreStlc]
stlc:_ .snd [notation, in MoreStlc]
stlc:_ .fst [notation, in MoreStlc]
stlc:_ * _ [notation, in MoreStlc]
stlc:_ _ [notation, in MoreStlc]
stlc:case _ of | nil => _ | _ :: _ => _ [notation, in MoreStlc]
stlc:case _ of | inl _ => _ | inr _ => _ [notation, in MoreStlc]
stlc:fix _ [notation, in MoreStlc]
stlc:if0 _ then _ else _ [notation, in MoreStlc]
stlc:inl _ _ [notation, in MoreStlc]
stlc:inr _ _ [notation, in MoreStlc]
stlc:let _ = _ in _ [notation, in MoreStlc]
stlc:nil _ [notation, in MoreStlc]
stlc:pred _ [notation, in MoreStlc]
stlc:succ _ [notation, in MoreStlc]
stlc:unit [notation, in MoreStlc]
stlc:( _ , _ ) [notation, in MoreStlc]
stlc:( _ ) [notation, in MoreStlc]
stlc:[ _ := _ ] _ [notation, in MoreStlc]
stlc:\ _ : _ , _ [notation, in MoreStlc]
stlc:{ _ } [notation, in MoreStlc]
_ ⊢ _ ∈ _ [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 [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_cons [constructor, in References]
STLCRef.extends_nil [constructor, 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 [inductive, in References]
_ / _ -->+ _ / _ [notation, in References]
STLCRef.replace [definition, in References]
STLCRef.replace_nil [lemma, in References]
STLCRef.step [inductive, 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_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_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.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:_ [notation, in References]
stlc:_ ; _ [notation, in References]
stlc:_ := _ [notation, in References]
stlc:_ * _ [notation, in References]
stlc:_ _ [notation, in References]
stlc:_ -> _ [notation, in References]
stlc:if0 _ then _ else _ [notation, in References]
stlc:loc _ [notation, in References]
stlc:Nat [notation, in References]
stlc:pred _ [notation, in References]
stlc:ref _ [notation, in References]
stlc:Ref _ [notation, in References]
stlc:succ _ [notation, in References]
stlc:unit [notation, in References]
stlc:Unit [notation, in References]
stlc:! _ [notation, in References]
stlc:( _ ) [notation, in References]
stlc:[ _ := _ ] _ [notation, in References]
stlc:\ _ : _ , _ [notation, in References]
stlc:{ _ } [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_smallest_2 [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_smallest_1 [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_4 [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_3 [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_2 [lemma, in Sub]
STLCSub.FormalThoughtExercises.formal_small_large_1 [lemma, 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.smallest [definition, in Sub]
STLCSub.FormalThoughtExercises.smallest_largest [definition, in Sub]
STLCSub.FormalThoughtExercises.TF [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.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.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_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_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.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:_ [notation, in Sub]
stlc:_ .snd [notation, in Sub]
stlc:_ .fst [notation, in Sub]
stlc:_ * _ [notation, in Sub]
stlc:_ _ [notation, in Sub]
stlc:_ -> _ [notation, in Sub]
stlc:Base _ [notation, in Sub]
stlc:Bool [notation, in Sub]
stlc:false [notation, in Sub]
stlc:if _ then _ else _ [notation, in Sub]
stlc:Top [notation, in Sub]
stlc:true [notation, in Sub]
stlc:unit [notation, in Sub]
stlc:Unit [notation, in Sub]
stlc:( _ , _ ) [notation, in Sub]
stlc:( _ ) [notation, in Sub]
stlc:[ _ := _ ] _ [notation, in Sub]
stlc:\ _ : _ , _ [notation, in Sub]
stlc:{ _ } [notation, in Sub]
_ ⊢ _ ∈ _ [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 [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.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.s_var1 [constructor, in Stlc]
STLC.tm [inductive, 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_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.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:_ [notation, in Stlc]
stlc:_ _ [notation, in Stlc]
stlc:_ -> _ [notation, in Stlc]
stlc:Bool [notation, in Stlc]
stlc:false [notation, in Stlc]
stlc:if _ then _ else _ [notation, in Stlc]
stlc:true [notation, in Stlc]
stlc:( _ ) [notation, in Stlc]
stlc:[ _ := _ ] _ [notation, in Stlc]
stlc:\ _ : _ , _ [notation, in Stlc]
_ ⊢ _ ∈ _ [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]
st'o:461 [binder, in PE]
st'o:472 [binder, in PE]
st'':132 [binder, in Hoare]
st'':148 [binder, in Hoare]
st'':150 [binder, in Equiv]
st'':166 [binder, in Equiv]
st'':179 [binder, in PE]
st'':180 [binder, in Hoare]
st'':188 [binder, in PE]
st'':194 [binder, in PE]
st'':196 [binder, in Hoare]
st'':200 [binder, in PE]
st'':217 [binder, in Hoare]
st'':233 [binder, in Hoare]
st'':331 [binder, in PE]
st'':351 [binder, in PE]
st'':374 [binder, in PE]
st'':384 [binder, in PE]
st'':393 [binder, in PE]
st'':401 [binder, in PE]
st'':408 [binder, in PE]
st'':434 [binder, in PE]
st':10 [binder, in Equiv]
st':102 [binder, in References]
st':108 [binder, in References]
st':115 [binder, in UseAuto]
ST':116 [binder, in UseAuto]
st':116 [binder, in References]
st':121 [binder, in References]
st':130 [binder, in UseAuto]
ST':131 [binder, in UseAuto]
st':131 [binder, in Hoare]
st':134 [binder, in Hoare]
st':137 [binder, in UseAuto]
st':139 [binder, in Hoare]
st':14 [binder, in Equiv]
st':147 [binder, in Hoare]
st':149 [binder, in Equiv]
st':152 [binder, in Equiv]
st':155 [binder, in Hoare]
st':157 [binder, in Equiv]
st':165 [binder, in Equiv]
st':172 [binder, in Equiv]
st':173 [binder, in References]
st':174 [binder, in Equiv]
st':176 [binder, in Equiv]
st':179 [binder, in Hoare]
st':182 [binder, in Hoare]
st':182 [binder, in PE]
st':184 [binder, in Equiv]
st':185 [binder, in References]
st':187 [binder, in Hoare]
ST':188 [binder, in References]
ST':190 [binder, in References]
ST':194 [binder, in References]
st':195 [binder, in Hoare]
ST':197 [binder, in References]
st':203 [binder, in Hoare]
st':206 [binder, in References]
ST':207 [binder, in References]
st':216 [binder, in Hoare]
st':219 [binder, in Hoare]
st':224 [binder, in Hoare]
ST':230 [binder, in References]
st':232 [binder, in Hoare]
st':243 [binder, in Hoare]
st':246 [binder, in References]
ST':247 [binder, in References]
st':253 [binder, in References]
st':257 [binder, in Smallstep]
st':271 [binder, in Hoare]
st':289 [binder, in Smallstep]
st':290 [binder, in Hoare]
st':308 [binder, in Hoare]
st':311 [binder, in Smallstep]
st':316 [binder, in Smallstep]
st':318 [binder, in Smallstep]
st':319 [binder, in Smallstep]
st':324 [binder, in Smallstep]
st':326 [binder, in Smallstep]
st':326 [binder, in Hoare]
st':327 [binder, in Hoare]
st':33 [binder, in Equiv]
st':330 [binder, in PE]
st':335 [binder, in PE]
st':341 [binder, in PE]
st':350 [binder, in PE]
st':358 [binder, in PE]
st':362 [binder, in PE]
st':378 [binder, in PE]
st':39 [binder, in Hoare]
st':409 [binder, in PE]
st':432 [binder, in PE]
st':449 [binder, in PE]
st':465 [binder, in PE]
st':5 [binder, in HoareAsLogic]
st':53 [binder, in References]
st':58 [binder, in References]
st':64 [binder, in References]
st':70 [binder, in References]
st':74 [binder, in Equiv]
st':78 [binder, in References]
st':80 [binder, in Equiv]
st':83 [binder, in References]
st':89 [binder, in References]
st1:121 [binder, in PE]
st1:13 [binder, in UseTactics]
ST1:178 [binder, in References]
st1:24 [binder, in UseTactics]
st1:28 [binder, in UseTactics]
st1:3 [binder, in UseTactics]
st1:68 [binder, in UseAuto]
st1:72 [binder, in UseAuto]
st1:76 [binder, in UseAuto]
st1:80 [binder, in UseAuto]
st1:84 [binder, in UseAuto]
st1:88 [binder, in UseTactics]
st1:92 [binder, in UseTactics]
st2:122 [binder, in PE]
st2:14 [binder, in UseTactics]
ST2:179 [binder, in References]
st2:25 [binder, in UseTactics]
st2:29 [binder, in UseTactics]
st2:4 [binder, in UseTactics]
st2:69 [binder, in UseAuto]
st2:73 [binder, in UseAuto]
st2:77 [binder, in UseAuto]
st2:81 [binder, in UseAuto]
st2:85 [binder, in UseAuto]
st2:89 [binder, in UseTactics]
st2:93 [binder, in UseTactics]
st:1 [binder, in Hoare]
st:101 [binder, in References]
st:103 [binder, in References]
st:107 [binder, in References]
st:107 [binder, in PE]
st:11 [binder, in Hoare]
ST:110 [binder, in UseAuto]
st:111 [binder, in Hoare]
st:111 [binder, in References]
st:113 [binder, in Hoare]
st:114 [binder, in UseAuto]
st:114 [binder, in PE]
st:115 [binder, in References]
st:118 [binder, in PE]
st:12 [binder, in Hoare]
st:12 [binder, in UseTactics]
st:120 [binder, in References]
st:120 [binder, in PE]
st:122 [binder, in UseAuto]
ST:123 [binder, in UseAuto]
st:123 [binder, in Hoare]
st:124 [binder, in Hoare]
ST:124 [binder, in References]
ST:125 [binder, in UseAuto]
ST:125 [binder, in References]
st:126 [binder, in PE]
st:129 [binder, in UseAuto]
st:13 [binder, in Hoare]
st:13 [binder, in Equiv]
st:130 [binder, in Hoare]
ST:132 [binder, in UseAuto]
st:133 [binder, in Hoare]
st:134 [binder, in Equiv]
st:135 [binder, in UseAuto]
st:138 [binder, in Hoare]
st:14 [binder, in Hoare]
st:141 [binder, in Equiv]
st:142 [binder, in Equiv]
st:144 [binder, in Hoare]
st:146 [binder, in Hoare]
st:148 [binder, in Equiv]
st:15 [binder, in Hoare]
st:151 [binder, in Equiv]
st:154 [binder, in Hoare]
st:156 [binder, in Equiv]
st:16 [binder, in Hoare]
st:162 [binder, in Equiv]
st:164 [binder, in Equiv]
st:167 [binder, in PE]
ST:168 [binder, in References]
st:169 [binder, in PE]
st:17 [binder, in Hoare]
st:171 [binder, in Hoare]
st:171 [binder, in References]
st:171 [binder, in Equiv]
st:171 [binder, in PE]
st:172 [binder, in Hoare]
st:173 [binder, in Equiv]
st:173 [binder, in PE]
ST:174 [binder, in References]
st:175 [binder, in References]
st:175 [binder, in Equiv]
st:175 [binder, in PE]
st:177 [binder, in References]
st:178 [binder, in Hoare]
st:178 [binder, in PE]
st:18 [binder, in Hoare]
ST:180 [binder, in References]
st:181 [binder, in Hoare]
st:183 [binder, in References]
st:183 [binder, in Equiv]
st:186 [binder, in Hoare]
st:187 [binder, in PE]
st:19 [binder, in Hoare]
st:190 [binder, in Smallstep]
ST:191 [binder, in References]
st:192 [binder, in Hoare]
ST:193 [binder, in References]
st:193 [binder, in PE]
st:194 [binder, in Hoare]
ST:196 [binder, in References]
ST:198 [binder, in References]
st:199 [binder, in PE]
st:2 [binder, in Hoare]
st:2 [binder, in UseTactics]
st:20 [binder, in Hoare]
st:20 [binder, in References]
ST:200 [binder, in References]
ST:201 [binder, in References]
st:202 [binder, in Hoare]
st:205 [binder, in References]
st:208 [binder, in Hoare]
st:209 [binder, in Hoare]
st:21 [binder, in Hoare]
ST:210 [binder, in References]
ST:214 [binder, in References]
st:215 [binder, in Hoare]
st:218 [binder, in Smallstep]
st:218 [binder, in Hoare]
ST:218 [binder, in References]
st:22 [binder, in Hoare]
st:22 [binder, in HoareAsLogic]
st:223 [binder, in Hoare]
ST:224 [binder, in References]
st:225 [binder, in References]
st:229 [binder, in Hoare]
ST:229 [binder, in References]
st:23 [binder, in Hoare]
st:23 [binder, in UseTactics]
st:23 [binder, in HoareAsLogic]
st:231 [binder, in Hoare]
ST:233 [binder, in References]
st:234 [binder, in References]
st:236 [binder, in Hoare]
st:24 [binder, in Hoare]
st:24 [binder, in PE]
ST:241 [binder, in References]
st:242 [binder, in Hoare]
st:245 [binder, in References]
st:247 [binder, in Smallstep]
ST:248 [binder, in References]
st:25 [binder, in Hoare]
st:250 [binder, in Hoare]
st:251 [binder, in Smallstep]
st:251 [binder, in References]
st:254 [binder, in Smallstep]
st:255 [binder, in Hoare]
st:259 [binder, in Smallstep]
st:261 [binder, in Smallstep]
st:263 [binder, in Hoare]
st:264 [binder, in Hoare]
st:266 [binder, in Smallstep]
st:269 [binder, in Smallstep]
st:27 [binder, in UseTactics]
st:27 [binder, in HoareAsLogic]
st:270 [binder, in Hoare]
st:272 [binder, in Smallstep]
st:275 [binder, in Hoare]
st:276 [binder, in Hoare]
st:279 [binder, in Smallstep]
st:28 [binder, in PE]
st:28 [binder, in HoareAsLogic]
st:281 [binder, in Hoare]
st:281 [binder, in PE]
st:283 [binder, in Smallstep]
st:283 [binder, in PE]
st:285 [binder, in PE]
st:286 [binder, in Smallstep]
st:287 [binder, in Hoare]
st:287 [binder, in PE]
st:289 [binder, in Hoare]
st:289 [binder, in PE]
st:29 [binder, in Hoare]
st:291 [binder, in Smallstep]
st:291 [binder, in PE]
st:293 [binder, in Smallstep]
st:293 [binder, in PE]
st:294 [binder, in Hoare]
st:295 [binder, in PE]
st:297 [binder, in Hoare]
st:297 [binder, in PE]
st:298 [binder, in Smallstep]
st:299 [binder, in Hoare]
st:299 [binder, in PE]
st:3 [binder, in Hoare]
st:3 [binder, in Equiv]
st:301 [binder, in Smallstep]
st:301 [binder, in Hoare]
st:301 [binder, in PE]
st:303 [binder, in PE]
st:304 [binder, in Smallstep]
st:305 [binder, in PE]
st:306 [binder, in Hoare]
st:307 [binder, in Smallstep]
st:307 [binder, in PE]
st:309 [binder, in PE]
st:31 [binder, in PE]
st:311 [binder, in PE]
st:312 [binder, in Smallstep]
st:313 [binder, in PE]
st:315 [binder, in PE]
st:317 [binder, in Smallstep]
st:317 [binder, in PE]
st:319 [binder, in PE]
st:32 [binder, in Equiv]
st:321 [binder, in Smallstep]
st:322 [binder, in PE]
st:323 [binder, in Smallstep]
st:323 [binder, in PE]
st:327 [binder, in Smallstep]
st:329 [binder, in PE]
st:334 [binder, in PE]
st:34 [binder, in Hoare]
st:34 [binder, in HoareAsLogic]
st:340 [binder, in PE]
st:347 [binder, in PE]
st:348 [binder, in Smallstep]
st:349 [binder, in Smallstep]
st:349 [binder, in PE]
st:35 [binder, in HoareAsLogic]
st:357 [binder, in PE]
st:361 [binder, in PE]
st:369 [binder, in PE]
st:37 [binder, in References]
st:37 [binder, in PE]
st:373 [binder, in PE]
st:38 [binder, in Hoare]
st:383 [binder, in PE]
st:392 [binder, in PE]
st:4 [binder, in Hoare]
st:4 [binder, in HoareAsLogic]
st:40 [binder, in PE]
st:40 [binder, in HoareAsLogic]
st:400 [binder, in PE]
st:407 [binder, in PE]
st:41 [binder, in References]
st:416 [binder, in PE]
st:42 [binder, in PE]
st:427 [binder, in PE]
st:429 [binder, in PE]
st:43 [binder, in Hoare]
st:436 [binder, in PE]
st:437 [binder, in PE]
st:438 [binder, in PE]
st:439 [binder, in PE]
st:446 [binder, in PE]
st:45 [binder, in HoareAsLogic]
st:458 [binder, in PE]
st:46 [binder, in HoareAsLogic]
st:469 [binder, in PE]
st:47 [binder, in Hoare]
st:47 [binder, in PE]
st:47 [binder, in HoareAsLogic]
st:48 [binder, in References]
st:52 [binder, in References]
st:55 [binder, in PE]
st:57 [binder, in Hoare]
st:57 [binder, in References]
st:6 [binder, in Equiv]
st:60 [binder, in References]
st:63 [binder, in References]
st:66 [binder, in Hoare]
st:66 [binder, in References]
st:67 [binder, in UseAuto]
st:67 [binder, in Hoare]
st:68 [binder, in UseTactics]
st:69 [binder, in References]
st:7 [binder, in Hoare]
st:70 [binder, in Hoare]
st:70 [binder, in PE]
st:71 [binder, in UseAuto]
st:71 [binder, in Hoare]
st:73 [binder, in References]
st:73 [binder, in Equiv]
st:74 [binder, in PE]
st:75 [binder, in UseAuto]
st:77 [binder, in References]
st:79 [binder, in UseAuto]
st:79 [binder, in Equiv]
st:82 [binder, in References]
st:83 [binder, in UseAuto]
st:87 [binder, in UseTactics]
st:88 [binder, in References]
st:9 [binder, in Equiv]
st:91 [binder, in UseTactics]
st:92 [binder, in References]
st:96 [binder, in References]
st:98 [binder, in References]
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]
s':58 [binder, in HoareAsLogic]
S1:113 [binder, in Sub]
S1:139 [binder, in UseAuto]
S1:144 [binder, in UseAuto]
S1:155 [binder, in RecordSub]
S1:162 [binder, in RecordSub]
S1:167 [binder, in RecordSub]
S1:174 [binder, in Sub]
S1:178 [binder, in Sub]
S1:182 [binder, in Sub]
S1:186 [binder, in Sub]
S1:42 [binder, in Sub]
S1:77 [binder, in RecordSub]
S1:85 [binder, in RecordSub]
S1:88 [binder, in Sub]
S1:97 [binder, in Sub]
S2:100 [binder, in Sub]
s2:114 [binder, in Sub]
s2:140 [binder, in UseAuto]
s2:145 [binder, in UseAuto]
s2:156 [binder, in RecordSub]
S2:165 [binder, in RecordSub]
s2:168 [binder, in RecordSub]
S2:175 [binder, in Sub]
S2:179 [binder, in Sub]
S2:183 [binder, in Sub]
S2:187 [binder, in Sub]
S2:43 [binder, in Sub]
S2:78 [binder, in RecordSub]
s2:89 [binder, in Sub]
S:104 [binder, in Sub]
s:11 [binder, in Stlc]
s:13 [binder, in References]
S:131 [binder, in RecordSub]
S:134 [binder, in Sub]
S:138 [binder, in Sub]
S:142 [binder, in Sub]
S:143 [binder, in Norm]
S:146 [binder, in Sub]
s:15 [binder, in Stlc]
S:150 [binder, in Sub]
s:151 [binder, in RecordSub]
S:154 [binder, in Sub]
S:158 [binder, in Sub]
s:161 [binder, in Norm]
S:162 [binder, in Sub]
S:164 [binder, in Sub]
S:166 [binder, in Sub]
S:167 [binder, in Sub]
S:169 [binder, in Sub]
S:171 [binder, in UseAuto]
S:171 [binder, in Sub]
S:175 [binder, in UseAuto]
S:181 [binder, in UseAuto]
s:19 [binder, in Stlc]
S:198 [binder, in Sub]
S:219 [binder, in Sub]
S:224 [binder, in Sub]
s:24 [binder, in RecordSub]
S:269 [binder, in Norm]
s:27 [binder, in Records]
S:38 [binder, in Sub]
S:41 [binder, in Sub]
s:57 [binder, in HoareAsLogic]
s:6 [binder, in MoreStlc]
s:6 [binder, in Norm]
s:6 [binder, in Sub]
S:67 [binder, in Stlc]
S:73 [binder, in RecordSub]
S:76 [binder, in RecordSub]
s:81 [binder, in Sub]
s:84 [binder, in StlcProp]
s:84 [binder, in Sub]
s:91 [binder, in Sub]
S:94 [binder, in RecordSub]
S:97 [binder, in UseTactics]
S:99 [binder, in RecordSub]
T
T [definition, in Hoare2]tass [definition, in Norm]
Temp1 [module, in Smallstep]
Temp1.step [inductive, 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.v_funny [constructor, in Smallstep]
Temp1.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp2 [module, in Smallstep]
Temp2.step [inductive, 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.v_const [constructor, in Smallstep]
_ --> _ [notation, in Smallstep]
Temp3 [module, in Smallstep]
Temp3.step [inductive, 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.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]