| 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 | (2374 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 | (252 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 | (82 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 | (7 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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 | (1040 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 | (200 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 | (215 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 | (27 entries) |
| Projection 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 | (2 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 | (12 entries) |
| Instance 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 | (5 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 | (510 entries) |
| Record 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 | (1 entry) |
Global Index
A
acclength [definition, in Repr]Affine [library]
agree [definition, in LibSepFmap]
agree_union_r_inv [lemma, in LibSepFmap]
agree_union_l_inv [lemma, in LibSepFmap]
agree_union_rr_inv_agree [lemma, in LibSepFmap]
agree_union_lr_inv_agree_agree [lemma, in LibSepFmap]
agree_union_rl_inv [lemma, in LibSepFmap]
agree_union_ll_inv [lemma, in LibSepFmap]
agree_union_lr [lemma, in LibSepFmap]
agree_union_r [lemma, in LibSepFmap]
agree_union_l [lemma, in LibSepFmap]
agree_empty_r [lemma, in LibSepFmap]
agree_empty_l [lemma, in LibSepFmap]
agree_of_disjoint [lemma, in LibSepFmap]
agree_sym [lemma, in LibSepFmap]
agree_refl [lemma, in LibSepFmap]
aliased_call [definition, in Basic]
AlternativeExistentialRule [module, in Triples]
AlternativeExistentialRule.triple_hexists_of_triple_hexists2 [lemma, in Triples]
AlternativeExistentialRule.triple_hexists2 [lemma, in Triples]
append [definition, in Repr]
Arrays [library]
B
BakedInFrame [module, in Triples]BakedInFrame.btriple [definition, in Triples]
BakedInFrame.btriple_iff_btriple_lowlevel [lemma, in Triples]
BakedInFrame.btriple_lowlevel [definition, in Triples]
BakedInFrame.btriple_frame [lemma, in Triples]
BakedInFrame.eval [axiom, in Triples]
BakedInFrame.hoare [definition, in Triples]
BakedInFrame.hoare_conseq [lemma, in Triples]
Basic [library]
Bib [library]
big [inductive, in Triples]
big_sind [definition, in Triples]
big_ind [definition, in Triples]
big_free [constructor, in Triples]
big_set [constructor, in Triples]
big_get [constructor, in Triples]
big_ref [constructor, in Triples]
big_rand [constructor, in Triples]
big_div [constructor, in Triples]
big_add [constructor, in Triples]
big_if [constructor, in Triples]
big_let [constructor, in Triples]
big_seq [constructor, in Triples]
big_app_fix [constructor, in Triples]
big_app_fun [constructor, in Triples]
big_fix [constructor, in Triples]
big_fun [constructor, in Triples]
big_val [constructor, in Triples]
C
conseq [definition, in LibSepFmap]conseq_fresh [lemma, in LibSepFmap]
conseq_cons' [lemma, in LibSepFmap]
conseq_cons [lemma, in LibSepFmap]
conseq_nil [lemma, in LibSepFmap]
correct [definition, in Triples]
correct [definition, in LibSepReference]
CounterSpec [definition, in Repr]
cps_append [definition, in Repr]
cps_append_aux [definition, in Repr]
cps_facto [definition, in Repr]
cps_facto_aux [definition, in Repr]
create_counter [definition, in Repr]
ctx [definition, in LibSepReference]
ctx [definition, in WPgen]
CtxOps [section, in LibSepReference]
ctx_disjoint_equiv_app [lemma, in LibSepReference]
ctx_disjoint_rem [lemma, in LibSepReference]
ctx_equiv_rem [lemma, in LibSepReference]
ctx_equiv [definition, in LibSepReference]
ctx_disjoint [definition, in LibSepReference]
D
DefinitionsForVariables [module, in LibSepVar]DefinitionsForVariables.a [definition, in LibSepVar]
DefinitionsForVariables.a1 [definition, in LibSepVar]
DefinitionsForVariables.a2 [definition, in LibSepVar]
DefinitionsForVariables.a3 [definition, in LibSepVar]
DefinitionsForVariables.b [definition, in LibSepVar]
DefinitionsForVariables.b1 [definition, in LibSepVar]
DefinitionsForVariables.b2 [definition, in LibSepVar]
DefinitionsForVariables.b3 [definition, in LibSepVar]
DefinitionsForVariables.c [definition, in LibSepVar]
DefinitionsForVariables.c1 [definition, in LibSepVar]
DefinitionsForVariables.c2 [definition, in LibSepVar]
DefinitionsForVariables.c3 [definition, in LibSepVar]
DefinitionsForVariables.d [definition, in LibSepVar]
DefinitionsForVariables.d1 [definition, in LibSepVar]
DefinitionsForVariables.d2 [definition, in LibSepVar]
DefinitionsForVariables.d3 [definition, in LibSepVar]
DefinitionsForVariables.e [definition, in LibSepVar]
DefinitionsForVariables.e1 [definition, in LibSepVar]
DefinitionsForVariables.e2 [definition, in LibSepVar]
DefinitionsForVariables.e3 [definition, in LibSepVar]
DefinitionsForVariables.f [definition, in LibSepVar]
DefinitionsForVariables.f1 [definition, in LibSepVar]
DefinitionsForVariables.f2 [definition, in LibSepVar]
DefinitionsForVariables.f3 [definition, in LibSepVar]
DefinitionsForVariables.g [definition, in LibSepVar]
DefinitionsForVariables.g1 [definition, in LibSepVar]
DefinitionsForVariables.g2 [definition, in LibSepVar]
DefinitionsForVariables.g3 [definition, in LibSepVar]
DefinitionsForVariables.h [definition, in LibSepVar]
DefinitionsForVariables.h1 [definition, in LibSepVar]
DefinitionsForVariables.h2 [definition, in LibSepVar]
DefinitionsForVariables.h3 [definition, in LibSepVar]
DefinitionsForVariables.i [definition, in LibSepVar]
DefinitionsForVariables.i1 [definition, in LibSepVar]
DefinitionsForVariables.i2 [definition, in LibSepVar]
DefinitionsForVariables.i3 [definition, in LibSepVar]
DefinitionsForVariables.j [definition, in LibSepVar]
DefinitionsForVariables.j1 [definition, in LibSepVar]
DefinitionsForVariables.j2 [definition, in LibSepVar]
DefinitionsForVariables.j3 [definition, in LibSepVar]
DefinitionsForVariables.k [definition, in LibSepVar]
DefinitionsForVariables.k1 [definition, in LibSepVar]
DefinitionsForVariables.k2 [definition, in LibSepVar]
DefinitionsForVariables.k3 [definition, in LibSepVar]
DefinitionsForVariables.l [definition, in LibSepVar]
DefinitionsForVariables.l1 [definition, in LibSepVar]
DefinitionsForVariables.l2 [definition, in LibSepVar]
DefinitionsForVariables.l3 [definition, in LibSepVar]
DefinitionsForVariables.m [definition, in LibSepVar]
DefinitionsForVariables.m1 [definition, in LibSepVar]
DefinitionsForVariables.m2 [definition, in LibSepVar]
DefinitionsForVariables.m3 [definition, in LibSepVar]
DefinitionsForVariables.n [definition, in LibSepVar]
DefinitionsForVariables.n1 [definition, in LibSepVar]
DefinitionsForVariables.n2 [definition, in LibSepVar]
DefinitionsForVariables.n3 [definition, in LibSepVar]
DefinitionsForVariables.o [definition, in LibSepVar]
DefinitionsForVariables.o1 [definition, in LibSepVar]
DefinitionsForVariables.o2 [definition, in LibSepVar]
DefinitionsForVariables.o3 [definition, in LibSepVar]
DefinitionsForVariables.p [definition, in LibSepVar]
DefinitionsForVariables.p1 [definition, in LibSepVar]
DefinitionsForVariables.p2 [definition, in LibSepVar]
DefinitionsForVariables.p3 [definition, in LibSepVar]
DefinitionsForVariables.q [definition, in LibSepVar]
DefinitionsForVariables.q1 [definition, in LibSepVar]
DefinitionsForVariables.q2 [definition, in LibSepVar]
DefinitionsForVariables.q3 [definition, in LibSepVar]
DefinitionsForVariables.r [definition, in LibSepVar]
DefinitionsForVariables.r1 [definition, in LibSepVar]
DefinitionsForVariables.r2 [definition, in LibSepVar]
DefinitionsForVariables.r3 [definition, in LibSepVar]
DefinitionsForVariables.s [definition, in LibSepVar]
DefinitionsForVariables.s1 [definition, in LibSepVar]
DefinitionsForVariables.s2 [definition, in LibSepVar]
DefinitionsForVariables.s3 [definition, in LibSepVar]
DefinitionsForVariables.t [definition, in LibSepVar]
DefinitionsForVariables.t1 [definition, in LibSepVar]
DefinitionsForVariables.t2 [definition, in LibSepVar]
DefinitionsForVariables.t3 [definition, in LibSepVar]
DefinitionsForVariables.u [definition, in LibSepVar]
DefinitionsForVariables.u1 [definition, in LibSepVar]
DefinitionsForVariables.u2 [definition, in LibSepVar]
DefinitionsForVariables.u3 [definition, in LibSepVar]
DefinitionsForVariables.v [definition, in LibSepVar]
DefinitionsForVariables.v1 [definition, in LibSepVar]
DefinitionsForVariables.v2 [definition, in LibSepVar]
DefinitionsForVariables.v3 [definition, in LibSepVar]
DefinitionsForVariables.w [definition, in LibSepVar]
DefinitionsForVariables.w1 [definition, in LibSepVar]
DefinitionsForVariables.w2 [definition, in LibSepVar]
DefinitionsForVariables.w3 [definition, in LibSepVar]
DefinitionsForVariables.x [definition, in LibSepVar]
DefinitionsForVariables.x1 [definition, in LibSepVar]
DefinitionsForVariables.x2 [definition, in LibSepVar]
DefinitionsForVariables.x3 [definition, in LibSepVar]
DefinitionsForVariables.y [definition, in LibSepVar]
DefinitionsForVariables.y1 [definition, in LibSepVar]
DefinitionsForVariables.y2 [definition, in LibSepVar]
DefinitionsForVariables.y3 [definition, in LibSepVar]
DefinitionsForVariables.z [definition, in LibSepVar]
DefinitionsForVariables.z1 [definition, in LibSepVar]
DefinitionsForVariables.z2 [definition, in LibSepVar]
DefinitionsForVariables.z3 [definition, in LibSepVar]
DemoPrograms [module, in LibSepReference]
DemoPrograms.decr [definition, in LibSepReference]
DemoPrograms.Def_myfun.myfun [definition, in LibSepReference]
DemoPrograms.Def_myfun [module, in LibSepReference]
DemoPrograms.Def_myrec.triple_myrec [lemma, in LibSepReference]
DemoPrograms.Def_myrec.myrec [definition, in LibSepReference]
DemoPrograms.Def_myrec [module, in LibSepReference]
DemoPrograms.Def_mysucc.mysucc [definition, in LibSepReference]
DemoPrograms.Def_mysucc [module, in LibSepReference]
DemoPrograms.Def_decr.decr [definition, in LibSepReference]
DemoPrograms.Def_decr [module, in LibSepReference]
DemoPrograms.Def_incr.incr' [definition, in LibSepReference]
DemoPrograms.Def_incr [module, in LibSepReference]
DemoPrograms.incr [definition, in LibSepReference]
DemoPrograms.myfield [definition, in LibSepReference]
DemoPrograms.project_32_rec [definition, in LibSepReference]
DemoPrograms.project_32 [definition, in LibSepReference]
DemoPrograms.triple_project_32_rec [lemma, in LibSepReference]
DemoPrograms.triple_project_32 [lemma, in LibSepReference]
DemoPrograms.triple_myfun [lemma, in LibSepReference]
DemoPrograms.triple_mysucc [lemma, in LibSepReference]
DemoPrograms.triple_decr [lemma, in LibSepReference]
DemoPrograms.triple_incr' [lemma, in LibSepReference]
DemoPrograms.triple_incr [lemma, in LibSepReference]
demo_hrecord_intro_elim [lemma, in Records]
disjoint [definition, in LibSepFmap]
DisjointHints [module, in LibSepFmap]
disjoint_single_conseq [lemma, in LibSepFmap]
disjoint_demo [lemma, in LibSepFmap]
disjoint_remove_l [lemma, in LibSepFmap]
disjoint_update_not_r [lemma, in LibSepFmap]
disjoint_update_l [lemma, in LibSepFmap]
disjoint_single_set [lemma, in LibSepFmap]
disjoint_3_unfold [lemma, in LibSepFmap]
disjoint_single_single_same_inv [lemma, in LibSepFmap]
disjoint_single_single [lemma, in LibSepFmap]
disjoint_union_eq_l [lemma, in LibSepFmap]
disjoint_union_eq_r [lemma, in LibSepFmap]
disjoint_empty_r [lemma, in LibSepFmap]
disjoint_empty_l [lemma, in LibSepFmap]
disjoint_comm [lemma, in LibSepFmap]
disjoint_sym [lemma, in LibSepFmap]
disjoint_single_of_not_indom [lemma, in LibSepFmap]
disjoint_inv_not_indom_both [lemma, in LibSepFmap]
disjoint_of_not_indom_both [lemma, in LibSepFmap]
disjoint_eq' [lemma, in LibSepFmap]
disjoint_eq [lemma, in LibSepFmap]
disjoint_3 [definition, in LibSepFmap]
DivSpec [module, in Rules]
DivSpec.triple_div_from_triple_div' [lemma, in Rules]
DivSpec.triple_div'_from_triple_div [lemma, in Rules]
DivSpec.triple_div' [axiom, in Rules]
DivSpec.triple_div [axiom, in Rules]
dummy_char [definition, in LibSepVar]
E
empty [definition, in LibSepFmap]EntailmentRulesProofs [module, in Himpl]
EntailmentRulesProofs.himpl_frame_lr [lemma, in Himpl]
EntailmentRulesProofs.himpl_frame_r [lemma, in Himpl]
EntailmentRulesProofs.himpl_frame_l [lemma, in Himpl]
eq_inv_fmap_data_eq [lemma, in LibSepFmap]
eval [inductive, in Triples]
eval [inductive, in LibSepReference]
Eval [section, in LibSepReference]
eval [inductive, in LibSepMinimal]
evalbinop [inductive, in LibSepReference]
evalbinop_sind [definition, in LibSepReference]
evalbinop_ind [definition, in LibSepReference]
evalbinop_ptr_add [constructor, in LibSepReference]
evalbinop_gt [constructor, in LibSepReference]
evalbinop_ge [constructor, in LibSepReference]
evalbinop_lt [constructor, in LibSepReference]
evalbinop_le [constructor, in LibSepReference]
evalbinop_mod [constructor, in LibSepReference]
evalbinop_div [constructor, in LibSepReference]
evalbinop_mul [constructor, in LibSepReference]
evalbinop_sub [constructor, in LibSepReference]
evalbinop_add [constructor, in LibSepReference]
evalbinop_neq [constructor, in LibSepReference]
evalbinop_eq [constructor, in LibSepReference]
EvalProp [section, in LibSepReference]
evalunop [inductive, in LibSepReference]
evalunop_sind [definition, in LibSepReference]
evalunop_ind [definition, in LibSepReference]
evalunop_rand [constructor, in LibSepReference]
evalunop_opp [constructor, in LibSepReference]
evalunop_neg [constructor, in LibSepReference]
eval_frame [lemma, in Triples]
eval_conseq [lemma, in Triples]
eval_sind [definition, in Triples]
eval_ind [definition, in Triples]
eval_free [constructor, in Triples]
eval_set [constructor, in Triples]
eval_get [constructor, in Triples]
eval_ref [constructor, in Triples]
eval_rand [constructor, in Triples]
eval_div [constructor, in Triples]
eval_add [constructor, in Triples]
eval_if [constructor, in Triples]
eval_let [constructor, in Triples]
eval_seq [constructor, in Triples]
eval_app_fix [constructor, in Triples]
eval_app_fun [constructor, in Triples]
eval_fix [constructor, in Triples]
eval_fun [constructor, in Triples]
eval_val [constructor, in Triples]
eval_like_trm_apps_fixs [lemma, in LibSepReference]
eval_like_trm_apps_funs [lemma, in LibSepReference]
eval_like_app_val_funs_one [lemma, in LibSepReference]
eval_like_app_val_funs_cons [lemma, in LibSepReference]
eval_like_trm_funs [lemma, in LibSepReference]
eval_frame [lemma, in LibSepReference]
eval_conseq [lemma, in LibSepReference]
eval_like [definition, in LibSepReference]
eval_app_arg2' [lemma, in LibSepReference]
eval_app_arg1' [lemma, in LibSepReference]
eval_rand [lemma, in LibSepReference]
eval_div [lemma, in LibSepReference]
eval_add [lemma, in LibSepReference]
eval_val_minimal [lemma, in LibSepReference]
eval_sind [definition, in LibSepReference]
eval_ind [definition, in LibSepReference]
eval_free [constructor, in LibSepReference]
eval_set [constructor, in LibSepReference]
eval_get [constructor, in LibSepReference]
eval_ref [constructor, in LibSepReference]
eval_binop [constructor, in LibSepReference]
eval_unop [constructor, in LibSepReference]
eval_if [constructor, in LibSepReference]
eval_let [constructor, in LibSepReference]
eval_seq [constructor, in LibSepReference]
eval_app_fix [constructor, in LibSepReference]
eval_app_fun [constructor, in LibSepReference]
eval_app_arg2 [constructor, in LibSepReference]
eval_app_arg1 [constructor, in LibSepReference]
eval_fix [constructor, in LibSepReference]
eval_fun [constructor, in LibSepReference]
eval_val [constructor, in LibSepReference]
eval_rand [axiom, in Rules]
eval_div [axiom, in Rules]
eval_add [axiom, in Rules]
eval_frame [lemma, in LibSepMinimal]
eval_conseq [lemma, in LibSepMinimal]
eval_sind [definition, in LibSepMinimal]
eval_ind [definition, in LibSepMinimal]
eval_free [constructor, in LibSepMinimal]
eval_set [constructor, in LibSepMinimal]
eval_get [constructor, in LibSepMinimal]
eval_ref [constructor, in LibSepMinimal]
eval_rand [constructor, in LibSepMinimal]
eval_div [constructor, in LibSepMinimal]
eval_add [constructor, in LibSepMinimal]
eval_if [constructor, in LibSepMinimal]
eval_let [constructor, in LibSepMinimal]
eval_app_fix [constructor, in LibSepMinimal]
eval_fix [constructor, in LibSepMinimal]
eval_val [constructor, in LibSepMinimal]
ExampleLocalFunWpgen [module, in WPgen]
ExampleLocalFunWpgen.incrtwice [definition, in WPgen]
ExampleLocalFunWpgen.succtwice [definition, in WPgen]
ExampleLocalFunWpgen.triple_succtwice_using_xfun [lemma, in WPgen]
ExampleLocalFunWpgen.triple_succtwice_using_xletval [lemma, in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_with_xfun [lemma, in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_with_assert [lemma, in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xletva_and_xapp_fun [lemma, in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xletval [lemma, in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xval [lemma, in WPgen]
ExampleLocalFunWpgen.xappfun_lemma [lemma, in WPgen]
ExampleLocalFunWpgen.xfun_lemma [lemma, in WPgen]
ExampleLocalFunWpgen.xletval_lemma [lemma, in WPgen]
ExamplePrograms [module, in Rules]
ExamplePrograms.incr [definition, in Rules]
ExamplePrograms.incr_eq_incr' [lemma, in Rules]
ExamplePrograms.incr' [definition, in Rules]
ExamplePrograms.succ_using_incr [definition, in Rules]
ExamplePrograms.triple_succ_using_incr [lemma, in Rules]
ExamplePrograms.triple_incr [lemma, in Rules]
ExamplePrograms2 [module, in Rules]
ExamplePrograms2.factorec [definition, in Rules]
ExamplePrograms2.triple_factorec [lemma, in Rules]
ExamplePrograms2.triple_hpure' [axiom, in Rules]
example_let [definition, in Basic]
exists_not_empty [lemma, in LibSepFmap]
exists_smallest_fresh [lemma, in LibSepFmap]
exists_fresh [lemma, in LibSepFmap]
Extensionality [module, in Hprop]
Extensionality.functional_extensionality [axiom, in Hprop]
Extensionality.predicate_extensionality_derived [lemma, in Hprop]
Extensionality.propositional_extensionality [axiom, in Hprop]
F
Facto [module, in Basic]factoimp [definition, in Basic]
factoimp_aux [definition, in Basic]
factorec [definition, in Basic]
Facto.facto [axiom, in Basic]
Facto.facto_succ [lemma, in Basic]
Facto.facto_step [axiom, in Basic]
Facto.facto_init [axiom, in Basic]
field [definition, in LibSepReference]
field [definition, in Records]
filter [definition, in LibSepFmap]
Fmap [module, in LibSepReference]
fmap [record, in LibSepFmap]
Fmap [module, in LibSepMinimal]
FmapFresh [section, in LibSepFmap]
FmapFresh.B [variable, in LibSepFmap]
FmapProp [section, in LibSepFmap]
FmapProp.A [variable, in LibSepFmap]
FmapProp.B [variable, in LibSepFmap]
fmap_eq_demo [lemma, in LibSepFmap]
fmap_extens [lemma, in LibSepFmap]
fmap_sind [definition, in LibSepFmap]
fmap_rec [definition, in LibSepFmap]
fmap_ind [definition, in LibSepFmap]
fmap_rect [definition, in LibSepFmap]
fmap_finite [projection, in LibSepFmap]
fmap_data [projection, in LibSepFmap]
formula [definition, in LibSepReference]
formula [definition, in WPgen]
formula_sound [definition, in LibSepReference]
formula_sound [definition, in WPsound]
fresh [definition, in LibSepFmap]
FromPreToPostGC [module, in Affine]
FromPreToPostGC.eta_same_triples [axiom, in Affine]
FromPreToPostGC.triple_hgc_post_from_hgc_pre [lemma, in Affine]
FromPreToPostGC.triple_hgc_post [axiom, in Affine]
FromPreToPostGC.triple_hgc_pre [axiom, in Affine]
FullyAffineLogic [module, in Affine]
FullyAffineLogic.haffine_equiv [lemma, in Affine]
FullyAffineLogic.heap_affine_union [lemma, in Affine]
FullyAffineLogic.heap_affine_empty [lemma, in Affine]
FullyAffineLogic.heap_affine_def [axiom, in Affine]
FullyAffineLogic.hgc_eq_htop [lemma, in Affine]
FullyAffineLogic.htop [definition, in Affine]
FullyLinearLogic [module, in Affine]
FullyLinearLogic.haffine_equiv [lemma, in Affine]
FullyLinearLogic.heap_affine_union [lemma, in Affine]
FullyLinearLogic.heap_affine_empty [lemma, in Affine]
FullyLinearLogic.heap_affine_def [axiom, in Affine]
FullyLinearLogic.hgc_eq_hempty [lemma, in Affine]
functional_extensionality [axiom, in LibSepReference]
functional_extensionality [axiom, in Hprop]
functional_extensionality [axiom, in LibSepMinimal]
G
get_and_free [definition, in Basic]H
haffine [definition, in Affine]HaffineQuantifiers [module, in Affine]
HaffineQuantifiers.haffine_hforall [lemma, in Affine]
HaffineQuantifiers.haffine_hexists [lemma, in Affine]
HaffineQuantifiers.haffine_post [definition, in Affine]
haffine_hgc [lemma, in LibSepReference]
haffine_hstar_hpure [lemma, in LibSepReference]
haffine_hforall [lemma, in LibSepReference]
haffine_hexists [lemma, in LibSepReference]
haffine_hstar [lemma, in LibSepReference]
haffine_hpure [lemma, in LibSepReference]
haffine_hempty [lemma, in LibSepReference]
haffine_hgc [lemma, in Affine]
haffine_hstar_hpure_l [lemma, in Affine]
haffine_hforall [lemma, in Affine]
haffine_hforall' [lemma, in Affine]
haffine_hexists [lemma, in Affine]
haffine_hstar [lemma, in Affine]
haffine_hpure [lemma, in Affine]
haffine_hempty [lemma, in Affine]
Hand [module, in Wand]
hand [definition, in LibSepReference]
hand_sym [lemma, in LibSepReference]
Hand.hand [definition, in Wand]
Hand.hand_comm [lemma, in Wand]
Hand.hand_eq_hand' [lemma, in Wand]
Hand.hand' [definition, in Wand]
Hand.himpl_hand_r [lemma, in Wand]
Hand.himpl_hand_l_l [lemma, in Wand]
Hand.himpl_hand_l_r [lemma, in Wand]
harray [axiom, in Arrays]
hcell [axiom, in Arrays]
head [definition, in Repr]
head [definition, in Records]
heap [definition, in LibSepReference]
heap [definition, in Hprop]
heap [definition, in LibSepMinimal]
heap_affine_union [axiom, in Affine]
heap_affine_empty [axiom, in Affine]
heap_affine [axiom, in Affine]
hempty [definition, in Hprop]
hempty [definition, in LibSepMinimal]
hempty_eq_hpure_true [lemma, in Hprop]
hempty_inv [lemma, in Hprop]
hempty_intro [lemma, in Hprop]
hempty_himpl_hgc [lemma, in Affine]
hempty' [definition, in Hprop]
hexists [definition, in Hprop]
hexists [definition, in LibSepMinimal]
hexists_inv [lemma, in Hprop]
hexists_intro [lemma, in Hprop]
hexists_named_eq [lemma, in Himpl]
hfield [definition, in Records]
hfields [definition, in Records]
hfields_update [definition, in LibSepReference]
hfields_lookup [definition, in LibSepReference]
hfields_update [definition, in Records]
hfields_lookup [definition, in Records]
Hforall [module, in Wand]
hforall [definition, in LibSepMinimal]
Hforall.hforall [definition, in Wand]
Hforall.hforall_specialize [lemma, in Wand]
Hforall.hforall_inv [lemma, in Wand]
Hforall.hforall_intro [lemma, in Wand]
Hforall.himpl_hforall_l [lemma, in Wand]
Hforall.himpl_hforall_r [lemma, in Wand]
Hforall.triple_hforall [lemma, in Wand]
\forall _ .. _ , _ [notation, in Wand]
hgc [definition, in Affine]
hgc_eq_heap_affine [lemma, in Affine]
hgc_inv [lemma, in Affine]
hgc_intro [lemma, in Affine]
hheader [axiom, in Arrays]
himpl [definition, in LibSepMinimal]
himpl [definition, in Himpl]
Himpl [library]
himpl_hand_r [lemma, in LibSepReference]
himpl_hand_l_l [lemma, in LibSepReference]
himpl_hand_l_r [lemma, in LibSepReference]
himpl_hor_l [lemma, in LibSepReference]
himpl_hor_r_r [lemma, in LibSepReference]
himpl_hor_r_l [lemma, in LibSepReference]
himpl_wpgen_wp [lemma, in LibSepReference]
himpl_hforall [lemma, in LibSepMinimal]
himpl_hforall_l [lemma, in LibSepMinimal]
himpl_hforall_r [lemma, in LibSepMinimal]
himpl_hexists [lemma, in LibSepMinimal]
himpl_hexists_r [lemma, in LibSepMinimal]
himpl_hexists_l [lemma, in LibSepMinimal]
himpl_hstar_hpure_l [lemma, in LibSepMinimal]
himpl_hstar_hpure_r [lemma, in LibSepMinimal]
himpl_frame_r [lemma, in LibSepMinimal]
himpl_frame_l [lemma, in LibSepMinimal]
himpl_antisym [lemma, in LibSepMinimal]
himpl_trans [lemma, in LibSepMinimal]
himpl_refl [lemma, in LibSepMinimal]
himpl_hexists_l [lemma, in Himpl]
himpl_hexists_r [lemma, in Himpl]
himpl_hstar_hpure_l [lemma, in Himpl]
himpl_hstar_hpure_r [lemma, in Himpl]
himpl_frame_l [axiom, in Himpl]
himpl_antisym [lemma, in Himpl]
himpl_trans [lemma, in Himpl]
himpl_refl [lemma, in Himpl]
himpl_hgc_absorb_r [lemma, in Affine]
himpl_hgc_r [lemma, in Affine]
Hor [module, in Wand]
hor [definition, in LibSepReference]
hor_sym [lemma, in LibSepReference]
Hor.himpl_hor_l [lemma, in Wand]
Hor.himpl_hor_r_r_trans [lemma, in Wand]
Hor.himpl_hor_r_l_trans [lemma, in Wand]
Hor.himpl_hor_r_r [lemma, in Wand]
Hor.himpl_hor_r_l [lemma, in Wand]
Hor.hor [definition, in Wand]
Hor.HorExample [module, in Wand]
Hor.HorExample.MList_using_hor [lemma, in Wand]
Hor.hor_comm [lemma, in Wand]
Hor.hor_eq_hor' [lemma, in Wand]
Hor.hor' [definition, in Wand]
Hor.if_neg [lemma, in Wand]
hprop [definition, in Hprop]
hprop [definition, in LibSepMinimal]
Hprop [library]
HpropProofs [module, in Hprop]
HpropProofs.hprop_op_comm [lemma, in Hprop]
HpropProofs.hstar_hpure_l [lemma, in Hprop]
HpropProofs.hstar_comm_assoc [lemma, in Hprop]
HpropProofs.hstar_hempty_r [lemma, in Hprop]
HpropProofs.hstar_assoc [lemma, in Hprop]
HpropProofs.hstar_comm [lemma, in Hprop]
HpropProofs.hstar_hempty_l [lemma, in Hprop]
HpropProofs.hstar_hexists [lemma, in Hprop]
hprop_eq [lemma, in Hprop]
hpure [definition, in Hprop]
hpure [definition, in LibSepMinimal]
hpure_eq_hexists_proof [lemma, in Hprop]
hpure_inv [lemma, in Hprop]
hpure_intro [lemma, in Hprop]
hpure' [definition, in Hprop]
hrecord [axiom, in LibSepReference]
hrecord [definition, in Records]
hrecord_not_null [axiom, in LibSepReference]
hrecord_fields [definition, in LibSepReference]
hrecord_field [definition, in LibSepReference]
hrecord_elim [lemma, in Records]
hrecord_fields [definition, in Records]
hrecord_field [definition, in Records]
HS [module, in LibSepReference]
hseg [definition, in Arrays]
hseg_last_r [lemma, in Arrays]
hseg_app_r [lemma, in Arrays]
hseg_cons_r [lemma, in Arrays]
hseg_last [lemma, in Arrays]
hseg_cons [lemma, in Arrays]
hseg_app [axiom, in Arrays]
hseg_one [axiom, in Arrays]
hseg_nil [axiom, in Arrays]
hsingle [definition, in Hprop]
hsingle [definition, in LibSepMinimal]
hsingle_inv [lemma, in Hprop]
hsingle_intro [lemma, in Hprop]
hstar [definition, in Hprop]
hstar [definition, in LibSepMinimal]
hstar_inv [lemma, in Hprop]
hstar_intro [lemma, in Hprop]
hstar_hpure_l [axiom, in Hprop]
hstar_hexists [axiom, in Hprop]
hstar_hempty_l [axiom, in Hprop]
hstar_comm [axiom, in Hprop]
hstar_assoc [axiom, in Hprop]
hstar_assoc_statement [axiom, in Hprop]
hstar_hsingle_same_loc [lemma, in LibSepMinimal]
hstar_hpure_l [lemma, in LibSepMinimal]
hstar_hempty_r [lemma, in LibSepMinimal]
hstar_hforall [lemma, in LibSepMinimal]
hstar_hexists [lemma, in LibSepMinimal]
hstar_hempty_l [lemma, in LibSepMinimal]
hstar_assoc [lemma, in LibSepMinimal]
hstar_comm [lemma, in LibSepMinimal]
hstar_intro [lemma, in LibSepMinimal]
hstar_hsingle_same_loc [lemma, in Himpl]
hstar_hgc_hgc [lemma, in Affine]
Hwand [module, in Wand]
HwandEquiv [module, in Wand]
HwandEquiv.hwand_characterization_3_eq_4 [lemma, in Wand]
HwandEquiv.hwand_characterization_2_eq_3 [lemma, in Wand]
HwandEquiv.hwand_characterization_1_eq_2 [lemma, in Wand]
HwandEquiv.hwand_characterization_4 [definition, in Wand]
HwandEquiv.hwand_characterization_3 [definition, in Wand]
HwandEquiv.hwand_characterization_2 [definition, in Wand]
HwandEquiv.hwand_characterization_1 [definition, in Wand]
HwandFalse [module, in Wand]
HwandFalse.himpl_hwand_same_hempty_counterexample [lemma, in Wand]
HwandFalse.not_himpl_hwand_r_inv_reciprocal [lemma, in Wand]
Hwand.himpl_hwand_hstar_same_r [lemma, in Wand]
Hwand.himpl_hwand_hpure_lr [lemma, in Wand]
Hwand.himpl_hwand_hpure_r [lemma, in Wand]
Hwand.himpl_hempty_hwand_same [lemma, in Wand]
Hwand.himpl_hwand_r_inv [lemma, in Wand]
Hwand.himpl_hwand_r [lemma, in Wand]
Hwand.hstar_hwand [lemma, in Wand]
Hwand.hwand [definition, in Wand]
Hwand.hwand_inv [lemma, in Wand]
Hwand.hwand_frame [lemma, in Wand]
Hwand.hwand_cancel_part [lemma, in Wand]
Hwand.hwand_curry_eq [lemma, in Wand]
Hwand.hwand_hpure_l [lemma, in Wand]
Hwand.hwand_hempty_l [lemma, in Wand]
Hwand.hwand_trans_elim [lemma, in Wand]
Hwand.hwand_himpl [lemma, in Wand]
Hwand.hwand_cancel [lemma, in Wand]
Hwand.hwand_equiv [lemma, in Wand]
Hwand.hwand' [definition, in Wand]
_ \−∗ _ [notation, in Wand]
I
incr [definition, in LibSepMinimal]incr [definition, in Basic]
incr_first [definition, in Basic]
incr_two [definition, in Basic]
indom [definition, in LibSepFmap]
indom_remove_eq [lemma, in LibSepFmap]
indom_update_eq [lemma, in LibSepFmap]
indom_union_r [lemma, in LibSepFmap]
indom_union_l [lemma, in LibSepFmap]
indom_union_eq [lemma, in LibSepFmap]
indom_single [lemma, in LibSepFmap]
indom_single_eq [lemma, in LibSepFmap]
Inhab_trm [instance, in LibSepReference]
Inhab_val [instance, in LibSepReference]
Inhab_fmap [instance, in LibSepFmap]
Inhab_val [instance, in LibSepMinimal]
injective_nat_to_var [lemma, in LibSepVar]
inplace_double [definition, in Basic]
IsCounter [definition, in Repr]
isubst [definition, in LibSepReference]
isubst [definition, in WPgen]
IsubstProp [module, in WPsound]
IsubstProp.ctx_disjoint_rem [lemma, in WPsound]
IsubstProp.ctx_disjoint [definition, in WPsound]
IsubstProp.ctx_equiv_rem [lemma, in WPsound]
IsubstProp.ctx_equiv [definition, in WPsound]
IsubstProp.isubst_rem_2 [lemma, in WPsound]
IsubstProp.isubst_rem [lemma, in WPsound]
IsubstProp.isubst_app_swap [lemma, in WPsound]
IsubstProp.isubst_app [lemma, in WPsound]
IsubstProp.isubst_ctx_equiv [lemma, in WPsound]
IsubstProp.isubst_nil [lemma, in WPsound]
IsubstProp.lookup_app [lemma, in WPsound]
IsubstProp.lookup_rem [lemma, in WPsound]
IsubstProp.rem_app [lemma, in WPsound]
IsubstProp.subst_eq_isubst_one [lemma, in WPsound]
isubst_rem_2 [lemma, in LibSepReference]
isubst_rem [lemma, in LibSepReference]
isubst_app_swap [lemma, in LibSepReference]
isubst_cons [lemma, in LibSepReference]
isubst_app [lemma, in LibSepReference]
isubst_ctx_equiv [lemma, in LibSepReference]
isubst_nil [lemma, in LibSepReference]
isubst_rem [axiom, in WPsound]
isubst_nil [axiom, in WPsound]
item [definition, in Repr]
L
Leaf [constructor, in Repr]left [definition, in Repr]
length_var_seq [lemma, in LibSepVar]
LetFrame [module, in Rules]
LetFrame.triple_let_frame [lemma, in Rules]
LetFrame.triple_let [axiom, in Rules]
LibSepFmap [library]
LibSepMinimal [library]
LibSepReference [library]
LibSepSimpl [library]
LibSepVar [library]
loc [definition, in LibSepReference]
loc [definition, in LibSepMinimal]
loc_fresh_nat [lemma, in LibSepFmap]
loc_fresh_nat_ge [lemma, in LibSepFmap]
loc_fresh_ind [lemma, in LibSepFmap]
loc_fresh_gen [definition, in LibSepFmap]
lookup [definition, in LibSepReference]
lookup [definition, in WPgen]
lookup_rem [lemma, in LibSepReference]
lookup_app [lemma, in LibSepReference]
M
make_eq [lemma, in LibSepFmap]map [definition, in LibSepFmap]
MapOps [section, in LibSepFmap]
MapOps.A [variable, in LibSepFmap]
MapOps.B [variable, in LibSepFmap]
maps_all_fields [definition, in Records]
map_ [definition, in LibSepFmap]
map_map_finite [definition, in LibSepFmap]
map_filter_finite [definition, in LibSepFmap]
map_remove_finite [definition, in LibSepFmap]
map_union_finite [lemma, in LibSepFmap]
map_union_comm [lemma, in LibSepFmap]
map_disjoint_sym [lemma, in LibSepFmap]
map_disjoint_eq [lemma, in LibSepFmap]
map_map [definition, in LibSepFmap]
map_filter [definition, in LibSepFmap]
map_indom [definition, in LibSepFmap]
map_agree [definition, in LibSepFmap]
map_disjoint [definition, in LibSepFmap]
map_finite [definition, in LibSepFmap]
map_remove [definition, in LibSepFmap]
map_union [definition, in LibSepFmap]
MatchStyle [module, in Rules]
MatchStyle.triple_ref' [axiom, in Rules]
MatchStyle.triple_ref [axiom, in Rules]
max_r [lemma, in Basic]
max_l [lemma, in Basic]
mcons [definition, in Repr]
mcons [definition, in Records]
mcopy [definition, in Repr]
mfree [definition, in Repr]
miter [definition, in Repr]
mkstruct [definition, in LibSepReference]
mkstruct [definition, in WPgen]
MkstructProp [module, in WPgen]
MkstructProp.mkstruct [axiom, in WPgen]
MkstructProp.mkstruct_monotone [axiom, in WPgen]
MkstructProp.mkstruct_erase [axiom, in WPgen]
MkstructProp.mkstruct_conseq [axiom, in WPgen]
MkstructProp.mkstruct_frame [axiom, in WPgen]
mkstruct_sound [lemma, in LibSepReference]
mkstruct_wp [lemma, in LibSepReference]
mkstruct_monotone [lemma, in LibSepReference]
mkstruct_frame [lemma, in LibSepReference]
mkstruct_conseq [lemma, in LibSepReference]
mkstruct_erase [lemma, in LibSepReference]
mkstruct_ramified [lemma, in LibSepReference]
mkstruct_monotone [lemma, in WPgen]
mkstruct_erase [lemma, in WPgen]
mkstruct_conseq [lemma, in WPgen]
mkstruct_frame [lemma, in WPgen]
mkstruct_idempotent [lemma, in WPsound]
mkstruct_sound' [lemma, in WPsound]
mkstruct_sound [lemma, in WPsound]
mkstruct_wp [lemma, in WPsound]
mkstruct' [definition, in WPgen]
mlength [definition, in Repr]
mlength_using_miter [definition, in Repr]
mlength' [definition, in Repr]
MList [definition, in Repr]
MList_if [lemma, in Repr]
MList_cons [lemma, in Repr]
MList_nil [lemma, in Repr]
mnil [definition, in Repr]
mnode [definition, in Repr]
MotivatingExample [module, in Affine]
MotivatingExampleSolved [module, in Affine]
MotivatingExampleSolved.triple_succ_using_incr' [lemma, in Affine]
MotivatingExample.succ_using_incr [definition, in Affine]
MotivatingExample.triple_succ_using_incr' [lemma, in Affine]
MotivatingExample.triple_succ_using_incr [lemma, in Affine]
mrev [definition, in Repr]
mrev_aux [definition, in Repr]
MTree [definition, in Repr]
mtreesum [definition, in Repr]
MTree_if [lemma, in Repr]
MTree_Node [lemma, in Repr]
MTree_Leaf [lemma, in Repr]
N
nat_to_var [definition, in LibSepVar]NewTriples [module, in Affine]
NewTriples.mkstruct [definition, in Affine]
NewTriples.mkstruct_haffine_pre [lemma, in Affine]
NewTriples.mkstruct_haffine_post [lemma, in Affine]
NewTriples.mkstruct_monotone [lemma, in Affine]
NewTriples.mkstruct_frame [lemma, in Affine]
NewTriples.mkstruct_conseq [lemma, in Affine]
NewTriples.mkstruct_erase [lemma, in Affine]
NewTriples.mkstruct_hgc [lemma, in Affine]
NewTriples.MotivatingExampleWithUpdatedXwp [module, in Affine]
NewTriples.MotivatingExampleWithUpdatedXwp.haffine_hany [axiom, in Affine]
NewTriples.MotivatingExampleWithUpdatedXwp.triple_succ_using_incr [lemma, in Affine]
NewTriples.triple [definition, in Affine]
NewTriples.triple_ramified_frame_hgc [lemma, in Affine]
NewTriples.triple_conseq_frame_hgc [lemma, in Affine]
NewTriples.triple_haffine_pre [lemma, in Affine]
NewTriples.triple_hgc_post_from_triple_haffine_post [lemma, in Affine]
NewTriples.triple_haffine_post [lemma, in Affine]
NewTriples.triple_hgc_post [lemma, in Affine]
NewTriples.triple_seq [lemma, in Affine]
NewTriples.triple_hexists [lemma, in Affine]
NewTriples.triple_hpure [lemma, in Affine]
NewTriples.triple_frame [lemma, in Affine]
NewTriples.triple_conseq [lemma, in Affine]
NewTriples.wp [definition, in Affine]
NewTriples.wp_ramified [lemma, in Affine]
NewTriples.wp_haffine_pre [lemma, in Affine]
NewTriples.wp_hgc_post [lemma, in Affine]
NewTriples.wp_frame [lemma, in Affine]
NewTriples.wp_conseq [lemma, in Affine]
NewTriples.wp_equiv [lemma, in Affine]
NewTriples.xwp_lemma' [lemma, in Affine]
NewTriples.xwp_lemma [axiom, in Affine]
Node [constructor, in Repr]
noduplicates_var_seq [lemma, in LibSepVar]
NotationForFmapDisjoint [module, in LibSepFmap]
\# _ _ _ (fmap_scope) [notation, in LibSepFmap]
\# _ _ (fmap_scope) [notation, in LibSepFmap]
NotationForVariables [module, in LibSepVar]
trm:'z3 (trm_scope) [notation, in LibSepVar]
trm:'y3 (trm_scope) [notation, in LibSepVar]
trm:'x3 (trm_scope) [notation, in LibSepVar]
trm:'w3 (trm_scope) [notation, in LibSepVar]
trm:'v3 (trm_scope) [notation, in LibSepVar]
trm:'u3 (trm_scope) [notation, in LibSepVar]
trm:'t3 (trm_scope) [notation, in LibSepVar]
trm:'s3 (trm_scope) [notation, in LibSepVar]
trm:'r3 (trm_scope) [notation, in LibSepVar]
trm:'q3 (trm_scope) [notation, in LibSepVar]
trm:'p3 (trm_scope) [notation, in LibSepVar]
trm:'o3 (trm_scope) [notation, in LibSepVar]
trm:'n3 (trm_scope) [notation, in LibSepVar]
trm:'m3 (trm_scope) [notation, in LibSepVar]
trm:'l3 (trm_scope) [notation, in LibSepVar]
trm:'k3 (trm_scope) [notation, in LibSepVar]
trm:'j3 (trm_scope) [notation, in LibSepVar]
trm:'i3 (trm_scope) [notation, in LibSepVar]
trm:'h3 (trm_scope) [notation, in LibSepVar]
trm:'g3 (trm_scope) [notation, in LibSepVar]
trm:'f3 (trm_scope) [notation, in LibSepVar]
trm:'e3 (trm_scope) [notation, in LibSepVar]
trm:'d3 (trm_scope) [notation, in LibSepVar]
trm:'c3 (trm_scope) [notation, in LibSepVar]
trm:'b3 (trm_scope) [notation, in LibSepVar]
trm:'a3 (trm_scope) [notation, in LibSepVar]
trm:'z2 (trm_scope) [notation, in LibSepVar]
trm:'y2 (trm_scope) [notation, in LibSepVar]
trm:'x2 (trm_scope) [notation, in LibSepVar]
trm:'w2 (trm_scope) [notation, in LibSepVar]
trm:'v2 (trm_scope) [notation, in LibSepVar]
trm:'u2 (trm_scope) [notation, in LibSepVar]
trm:'t2 (trm_scope) [notation, in LibSepVar]
trm:'s2 (trm_scope) [notation, in LibSepVar]
trm:'r2 (trm_scope) [notation, in LibSepVar]
trm:'q2 (trm_scope) [notation, in LibSepVar]
trm:'p2 (trm_scope) [notation, in LibSepVar]
trm:'o2 (trm_scope) [notation, in LibSepVar]
trm:'n2 (trm_scope) [notation, in LibSepVar]
trm:'m2 (trm_scope) [notation, in LibSepVar]
trm:'l2 (trm_scope) [notation, in LibSepVar]
trm:'k2 (trm_scope) [notation, in LibSepVar]
trm:'j2 (trm_scope) [notation, in LibSepVar]
trm:'i2 (trm_scope) [notation, in LibSepVar]
trm:'h2 (trm_scope) [notation, in LibSepVar]
trm:'g2 (trm_scope) [notation, in LibSepVar]
trm:'f2 (trm_scope) [notation, in LibSepVar]
trm:'e2 (trm_scope) [notation, in LibSepVar]
trm:'d2 (trm_scope) [notation, in LibSepVar]
trm:'c2 (trm_scope) [notation, in LibSepVar]
trm:'b2 (trm_scope) [notation, in LibSepVar]
trm:'a2 (trm_scope) [notation, in LibSepVar]
trm:'z1 (trm_scope) [notation, in LibSepVar]
trm:'y1 (trm_scope) [notation, in LibSepVar]
trm:'x1 (trm_scope) [notation, in LibSepVar]
trm:'w1 (trm_scope) [notation, in LibSepVar]
trm:'v1 (trm_scope) [notation, in LibSepVar]
trm:'u1 (trm_scope) [notation, in LibSepVar]
trm:'t1 (trm_scope) [notation, in LibSepVar]
trm:'s1 (trm_scope) [notation, in LibSepVar]
trm:'r1 (trm_scope) [notation, in LibSepVar]
trm:'q1 (trm_scope) [notation, in LibSepVar]
trm:'p1 (trm_scope) [notation, in LibSepVar]
trm:'o1 (trm_scope) [notation, in LibSepVar]
trm:'n1 (trm_scope) [notation, in LibSepVar]
trm:'m1 (trm_scope) [notation, in LibSepVar]
trm:'l1 (trm_scope) [notation, in LibSepVar]
trm:'k1 (trm_scope) [notation, in LibSepVar]
trm:'j1 (trm_scope) [notation, in LibSepVar]
trm:'i1 (trm_scope) [notation, in LibSepVar]
trm:'h1 (trm_scope) [notation, in LibSepVar]
trm:'g1 (trm_scope) [notation, in LibSepVar]
trm:'f1 (trm_scope) [notation, in LibSepVar]
trm:'e1 (trm_scope) [notation, in LibSepVar]
trm:'d1 (trm_scope) [notation, in LibSepVar]
trm:'c1 (trm_scope) [notation, in LibSepVar]
trm:'b1 (trm_scope) [notation, in LibSepVar]
trm:'a1 (trm_scope) [notation, in LibSepVar]
trm:'z (trm_scope) [notation, in LibSepVar]
trm:'y (trm_scope) [notation, in LibSepVar]
trm:'x (trm_scope) [notation, in LibSepVar]
trm:'w (trm_scope) [notation, in LibSepVar]
trm:'v (trm_scope) [notation, in LibSepVar]
trm:'u (trm_scope) [notation, in LibSepVar]
trm:'t (trm_scope) [notation, in LibSepVar]
trm:'s (trm_scope) [notation, in LibSepVar]
trm:'r (trm_scope) [notation, in LibSepVar]
trm:'q (trm_scope) [notation, in LibSepVar]
trm:'p (trm_scope) [notation, in LibSepVar]
trm:'o (trm_scope) [notation, in LibSepVar]
trm:'n (trm_scope) [notation, in LibSepVar]
trm:'m (trm_scope) [notation, in LibSepVar]
trm:'l (trm_scope) [notation, in LibSepVar]
trm:'k (trm_scope) [notation, in LibSepVar]
trm:'j (trm_scope) [notation, in LibSepVar]
trm:'i (trm_scope) [notation, in LibSepVar]
trm:'h (trm_scope) [notation, in LibSepVar]
trm:'g (trm_scope) [notation, in LibSepVar]
trm:'f (trm_scope) [notation, in LibSepVar]
trm:'e (trm_scope) [notation, in LibSepVar]
trm:'d (trm_scope) [notation, in LibSepVar]
trm:'c (trm_scope) [notation, in LibSepVar]
trm:'b (trm_scope) [notation, in LibSepVar]
trm:'a (trm_scope) [notation, in LibSepVar]
notstuck [definition, in Triples]
notstuck [definition, in LibSepReference]
null [definition, in LibSepReference]
P
Pivot [module, in Arrays]Pivot.triple_pivot' [lemma, in Arrays]
Pivot.triple_array_swap_seg_self [lemma, in Arrays]
Pivot.triple_array_swap_seg_lists [lemma, in Arrays]
Pivot.triple_array_swap_seg [lemma, in Arrays]
Pivot.triple_array_get_hseg_vals_int [lemma, in Arrays]
Pivot.val_pivot [definition, in Arrays]
Pivot.val_array_swap [definition, in Arrays]
Postscript [library]
predicate_extensionality [axiom, in Hprop]
Preface [library]
Preview [module, in Affine]
Preview.haffine [axiom, in Affine]
Preview.triple_haffine_pre [axiom, in Affine]
Preview.triple_haffine_post [axiom, in Affine]
prim [inductive, in LibSepReference]
prim [inductive, in LibSepMinimal]
prim_sind [definition, in LibSepReference]
prim_rec [definition, in LibSepReference]
prim_ind [definition, in LibSepReference]
prim_rect [definition, in LibSepReference]
prim_sind [definition, in LibSepMinimal]
prim_rec [definition, in LibSepMinimal]
prim_ind [definition, in LibSepMinimal]
prim_rect [definition, in LibSepMinimal]
ProgramSyntax [module, in LibSepReference]
ProgramSyntax.string_to_var [definition, in LibSepReference]
ProgramSyntax.Vars [module, in LibSepReference]
ProofsSameSemantics [module, in Rules]
ProofsSameSemantics.eta_same_triples [lemma, in Rules]
ProofsSameSemantics.eval_like_eta_expansion [lemma, in Rules]
ProofsSameSemantics.eval_like_eta_reduction [lemma, in Rules]
ProofsSameSemantics.eval_like [definition, in Rules]
ProofsSameSemantics.triple_trm_seq_assoc [lemma, in Rules]
ProofsSameSemantics.triple_app_fun [lemma, in Rules]
ProofsSameSemantics.triple_eval_like [lemma, in Rules]
ProofsWithAdvancedXtactics [module, in WPgen]
ProofsWithAdvancedXtactics.triple_incr [lemma, in WPgen]
ProofsWithStructuralXtactics [module, in WPgen]
ProofsWithStructuralXtactics.triple_incr_frame [lemma, in WPgen]
ProofsWithXlemmas [module, in WPgen]
ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas [lemma, in WPgen]
ProofsWithXlemmas.triple_incr [lemma, in WPgen]
ProofsWithXtactics [module, in WPgen]
ProofsWithXtactics.triple_succ_using_incr_with_xtactics [lemma, in WPgen]
ProofsWithXtactics.triple_incr [lemma, in WPgen]
propositional_extensionality [axiom, in LibSepReference]
propositional_extensionality [axiom, in LibSepMinimal]
prove_eq_val_fix_trm_funs_demo [lemma, in LibSepReference]
prove_eq_val_funs_demo [lemma, in LibSepReference]
prove_eq_trm_apps_demo [lemma, in LibSepReference]
purepost [definition, in LibSepReference]
purepostin [definition, in LibSepReference]
Q
qimpl [definition, in LibSepMinimal]qimpl [definition, in Himpl]
qimpl_refl [lemma, in LibSepMinimal]
qimpl_antisym [lemma, in Himpl]
qimpl_trans [lemma, in Himpl]
qimpl_refl [lemma, in Himpl]
qprop_eq [lemma, in Hprop]
quadruple [definition, in Basic]
QuickSort [module, in Arrays]
QuickSort.harray_eq [axiom, in Arrays]
QuickSort.length_vals_int [lemma, in Arrays]
QuickSort.list_of_le [definition, in Arrays]
QuickSort.list_of_gt [definition, in Arrays]
QuickSort.permut [inductive, in Arrays]
QuickSort.permut_Forall [lemma, in Arrays]
QuickSort.permut_swap_first_last [lemma, in Arrays]
QuickSort.permut_swap_first_two [lemma, in Arrays]
QuickSort.permut_last [lemma, in Arrays]
QuickSort.permut_cons [lemma, in Arrays]
QuickSort.permut_app [lemma, in Arrays]
QuickSort.permut_length [lemma, in Arrays]
QuickSort.permut_sym [lemma, in Arrays]
QuickSort.permut_refl [lemma, in Arrays]
QuickSort.permut_sind [definition, in Arrays]
QuickSort.permut_ind [definition, in Arrays]
QuickSort.permut_trans [constructor, in Arrays]
QuickSort.permut_mid [constructor, in Arrays]
QuickSort.sorted [inductive, in Arrays]
QuickSort.SortedLists [section, in Arrays]
QuickSort.sorted_app_le [lemma, in Arrays]
QuickSort.sorted_cons_gt [lemma, in Arrays]
QuickSort.sorted_sind [definition, in Arrays]
QuickSort.sorted_ind [definition, in Arrays]
QuickSort.sorted_cons [constructor, in Arrays]
QuickSort.sorted_one [constructor, in Arrays]
QuickSort.sorted_nil [constructor, in Arrays]
QuickSort.triple_quicksort_full [lemma, in Arrays]
QuickSort.triple_quicksort [lemma, in Arrays]
QuickSort.triple_pivot [axiom, in Arrays]
QuickSort.triple_quicksort_safety [lemma, in Arrays]
QuickSort.triple_pivot_safety [axiom, in Arrays]
QuickSort.vals_int_last [lemma, in Arrays]
QuickSort.vals_int_app [lemma, in Arrays]
QuickSort.vals_int_cons [lemma, in Arrays]
QuickSort.vals_int_nil [lemma, in Arrays]
QuickSort.vals_int [definition, in Arrays]
QuickSort.val_quicksort_full [definition, in Arrays]
QuickSort.val_quicksort [definition, in Arrays]
QuickSort.val_pivot [axiom, in Arrays]
Qwand [module, in Wand]
QwandEquiv [module, in Wand]
QwandEquiv.hwand_characterization_1_eq_2 [lemma, in Wand]
QwandEquiv.qwand_characterization_4_eq_5 [lemma, in Wand]
QwandEquiv.qwand_characterization_2_eq_4 [lemma, in Wand]
QwandEquiv.qwand_characterization_2_eq_3 [lemma, in Wand]
QwandEquiv.qwand_characterization_5 [definition, in Wand]
QwandEquiv.qwand_characterization_4 [definition, in Wand]
QwandEquiv.qwand_characterization_3 [definition, in Wand]
QwandEquiv.qwand_characterization_2 [definition, in Wand]
QwandEquiv.qwand_characterization_1 [definition, in Wand]
Qwand.himpl_qwand_hstar_same_r [lemma, in Wand]
Qwand.hstar_qwand [lemma, in Wand]
Qwand.qwand [definition, in Wand]
Qwand.qwand_cancel_part [lemma, in Wand]
Qwand.qwand_himpl [lemma, in Wand]
Qwand.qwand_cancel [lemma, in Wand]
Qwand.qwand_equiv [lemma, in Wand]
Qwand.qwand_specialize [lemma, in Wand]
Qwand.qwand' [definition, in Wand]
_ \−−∗ _ [notation, in Wand]
R
RamifiedFrame [module, in Wand]RamifiedFrame.triple_ref_extended' [lemma, in Wand]
RamifiedFrame.triple_ref_extended [lemma, in Wand]
RamifiedFrame.triple_ref [axiom, in Wand]
RamifiedFrame.triple_conseq_frame' [axiom, in Wand]
RamifiedFrame.triple_conseq_frame_of_ramified_frame [lemma, in Wand]
RamifiedFrame.triple_ramified_frame [lemma, in Wand]
RamifiedFrame.triple_conseq_frame [axiom, in Wand]
read [definition, in LibSepFmap]
read_union_r [lemma, in LibSepFmap]
read_union_l [lemma, in LibSepFmap]
read_single [lemma, in LibSepFmap]
Realization [module, in Records]
Realization [module, in Arrays]
Realization.eval_alloc [axiom, in Arrays]
Realization.eval_ptr_add [axiom, in Arrays]
Realization.harray [definition, in Arrays]
Realization.harray_focus_read [lemma, in Arrays]
Realization.harray_focus [lemma, in Arrays]
Realization.harray_focus' [axiom, in Arrays]
Realization.harray_focus_read' [axiom, in Arrays]
Realization.harray_eq [lemma, in Arrays]
Realization.hcell [definition, in Arrays]
Realization.hcell_nonneg [lemma, in Arrays]
Realization.hcell_eq [lemma, in Arrays]
Realization.hfields_eq_hrange [lemma, in Records]
Realization.hfields_update_preserves_maps_all_fields [lemma, in Records]
Realization.hfields_update_preserves_fields [lemma, in Records]
Realization.hheader [definition, in Arrays]
Realization.hheader_eq [lemma, in Arrays]
Realization.hrange [definition, in Arrays]
Realization.hrange_intro [lemma, in Arrays]
Realization.hseg [definition, in Arrays]
Realization.hseg_eq_hrange [lemma, in Arrays]
Realization.hseg_focus [lemma, in Arrays]
Realization.hseg_focus_relative [lemma, in Arrays]
Realization.hseg_app [lemma, in Arrays]
Realization.hseg_cons [lemma, in Arrays]
Realization.hseg_one [lemma, in Arrays]
Realization.hseg_nil [lemma, in Arrays]
Realization.hseg_start_eq [lemma, in Arrays]
Realization.triple_new_hrecord_2 [lemma, in Records]
Realization.triple_alloc_mcons [lemma, in Records]
Realization.triple_alloc_hrecord [lemma, in Records]
Realization.triple_set_field_hrecord [lemma, in Records]
Realization.triple_get_field_hrecord [lemma, in Records]
Realization.triple_set_field_hfields [lemma, in Records]
Realization.triple_get_field_hfields [lemma, in Records]
Realization.triple_set_field [lemma, in Records]
Realization.triple_get_field [lemma, in Records]
Realization.triple_array_make [lemma, in Arrays]
Realization.triple_array_length [lemma, in Arrays]
Realization.triple_array_set [lemma, in Arrays]
Realization.triple_array_get [lemma, in Arrays]
Realization.triple_array_make_hseg [lemma, in Arrays]
Realization.triple_array_fill [lemma, in Arrays]
Realization.triple_array_set_hseg [lemma, in Arrays]
Realization.triple_array_get_hseg [lemma, in Arrays]
Realization.triple_array_set_hcell [lemma, in Arrays]
Realization.triple_array_get_hcell [lemma, in Arrays]
Realization.triple_array_length_hheader [lemma, in Arrays]
Realization.triple_alloc [lemma, in Arrays]
Realization.triple_ptr_add_nonneg [lemma, in Arrays]
Realization.triple_ptr_add [lemma, in Arrays]
Realization.val_new_hrecord_2 [definition, in Records]
Realization.val_alloc_hrecord [definition, in Records]
Realization.val_set_field [definition, in Records]
Realization.val_get_field [definition, in Records]
Realization.val_array_make [definition, in Arrays]
Realization.val_array_fill [definition, in Arrays]
Realization.val_array_set [definition, in Arrays]
Realization.val_array_get [definition, in Arrays]
Realization.val_array_length [definition, in Arrays]
Realization.val_alloc [axiom, in Arrays]
Realization.val_ptr_add [axiom, in Arrays]
trm:`{ _ := _ ; _ := _ } (trm_scope_ext) [notation, in Records]
trm:_ `. _ := _ [notation, in Records]
trm:_ `. _ [notation, in Records]
Records [library]
reducible [definition, in Triples]
reducible [definition, in LibSepReference]
reducible_val_inv [lemma, in Triples]
ref_greater [definition, in Basic]
rem [definition, in LibSepReference]
rem [definition, in WPgen]
remove [definition, in LibSepFmap]
remove_union_single_l [lemma, in LibSepFmap]
remove_disjoint_union_l [lemma, in LibSepFmap]
remove_single [lemma, in LibSepFmap]
rem_app [lemma, in LibSepReference]
repeat [definition, in Repr]
repeat_incr [definition, in Basic]
Repr [library]
right [definition, in Repr]
Rules [library]
S
safe [definition, in Triples]safe [definition, in LibSepReference]
SepSimplArgs [module, in LibSepReference]
SepSimplArgs.haffine [definition, in LibSepReference]
SepSimplArgs.haffine_hgc [lemma, in LibSepReference]
SepSimplArgs.haffine_hempty [lemma, in LibSepReference]
SepSimplArgs.haffine_hany [lemma, in LibSepReference]
SepSimplArgs.hempty [definition, in LibSepReference]
SepSimplArgs.hempty_eq_hpure_true [lemma, in LibSepReference]
SepSimplArgs.hempty_inv [lemma, in LibSepReference]
SepSimplArgs.hempty_intro [lemma, in LibSepReference]
SepSimplArgs.hexists [definition, in LibSepReference]
SepSimplArgs.hexists_inv [lemma, in LibSepReference]
SepSimplArgs.hexists_intro [lemma, in LibSepReference]
SepSimplArgs.hfalse_hstar_any [lemma, in LibSepReference]
SepSimplArgs.hforall [definition, in LibSepReference]
SepSimplArgs.hforall_specialize [lemma, in LibSepReference]
SepSimplArgs.hforall_inv [lemma, in LibSepReference]
SepSimplArgs.hforall_intro [lemma, in LibSepReference]
SepSimplArgs.hgc [definition, in LibSepReference]
SepSimplArgs.himpl [definition, in LibSepReference]
SepSimplArgs.himpl_hgc_r [lemma, in LibSepReference]
SepSimplArgs.himpl_htop_r [lemma, in LibSepReference]
SepSimplArgs.himpl_qwand_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hempty_hwand_same [lemma, in LibSepReference]
SepSimplArgs.himpl_hwand_r_inv [lemma, in LibSepReference]
SepSimplArgs.himpl_hwand_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hforall [lemma, in LibSepReference]
SepSimplArgs.himpl_hforall_l [lemma, in LibSepReference]
SepSimplArgs.himpl_hforall_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hexists [lemma, in LibSepReference]
SepSimplArgs.himpl_hexists_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hexists_l [lemma, in LibSepReference]
SepSimplArgs.himpl_hstar_hpure_l [lemma, in LibSepReference]
SepSimplArgs.himpl_hempty_hpure [lemma, in LibSepReference]
SepSimplArgs.himpl_hstar_hpure_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hstar_trans_r [lemma, in LibSepReference]
SepSimplArgs.himpl_hstar_trans_l [lemma, in LibSepReference]
SepSimplArgs.himpl_frame_lr [lemma, in LibSepReference]
SepSimplArgs.himpl_frame_r [lemma, in LibSepReference]
SepSimplArgs.himpl_frame_l [lemma, in LibSepReference]
SepSimplArgs.himpl_antisym [lemma, in LibSepReference]
SepSimplArgs.himpl_trans_r [lemma, in LibSepReference]
SepSimplArgs.himpl_trans [lemma, in LibSepReference]
SepSimplArgs.himpl_refl [lemma, in LibSepReference]
SepSimplArgs.hprop [definition, in LibSepReference]
SepSimplArgs.hprop_op_comm [lemma, in LibSepReference]
SepSimplArgs.hpure [definition, in LibSepReference]
SepSimplArgs.hpure_intro_hempty [lemma, in LibSepReference]
SepSimplArgs.hpure_inv_hempty [lemma, in LibSepReference]
SepSimplArgs.hpure_inv [lemma, in LibSepReference]
SepSimplArgs.hpure_intro [lemma, in LibSepReference]
SepSimplArgs.hsingle [definition, in LibSepReference]
SepSimplArgs.hsingle_inv [lemma, in LibSepReference]
SepSimplArgs.hsingle_intro [lemma, in LibSepReference]
SepSimplArgs.hstar [definition, in LibSepReference]
SepSimplArgs.hstar_hgc_hgc [lemma, in LibSepReference]
SepSimplArgs.hstar_hsingle_same_loc [lemma, in LibSepReference]
SepSimplArgs.hstar_htop_htop [lemma, in LibSepReference]
SepSimplArgs.hstar_hpure_r [lemma, in LibSepReference]
SepSimplArgs.hstar_hpure_l [lemma, in LibSepReference]
SepSimplArgs.hstar_hforall [lemma, in LibSepReference]
SepSimplArgs.hstar_hexists [lemma, in LibSepReference]
SepSimplArgs.hstar_hempty_r [lemma, in LibSepReference]
SepSimplArgs.hstar_hempty_l [lemma, in LibSepReference]
SepSimplArgs.hstar_assoc [lemma, in LibSepReference]
SepSimplArgs.hstar_comm [lemma, in LibSepReference]
SepSimplArgs.hstar_inv [lemma, in LibSepReference]
SepSimplArgs.hstar_intro [lemma, in LibSepReference]
SepSimplArgs.htop [definition, in LibSepReference]
SepSimplArgs.htop_eq [lemma, in LibSepReference]
SepSimplArgs.htop_intro [lemma, in LibSepReference]
SepSimplArgs.hwand [definition, in LibSepReference]
SepSimplArgs.hwand_inv [lemma, in LibSepReference]
SepSimplArgs.hwand_curry_eq [lemma, in LibSepReference]
SepSimplArgs.hwand_uncurry [lemma, in LibSepReference]
SepSimplArgs.hwand_curry [lemma, in LibSepReference]
SepSimplArgs.hwand_hpure_l [lemma, in LibSepReference]
SepSimplArgs.hwand_hempty_l [lemma, in LibSepReference]
SepSimplArgs.hwand_cancel [lemma, in LibSepReference]
SepSimplArgs.hwand_equiv [lemma, in LibSepReference]
SepSimplArgs.qimpl [definition, in LibSepReference]
SepSimplArgs.qimpl_refl [lemma, in LibSepReference]
SepSimplArgs.qwand [definition, in LibSepReference]
SepSimplArgs.qwand_specialize [lemma, in LibSepReference]
SepSimplArgs.qwand_cancel [lemma, in LibSepReference]
SepSimplArgs.qwand_equiv [lemma, in LibSepReference]
\GC (hprop_scope) [notation, in LibSepReference]
_ \−−∗ _ (hprop_scope) [notation, in LibSepReference]
_ \−∗ _ (hprop_scope) [notation, in LibSepReference]
_ \*+ _ (hprop_scope) [notation, in LibSepReference]
\Top (hprop_scope) [notation, in LibSepReference]
\[ _ ] (hprop_scope) [notation, in LibSepReference]
\forall _ .. _ , _ (hprop_scope) [notation, in LibSepReference]
\exists _ .. _ , _ (hprop_scope) [notation, in LibSepReference]
_ \* _ (hprop_scope) [notation, in LibSepReference]
_ ~~> _ (hprop_scope) [notation, in LibSepReference]
\[] (hprop_scope) [notation, in LibSepReference]
_ ===> _ (hprop_scope) [notation, in LibSepReference]
_ ==> _ (hprop_scope) [notation, in LibSepReference]
seval [inductive, in Triples]
seval [inductive, in LibSepReference]
seval_frame [lemma, in Triples]
seval_conseq [lemma, in Triples]
seval_of_eval [lemma, in Triples]
seval_if [lemma, in Triples]
seval_let [lemma, in Triples]
seval_seq [lemma, in Triples]
seval_app_fix [lemma, in Triples]
seval_app_fun [lemma, in Triples]
seval_fix [lemma, in Triples]
seval_fun [lemma, in Triples]
seval_sound [lemma, in Triples]
seval_correct [lemma, in Triples]
seval_safe [lemma, in Triples]
seval_terminates [lemma, in Triples]
seval_val_inv [lemma, in Triples]
seval_sind [definition, in Triples]
seval_ind [definition, in Triples]
seval_step [constructor, in Triples]
seval_val [constructor, in Triples]
seval_of_eval [lemma, in LibSepReference]
seval_if [lemma, in LibSepReference]
seval_app_arg2 [lemma, in LibSepReference]
seval_app_arg1 [lemma, in LibSepReference]
seval_let [lemma, in LibSepReference]
seval_seq [lemma, in LibSepReference]
seval_app_fix [lemma, in LibSepReference]
seval_app_fun [lemma, in LibSepReference]
seval_fix [lemma, in LibSepReference]
seval_fun [lemma, in LibSepReference]
seval_correct [lemma, in LibSepReference]
seval_safe [lemma, in LibSepReference]
seval_terminates [lemma, in LibSepReference]
seval_sind [definition, in LibSepReference]
seval_ind [definition, in LibSepReference]
seval_step [constructor, in LibSepReference]
seval_val [constructor, in LibSepReference]
single [definition, in LibSepFmap]
single_fresh [lemma, in LibSepFmap]
SizedStack [module, in Repr]
SizedStack.create [definition, in Repr]
SizedStack.data [definition, in Repr]
SizedStack.pop [definition, in Repr]
SizedStack.push [definition, in Repr]
SizedStack.size [definition, in Repr]
SizedStack.sizeof [definition, in Repr]
SizedStack.Stack [definition, in Repr]
SizedStack.top [definition, in Repr]
SizedStack.triple_top [lemma, in Repr]
SizedStack.triple_pop [lemma, in Repr]
SizedStack.triple_push [lemma, in Repr]
SizedStack.triple_sizeof [lemma, in Repr]
SizedStack.triple_create [lemma, in Repr]
smallest_fresh [definition, in LibSepFmap]
soundness_small_step [lemma, in Triples]
StateEq [section, in LibSepFmap]
StateEq.A [variable, in LibSepFmap]
StateEq.B [variable, in LibSepFmap]
step [inductive, in Triples]
step [inductive, in LibSepReference]
steps [inductive, in Triples]
steps [inductive, in LibSepReference]
stepsFrame [section, in Triples]
steps_trans [lemma, in Triples]
steps_of_step [lemma, in Triples]
steps_sind [definition, in Triples]
steps_ind [definition, in Triples]
steps_step [constructor, in Triples]
steps_refl [constructor, in Triples]
steps_trans [lemma, in LibSepReference]
steps_of_step [lemma, in LibSepReference]
steps_sind [definition, in LibSepReference]
steps_ind [definition, in LibSepReference]
steps_step [constructor, in LibSepReference]
steps_refl [constructor, in LibSepReference]
step_sind [definition, in Triples]
step_ind [definition, in Triples]
step_free [constructor, in Triples]
step_set [constructor, in Triples]
step_get [constructor, in Triples]
step_ref [constructor, in Triples]
step_rand [constructor, in Triples]
step_div [constructor, in Triples]
step_add [constructor, in Triples]
step_let [constructor, in Triples]
step_seq [constructor, in Triples]
step_if [constructor, in Triples]
step_app_fix [constructor, in Triples]
step_app_fun [constructor, in Triples]
step_fix [constructor, in Triples]
step_fun [constructor, in Triples]
step_let_ctx [constructor, in Triples]
step_seq_ctx [constructor, in Triples]
step_sind [definition, in LibSepReference]
step_ind [definition, in LibSepReference]
step_free [constructor, in LibSepReference]
step_set [constructor, in LibSepReference]
step_get [constructor, in LibSepReference]
step_ref [constructor, in LibSepReference]
step_ptr_add [constructor, in LibSepReference]
step_gt [constructor, in LibSepReference]
step_ge [constructor, in LibSepReference]
step_lt [constructor, in LibSepReference]
step_le [constructor, in LibSepReference]
step_mod [constructor, in LibSepReference]
step_div [constructor, in LibSepReference]
step_mul [constructor, in LibSepReference]
step_sub [constructor, in LibSepReference]
step_add [constructor, in LibSepReference]
step_neq [constructor, in LibSepReference]
step_eq [constructor, in LibSepReference]
step_rand [constructor, in LibSepReference]
step_opp [constructor, in LibSepReference]
step_neg [constructor, in LibSepReference]
step_let [constructor, in LibSepReference]
step_seq [constructor, in LibSepReference]
step_if [constructor, in LibSepReference]
step_app_fix [constructor, in LibSepReference]
step_app_fun [constructor, in LibSepReference]
step_fix [constructor, in LibSepReference]
step_fun [constructor, in LibSepReference]
step_app_arg2 [constructor, in LibSepReference]
step_app_arg1 [constructor, in LibSepReference]
step_let_ctx [constructor, in LibSepReference]
step_seq_ctx [constructor, in LibSepReference]
step_transfer [definition, in Basic]
striple [definition, in Triples]
striple_frame [lemma, in Triples]
striple_conseq [lemma, in Triples]
striple_sound [lemma, in Triples]
StructuralRules [module, in Triples]
StructuralRules.triple_hpure' [lemma, in Triples]
StructuralRules.triple_conseq_frame [lemma, in Triples]
StructuralRules.triple_hexists [axiom, in Triples]
StructuralRules.triple_hpure [axiom, in Triples]
StructuralRules.triple_conseq [axiom, in Triples]
StructuralRules.triple_frame [axiom, in Triples]
subst [definition, in LibSepReference]
subst [definition, in LibSepMinimal]
subst_trm_funs [lemma, in LibSepReference]
subst_eq_isubst_one [lemma, in LibSepReference]
succ_using_incr [definition, in Basic]
succ_using_incr_attempt [definition, in Basic]
SummaryHprop [module, in Wand]
SummaryHprop.hempty [definition, in Wand]
SummaryHprop.hexists [definition, in Wand]
SummaryHprop.hforall [definition, in Wand]
SummaryHprop.hsingle [definition, in Wand]
SummaryHprop.hstar [definition, in Wand]
SummaryHprop.ReaminingOperatorsDerived [module, in Wand]
SummaryHprop.ReaminingOperatorsDerived.hand [definition, in Wand]
SummaryHprop.ReaminingOperatorsDerived.hor [definition, in Wand]
SummaryHprop.ReaminingOperatorsDerived.hpure [definition, in Wand]
SummaryHprop.ReaminingOperatorsDerived.hwand [definition, in Wand]
SummaryHprop.ReaminingOperatorsDerived.qwand [definition, in Wand]
SummaryHprop.ReaminingOperatorsDirect [module, in Wand]
SummaryHprop.ReaminingOperatorsDirect.hand [definition, in Wand]
SummaryHprop.ReaminingOperatorsDirect.hor [definition, in Wand]
SummaryHprop.ReaminingOperatorsDirect.hpure [definition, in Wand]
SummaryHprop.ReaminingOperatorsDirect.hwand [definition, in Wand]
SummaryHprop.ReaminingOperatorsDirect.qwand [definition, in Wand]
Syntax [module, in Triples]
Syntax.heap [definition, in Triples]
Syntax.Inhab_val [instance, in Triples]
Syntax.subst [definition, in Triples]
Syntax.trm [inductive, in Triples]
Syntax.trm_sind [definition, in Triples]
Syntax.trm_rec [definition, in Triples]
Syntax.trm_ind [definition, in Triples]
Syntax.trm_rect [definition, in Triples]
Syntax.trm_if [constructor, in Triples]
Syntax.trm_let [constructor, in Triples]
Syntax.trm_seq [constructor, in Triples]
Syntax.trm_app [constructor, in Triples]
Syntax.trm_fix [constructor, in Triples]
Syntax.trm_fun [constructor, in Triples]
Syntax.trm_var [constructor, in Triples]
Syntax.trm_val [constructor, in Triples]
Syntax.val [inductive, in Triples]
Syntax.val_sind [definition, in Triples]
Syntax.val_rec [definition, in Triples]
Syntax.val_ind [definition, in Triples]
Syntax.val_rect [definition, in Triples]
Syntax.val_rand [constructor, in Triples]
Syntax.val_div [constructor, in Triples]
Syntax.val_add [constructor, in Triples]
Syntax.val_free [constructor, in Triples]
Syntax.val_set [constructor, in Triples]
Syntax.val_get [constructor, in Triples]
Syntax.val_ref [constructor, in Triples]
Syntax.val_fix [constructor, in Triples]
Syntax.val_fun [constructor, in Triples]
Syntax.val_loc [constructor, in Triples]
Syntax.val_int [constructor, in Triples]
Syntax.val_bool [constructor, in Triples]
Syntax.val_unit [constructor, in Triples]
T
tail [definition, in Repr]tail [definition, in Records]
terminates [inductive, in Triples]
terminates [inductive, in LibSepReference]
terminates_sind [definition, in Triples]
terminates_ind [definition, in Triples]
terminates_step [constructor, in Triples]
terminates_sind [definition, in LibSepReference]
terminates_ind [definition, in LibSepReference]
terminates_step [constructor, in LibSepReference]
test_counter [definition, in Repr]
TexanTriples [module, in WPsem]
TexanTriples.incr [axiom, in WPsem]
TexanTriples.texan_triple_equiv [lemma, in WPsem]
TexanTriples.triple_incr [axiom, in WPsem]
TexanTriples.triple_free' [axiom, in WPsem]
TexanTriples.triple_set' [axiom, in WPsem]
TexanTriples.triple_ref [axiom, in WPsem]
TexanTriples.WpSpecRef [section, in WPsem]
TexanTriples.wp_free' [lemma, in WPsem]
TexanTriples.wp_set' [lemma, in WPsem]
TexanTriples.wp_free [lemma, in WPsem]
TexanTriples.wp_set [lemma, in WPsem]
TexanTriples.wp_get [lemma, in WPsem]
TexanTriples.wp_ref_3 [lemma, in WPsem]
TexanTriples.wp_ref_2 [lemma, in WPsem]
TexanTriples.wp_ref_1 [lemma, in WPsem]
TexanTriples.wp_ref_0 [lemma, in WPsem]
TexanTriples.wp_ref [axiom, in WPsem]
transfer [definition, in Basic]
tree [inductive, in Repr]
treeacc [definition, in Repr]
treesum [definition, in Repr]
tree_copy [definition, in Repr]
tree_sub_wf [lemma, in Repr]
tree_sub_sind [definition, in Repr]
tree_sub_ind [definition, in Repr]
tree_sub_2 [constructor, in Repr]
tree_sub_1 [constructor, in Repr]
tree_sub [inductive, in Repr]
tree_sind [definition, in Repr]
tree_rec [definition, in Repr]
tree_ind [definition, in Repr]
tree_rect [definition, in Repr]
triple [definition, in Triples]
triple [definition, in LibSepReference]
triple [definition, in LibSepMinimal]
Triples [library]
triple_named_heap [lemma, in Triples]
triple_hexists [lemma, in Triples]
triple_hpure [lemma, in Triples]
triple_frame [lemma, in Triples]
triple_conseq [lemma, in Triples]
triple_dealloc_hrecord [axiom, in LibSepReference]
triple_new_hrecord_3 [axiom, in LibSepReference]
triple_new_hrecord_2 [axiom, in LibSepReference]
triple_alloc_hrecord [axiom, in LibSepReference]
triple_set_field_hrecord [axiom, in LibSepReference]
triple_get_field_hrecord [axiom, in LibSepReference]
triple_hand_r [lemma, in LibSepReference]
triple_hand_l [lemma, in LibSepReference]
triple_hor [lemma, in LibSepReference]
triple_of_wpgen [lemma, in LibSepReference]
triple_ptr_add_nat [lemma, in LibSepReference]
triple_ptr_add [lemma, in LibSepReference]
triple_gt [lemma, in LibSepReference]
triple_ge [lemma, in LibSepReference]
triple_lt [lemma, in LibSepReference]
triple_le [lemma, in LibSepReference]
triple_mod [lemma, in LibSepReference]
triple_mul [lemma, in LibSepReference]
triple_sub [lemma, in LibSepReference]
triple_neq [lemma, in LibSepReference]
triple_eq [lemma, in LibSepReference]
triple_opp [lemma, in LibSepReference]
triple_neg [lemma, in LibSepReference]
triple_rand [lemma, in LibSepReference]
triple_div [lemma, in LibSepReference]
triple_add [lemma, in LibSepReference]
triple_binop [lemma, in LibSepReference]
triple_unop [lemma, in LibSepReference]
triple_binop' [lemma, in LibSepReference]
triple_unop' [lemma, in LibSepReference]
triple_free [lemma, in LibSepReference]
triple_free' [lemma, in LibSepReference]
triple_set [lemma, in LibSepReference]
triple_get [lemma, in LibSepReference]
triple_ref [lemma, in LibSepReference]
triple_app_fix_direct [lemma, in LibSepReference]
triple_app_fix [lemma, in LibSepReference]
triple_app_fun_direct [lemma, in LibSepReference]
triple_app_fun [lemma, in LibSepReference]
triple_if [lemma, in LibSepReference]
triple_let_val [lemma, in LibSepReference]
triple_let [lemma, in LibSepReference]
triple_seq [lemma, in LibSepReference]
triple_fix [lemma, in LibSepReference]
triple_fun [lemma, in LibSepReference]
triple_val_minimal [lemma, in LibSepReference]
triple_val [lemma, in LibSepReference]
triple_eval_like [lemma, in LibSepReference]
triple_ramified_frame [lemma, in LibSepReference]
triple_conseq_frame [lemma, in LibSepReference]
triple_named_heap [lemma, in LibSepReference]
triple_hpure' [axiom, in LibSepReference]
triple_hwand_hpure_l [lemma, in LibSepReference]
triple_hforall [lemma, in LibSepReference]
triple_hexists [lemma, in LibSepReference]
triple_hpure [lemma, in LibSepReference]
triple_frame [lemma, in LibSepReference]
triple_conseq [lemma, in LibSepReference]
triple_sound [lemma, in LibSepReference]
triple_cps_append [lemma, in Repr]
triple_cps_append_aux [lemma, in Repr]
triple_cps_facto [lemma, in Repr]
triple_cps_facto_aux [lemma, in Repr]
triple_mlength_using_miter [lemma, in Repr]
triple_miter [lemma, in Repr]
triple_repeat [lemma, in Repr]
triple_test_counter [lemma, in Repr]
triple_apply_counter_abstract [lemma, in Repr]
triple_create_counter_abstract [lemma, in Repr]
triple_create_counter [lemma, in Repr]
triple_mtreesum [lemma, in Repr]
triple_tree_copy [lemma, in Repr]
triple_mnode' [lemma, in Repr]
triple_mnode [lemma, in Repr]
triple_mrev [lemma, in Repr]
triple_mfree [lemma, in Repr]
triple_mlength' [lemma, in Repr]
triple_mlength [lemma, in Repr]
triple_mcopy' [lemma, in Repr]
triple_mcopy [lemma, in Repr]
triple_mcons' [lemma, in Repr]
triple_mcons [lemma, in Repr]
triple_mnil' [lemma, in Repr]
triple_mnil [lemma, in Repr]
triple_append [lemma, in Repr]
triple_app_fun_from_wpgen [axiom, in WPgen]
triple_var' [lemma, in WPgen]
triple_var [lemma, in WPgen]
triple_set [lemma, in Rules]
triple_get [lemma, in Rules]
triple_free [lemma, in Rules]
triple_free' [lemma, in Rules]
triple_ref' [lemma, in Rules]
triple_ref [lemma, in Rules]
triple_rand [lemma, in Rules]
triple_div [lemma, in Rules]
triple_add' [lemma, in Rules]
triple_add [lemma, in Rules]
triple_app_fix [lemma, in Rules]
triple_app_fun [lemma, in Rules]
triple_fix [lemma, in Rules]
triple_fun [lemma, in Rules]
triple_val' [lemma, in Rules]
triple_val_minimal [lemma, in Rules]
triple_val [lemma, in Rules]
triple_if [lemma, in Rules]
triple_if_case [lemma, in Rules]
triple_let [lemma, in Rules]
triple_seq [lemma, in Rules]
triple_incr [lemma, in LibSepMinimal]
triple_free [lemma, in LibSepMinimal]
triple_set [lemma, in LibSepMinimal]
triple_get [lemma, in LibSepMinimal]
triple_ref [lemma, in LibSepMinimal]
triple_rand [lemma, in LibSepMinimal]
triple_div [lemma, in LibSepMinimal]
triple_add [lemma, in LibSepMinimal]
triple_let [lemma, in LibSepMinimal]
triple_app_fix [lemma, in LibSepMinimal]
triple_if [lemma, in LibSepMinimal]
triple_fix [lemma, in LibSepMinimal]
triple_val [lemma, in LibSepMinimal]
triple_hpure [lemma, in LibSepMinimal]
triple_hexists [lemma, in LibSepMinimal]
triple_frame [lemma, in LibSepMinimal]
triple_conseq [lemma, in LibSepMinimal]
triple_mcons [lemma, in Records]
triple_new_hrecord_2 [axiom, in Records]
triple_set_field_hrecord [axiom, in Records]
triple_set_field_hfields [axiom, in Records]
triple_set_field [axiom, in Records]
triple_get_field_hrecord [axiom, in Records]
triple_get_field_hfields [axiom, in Records]
triple_get_field [axiom, in Records]
triple_app_fix_from_wpgen [lemma, in WPsound]
triple_app_fun_from_wpgen [lemma, in WPsound]
triple_of_wpgen [lemma, in WPsound]
triple_factoimp' [lemma, in Basic]
triple_factoimp_aux' [lemma, in Basic]
triple_factoimp_zero [lemma, in Basic]
triple_factoimp_aux_zero [lemma, in Basic]
triple_factoimp [lemma, in Basic]
triple_factoimp_aux [lemma, in Basic]
triple_step_transfer [lemma, in Basic]
triple_repeat_incr' [lemma, in Basic]
triple_repeat_incr_incorrect [lemma, in Basic]
triple_repeat_incr' [lemma, in Basic]
triple_repeat_incr [lemma, in Basic]
triple_factorec [lemma, in Basic]
triple_two_dice [lemma, in Basic]
triple_rand [axiom, in Basic]
triple_get_and_free [lemma, in Basic]
triple_succ_using_incr [lemma, in Basic]
triple_succ_using_incr_attempt' [lemma, in Basic]
triple_succ_using_incr_attempt [lemma, in Basic]
triple_ref_with_frame [axiom, in Basic]
triple_ref_greater [lemma, in Basic]
triple_ref' [axiom, in Basic]
triple_ref [axiom, in Basic]
triple_incr_first_derived [lemma, in Basic]
triple_incr_first' [lemma, in Basic]
triple_incr_first [lemma, in Basic]
triple_aliased_call [lemma, in Basic]
triple_incr_two_aliased [lemma, in Basic]
triple_aliased_call [lemma, in Basic]
triple_incr_two [lemma, in Basic]
triple_example_let [lemma, in Basic]
triple_incr' [lemma, in Basic]
triple_incr [lemma, in Basic]
triple_hgc_post [axiom, in Affine]
triple_hany_pre [axiom, in Affine]
triple_hany_post [axiom, in Affine]
triple_conseq_frame [axiom, in WPsem]
triple_app_fun [axiom, in WPsem]
triple_if [axiom, in WPsem]
triple_fun [axiom, in WPsem]
triple_let [axiom, in WPsem]
triple_seq [axiom, in WPsem]
triple_val [axiom, in WPsem]
triple_ramified_frame [axiom, in WPsem]
triple_hpure_with_wp [lemma, in WPsem]
triple_hpure [axiom, in WPsem]
triple_array_set_hseg [axiom, in Arrays]
triple_array_get_hseg [axiom, in Arrays]
triple_array_make_hseg [axiom, in Arrays]
triple_array_set_hcell [axiom, in Arrays]
triple_array_get_hcell [axiom, in Arrays]
triple_array_length_hheader [axiom, in Arrays]
triple_array_set [axiom, in Arrays]
triple_array_get [axiom, in Arrays]
triple_array_length [axiom, in Arrays]
triple_array_make' [axiom, in Arrays]
triple_array_make [axiom, in Arrays]
trm [inductive, in LibSepReference]
trm [inductive, in LibSepMinimal]
trms [definition, in LibSepReference]
trms_to_vals_spec [lemma, in LibSepReference]
trms_to_vals [definition, in LibSepReference]
trms_vals_cons [lemma, in LibSepReference]
trms_vals_nil [lemma, in LibSepReference]
trms_vals [definition, in LibSepReference]
trm_is_val [definition, in Triples]
trm_apps_of_trm_demo [lemma, in LibSepReference]
trm_fixs [definition, in LibSepReference]
trm_funs [definition, in LibSepReference]
trm_apps [definition, in LibSepReference]
trm_is_val [definition, in LibSepReference]
trm_sind [definition, in LibSepReference]
trm_rec [definition, in LibSepReference]
trm_ind [definition, in LibSepReference]
trm_rect [definition, in LibSepReference]
trm_if [constructor, in LibSepReference]
trm_let [constructor, in LibSepReference]
trm_seq [constructor, in LibSepReference]
trm_app [constructor, in LibSepReference]
trm_fix [constructor, in LibSepReference]
trm_fun [constructor, in LibSepReference]
trm_var [constructor, in LibSepReference]
trm_val [constructor, in LibSepReference]
trm_sind [definition, in LibSepMinimal]
trm_rec [definition, in LibSepMinimal]
trm_ind [definition, in LibSepMinimal]
trm_rect [definition, in LibSepMinimal]
trm_if [constructor, in LibSepMinimal]
trm_let [constructor, in LibSepMinimal]
trm_app [constructor, in LibSepMinimal]
trm_fix [constructor, in LibSepMinimal]
trm_var [constructor, in LibSepMinimal]
trm_val [constructor, in LibSepMinimal]
two_dice [definition, in Basic]
U
union [definition, in LibSepFmap]union_eq_cancel_4' [lemma, in LibSepFmap]
union_eq_cancel_4 [lemma, in LibSepFmap]
union_eq_cancel_3' [lemma, in LibSepFmap]
union_eq_cancel_3 [lemma, in LibSepFmap]
union_eq_cancel_2' [lemma, in LibSepFmap]
union_eq_cancel_2 [lemma, in LibSepFmap]
union_eq_cancel_1' [lemma, in LibSepFmap]
union_eq_cancel_1 [lemma, in LibSepFmap]
union_eq_inv_of_disjoint [lemma, in LibSepFmap]
union_assoc [lemma, in LibSepFmap]
union_comm_of_agree [lemma, in LibSepFmap]
union_comm_of_disjoint [lemma, in LibSepFmap]
union_eq_empty_inv_r [lemma, in LibSepFmap]
union_eq_empty_inv_l [lemma, in LibSepFmap]
union_empty_r [lemma, in LibSepFmap]
union_empty_l [lemma, in LibSepFmap]
union_self [lemma, in LibSepFmap]
update [definition, in LibSepFmap]
update_union_not_l [lemma, in LibSepFmap]
update_union_not_r [lemma, in LibSepFmap]
update_union_r [lemma, in LibSepFmap]
update_union_l [lemma, in LibSepFmap]
update_single [lemma, in LibSepFmap]
update_empty [lemma, in LibSepFmap]
update_eq_union_single [lemma, in LibSepFmap]
V
val [inductive, in LibSepReference]val [inductive, in LibSepMinimal]
vals [definition, in LibSepReference]
val_dealloc_hrecord [axiom, in LibSepReference]
val_new_hrecord_3 [axiom, in LibSepReference]
val_new_hrecord_2 [axiom, in LibSepReference]
val_alloc_hrecord [axiom, in LibSepReference]
val_set_field [axiom, in LibSepReference]
val_get_field [axiom, in LibSepReference]
val_fixs [definition, in LibSepReference]
val_funs [definition, in LibSepReference]
val_sind [definition, in LibSepReference]
val_rec [definition, in LibSepReference]
val_ind [definition, in LibSepReference]
val_rect [definition, in LibSepReference]
val_error [constructor, in LibSepReference]
val_uninit [constructor, in LibSepReference]
val_fix [constructor, in LibSepReference]
val_fun [constructor, in LibSepReference]
val_prim [constructor, in LibSepReference]
val_loc [constructor, in LibSepReference]
val_int [constructor, in LibSepReference]
val_bool [constructor, in LibSepReference]
val_unit [constructor, in LibSepReference]
val_ptr_add [constructor, in LibSepReference]
val_gt [constructor, in LibSepReference]
val_ge [constructor, in LibSepReference]
val_lt [constructor, in LibSepReference]
val_le [constructor, in LibSepReference]
val_rand [constructor, in LibSepReference]
val_mod [constructor, in LibSepReference]
val_div [constructor, in LibSepReference]
val_mul [constructor, in LibSepReference]
val_sub [constructor, in LibSepReference]
val_neq [constructor, in LibSepReference]
val_add [constructor, in LibSepReference]
val_eq [constructor, in LibSepReference]
val_opp [constructor, in LibSepReference]
val_neg [constructor, in LibSepReference]
val_free [constructor, in LibSepReference]
val_set [constructor, in LibSepReference]
val_get [constructor, in LibSepReference]
val_ref [constructor, in LibSepReference]
val_sind [definition, in LibSepMinimal]
val_rec [definition, in LibSepMinimal]
val_ind [definition, in LibSepMinimal]
val_rect [definition, in LibSepMinimal]
val_fix [constructor, in LibSepMinimal]
val_prim [constructor, in LibSepMinimal]
val_loc [constructor, in LibSepMinimal]
val_int [constructor, in LibSepMinimal]
val_bool [constructor, in LibSepMinimal]
val_unit [constructor, in LibSepMinimal]
val_rand [constructor, in LibSepMinimal]
val_div [constructor, in LibSepMinimal]
val_add [constructor, in LibSepMinimal]
val_free [constructor, in LibSepMinimal]
val_set [constructor, in LibSepMinimal]
val_get [constructor, in LibSepMinimal]
val_ref [constructor, in LibSepMinimal]
val_new_hrecord_2 [axiom, in Records]
val_set_field [axiom, in Records]
val_get_field [axiom, in Records]
val_array_set [axiom, in Arrays]
val_array_get [axiom, in Arrays]
val_array_length [axiom, in Arrays]
val_array_make [axiom, in Arrays]
var [definition, in LibSepVar]
var [definition, in LibSepMinimal]
vars [definition, in LibSepReference]
vars [definition, in LibSepVar]
var_funs_exec_eq [lemma, in LibSepReference]
var_funs_exec [definition, in LibSepReference]
Var_funs_exec [section, in LibSepReference]
var_funs [definition, in LibSepReference]
var_fresh_var_seq_ge [lemma, in LibSepVar]
var_fresh_var_seq_lt [lemma, in LibSepVar]
Var_seq [section, in LibSepVar]
var_seq [definition, in LibSepVar]
var_fresh_mem_inv [lemma, in LibSepVar]
var_fresh [definition, in LibSepVar]
var_eq_spec [lemma, in LibSepVar]
var_eq [definition, in LibSepVar]
var_eq [definition, in LibSepMinimal]
W
Wand [library]wp [definition, in LibSepReference]
wp [definition, in WPsem]
WpFromTriple [module, in WPsem]
WpFromTriple.wp_equiv_1 [lemma, in WPsem]
WpFromTriple.wp_1 [definition, in WPsem]
WpFromTriple2 [module, in WPsem]
WpFromTriple2.wp_equiv_2 [lemma, in WPsem]
WpFromTriple2.wp_2 [definition, in WPsem]
wpgen [definition, in LibSepReference]
wpgen [definition, in WPgen]
WPgen [library]
WpgenExec1 [module, in WPgen]
WpgenExec1.triple_incr [lemma, in WPgen]
WpgenExec1.triple_app_fun_from_wpgen [axiom, in WPgen]
WpgenExec1.triple_app_fun [axiom, in WPgen]
WpgenExec1.wpgen [definition, in WPgen]
WpgenExec1.wpgen_frame [lemma, in WPgen]
WpgenExec1.wpgen_conseq [lemma, in WPgen]
WpgenExec1.wpgen_sound [axiom, in WPgen]
WpgenExec2 [module, in WPgen]
WpgenExec2.wpgen [definition, in WPgen]
WPgenRec [module, in WPgen]
WPgenRec.ExampleLocalFunWpgenRec [module, in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.forloop [definition, in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_forloop [lemma, in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_incrtwice' [lemma, in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_incrtwice [lemma, in WPgen]
WPgenRec.triple_app_fun_from_wpgen [axiom, in WPgen]
WPgenRec.wpgen [definition, in WPgen]
WPgenRec.wpgen_fix [definition, in WPgen]
WPgenRec.wpgen_fun_eq [lemma, in WPgen]
WPgenRec.wpgen_fun [definition, in WPgen]
WPgenRec.wpgen_fun' [definition, in WPgen]
WPgenRec.xfun_nospec_lemma [lemma, in WPgen]
WPgenRec.xfun_spec_lemma [lemma, in WPgen]
Fix _ _ := _ [notation, in WPgen]
Fun _ := _ [notation, in WPgen]
WPgenWithNotation [module, in WPgen]
WPgenWithNotation.triple_incr [lemma, in WPgen]
WPgenWithNotation.triple_app_fun_from_wpgen [axiom, in WPgen]
wpgen_sound [lemma, in LibSepReference]
wpgen_app_sound [lemma, in LibSepReference]
wpgen_if_sound [lemma, in LibSepReference]
wpgen_let_sound [lemma, in LibSepReference]
wpgen_seq_sound [lemma, in LibSepReference]
wpgen_fix_sound [lemma, in LibSepReference]
wpgen_fun_sound [lemma, in LibSepReference]
wpgen_val_sound [lemma, in LibSepReference]
wpgen_fail_sound [lemma, in LibSepReference]
wpgen_app [definition, in LibSepReference]
wpgen_if_trm [definition, in LibSepReference]
wpgen_if [definition, in LibSepReference]
wpgen_let [definition, in LibSepReference]
wpgen_seq [definition, in LibSepReference]
wpgen_var [definition, in LibSepReference]
wpgen_fix [definition, in LibSepReference]
wpgen_fun [definition, in LibSepReference]
wpgen_val [definition, in LibSepReference]
wpgen_fail [definition, in LibSepReference]
wpgen_app [definition, in WPgen]
wpgen_var [definition, in WPgen]
wpgen_fail [definition, in WPgen]
wpgen_if [definition, in WPgen]
wpgen_let [definition, in WPgen]
wpgen_val [definition, in WPgen]
wpgen_seq [definition, in WPgen]
wpgen_sound [lemma, in WPsound]
wpgen_sound_induct [lemma, in WPsound]
wpgen_fix_val_sound [lemma, in WPsound]
wpgen_fun_val_sound [lemma, in WPsound]
wpgen_fix_sound [lemma, in WPsound]
wpgen_fun_sound [lemma, in WPsound]
wpgen_fail_sound [lemma, in WPsound]
wpgen_app_sound [lemma, in WPsound]
wpgen_if_sound [lemma, in WPsound]
wpgen_let_sound [lemma, in WPsound]
wpgen_val_sound [lemma, in WPsound]
wpgen_seq_sound [lemma, in WPsound]
wpgen_sound_seq_3 [axiom, in WPsound]
wpgen_sound_seq_2 [axiom, in WPsound]
wpgen_sound_seq_1 [axiom, in WPsound]
WPsem [library]
WPsound [library]
wp_sound [lemma, in LibSepReference]
wp_if_case [lemma, in LibSepReference]
wp_if [lemma, in LibSepReference]
wp_let [lemma, in LibSepReference]
wp_seq [lemma, in LibSepReference]
wp_app_fix [lemma, in LibSepReference]
wp_app_fun [lemma, in LibSepReference]
wp_fix [lemma, in LibSepReference]
wp_fun [lemma, in LibSepReference]
wp_val [lemma, in LibSepReference]
wp_eval_like [lemma, in LibSepReference]
wp_ramified_trans [lemma, in LibSepReference]
wp_conseq_frame [lemma, in LibSepReference]
wp_ramified [lemma, in LibSepReference]
wp_frame [lemma, in LibSepReference]
wp_conseq [lemma, in LibSepReference]
wp_equiv [lemma, in LibSepReference]
wp_if [axiom, in WPgen]
wp_var [lemma, in WPgen]
wp_let [axiom, in WPgen]
wp_seq [axiom, in WPgen]
wp_fun [axiom, in WPgen]
wp_val [axiom, in WPgen]
wp_equiv_iff_wp_pre_and_wp_weakest [lemma, in WPsem]
wp_unique [lemma, in WPsem]
wp_conseq_frame [lemma, in WPsem]
wp_conseq_frame_trans [lemma, in WPsem]
wp_app_fix [lemma, in WPsem]
wp_app_fun [lemma, in WPsem]
wp_if' [lemma, in WPsem]
wp_if [lemma, in WPsem]
wp_fix [lemma, in WPsem]
wp_fun [lemma, in WPsem]
wp_let [lemma, in WPsem]
wp_seq [lemma, in WPsem]
wp_val [lemma, in WPsem]
wp_frame_of_wp_ramified [lemma, in WPsem]
wp_conseq_of_wp_ramified [lemma, in WPsem]
wp_ramified_trans [lemma, in WPsem]
wp_ramified [lemma, in WPsem]
wp_conseq_trans [lemma, in WPsem]
wp_conseq [lemma, in WPsem]
wp_frame_trans [lemma, in WPsem]
wp_frame [lemma, in WPsem]
wp_weakest [lemma, in WPsem]
wp_pre [lemma, in WPsem]
wp_equiv [lemma, in WPsem]
X
Xaffine [module, in Affine]Xaffine.xaffine_demo [lemma, in Affine]
xapp_set_field_lemma [axiom, in LibSepReference]
xapp_get_field_lemma [axiom, in LibSepReference]
xapp_simpl_lemma [lemma, in LibSepReference]
xapp_lemma [lemma, in LibSepReference]
xapp_lemma [lemma, in WPgen]
xapp_set_field_lemma [lemma, in Records]
xapp_get_field_lemma [lemma, in Records]
xchange_lemma [lemma, in LibSepMinimal]
xconseq_lemma [lemma, in WPgen]
xfix_nospec_lemma [lemma, in LibSepReference]
xfix_spec_lemma [lemma, in LibSepReference]
xframe_lemma [lemma, in WPgen]
xfun_nospec_lemma [lemma, in LibSepReference]
xfun_spec_lemma [lemma, in LibSepReference]
XGC [module, in Affine]
XGC.mkstruct_hgc [axiom, in Affine]
XGC.xgc_keep_demo [lemma, in Affine]
XGC.xgc_post_lemma [lemma, in Affine]
XGC.xgc_keep_demo [lemma, in Affine]
XGC.xgc_demo [lemma, in Affine]
XGC.xgc_lemma [lemma, in Affine]
xif_lemma [lemma, in LibSepReference]
xlet_lemma [lemma, in LibSepReference]
xlet_lemma [lemma, in WPgen]
xseq_lemma [lemma, in LibSepReference]
xseq_lemma [lemma, in WPgen]
XsimplDemo [module, in Wand]
XsimplDemo.xsimpl_hwand_frame [lemma, in Wand]
XsimplDemo.xsimpl_demo_qwand_cancel [lemma, in Wand]
XsimplDemo.xsimpl_demo_hwand_iter_2 [lemma, in Wand]
XsimplDemo.xsimpl_demo_hwand_iter [lemma, in Wand]
XsimplDemo.xsimpl_demo_himpl_hwand_r [lemma, in Wand]
XsimplDemo.xsimpl_demo_hwand_cancel_partial [lemma, in Wand]
XsimplDemo.xsimpl_demo_hwand_cancel [lemma, in Wand]
XsimplExtended [module, in Affine]
XsimplExtended.xsimpl_xaffine_demo [lemma, in Affine]
XsimplExtended.xsimpl_xgc_demo [lemma, in Affine]
XsimplParams [module, in LibSepSimpl]
XsimplParams.haffine [axiom, in LibSepSimpl]
XsimplParams.haffine_hempty [axiom, in LibSepSimpl]
XsimplParams.hempty [axiom, in LibSepSimpl]
XsimplParams.hexists [axiom, in LibSepSimpl]
XsimplParams.hforall [axiom, in LibSepSimpl]
XsimplParams.hgc [axiom, in LibSepSimpl]
XsimplParams.himpl [axiom, in LibSepSimpl]
XsimplParams.himpl_hgc_r [axiom, in LibSepSimpl]
XsimplParams.himpl_htop_r [axiom, in LibSepSimpl]
XsimplParams.himpl_hforall_r [axiom, in LibSepSimpl]
XsimplParams.himpl_hexists_r [axiom, in LibSepSimpl]
XsimplParams.himpl_hexists_l [axiom, in LibSepSimpl]
XsimplParams.himpl_hstar_hpure_l [axiom, in LibSepSimpl]
XsimplParams.himpl_hempty_hpure [axiom, in LibSepSimpl]
XsimplParams.himpl_frame_lr [axiom, in LibSepSimpl]
XsimplParams.himpl_antisym [axiom, in LibSepSimpl]
XsimplParams.himpl_trans [axiom, in LibSepSimpl]
XsimplParams.himpl_refl [axiom, in LibSepSimpl]
XsimplParams.hprop [axiom, in LibSepSimpl]
XsimplParams.hpure [axiom, in LibSepSimpl]
XsimplParams.hstar [axiom, in LibSepSimpl]
XsimplParams.hstar_hgc_hgc [axiom, in LibSepSimpl]
XsimplParams.hstar_htop_htop [axiom, in LibSepSimpl]
XsimplParams.hstar_hforall [axiom, in LibSepSimpl]
XsimplParams.hstar_hexists [axiom, in LibSepSimpl]
XsimplParams.hstar_assoc [axiom, in LibSepSimpl]
XsimplParams.hstar_comm [axiom, in LibSepSimpl]
XsimplParams.hstar_hempty_r [axiom, in LibSepSimpl]
XsimplParams.hstar_hempty_l [axiom, in LibSepSimpl]
XsimplParams.htop [axiom, in LibSepSimpl]
XsimplParams.hwand [axiom, in LibSepSimpl]
XsimplParams.hwand_cancel [axiom, in LibSepSimpl]
XsimplParams.hwand_hempty_l [axiom, in LibSepSimpl]
XsimplParams.hwand_curry_eq [axiom, in LibSepSimpl]
XsimplParams.hwand_equiv [axiom, in LibSepSimpl]
XsimplParams.qimpl [definition, in LibSepSimpl]
XsimplParams.qwand [axiom, in LibSepSimpl]
XsimplParams.qwand_specialize [axiom, in LibSepSimpl]
XsimplParams.qwand_equiv [axiom, in LibSepSimpl]
\forall _ .. _ , _ (heap_scope) [notation, in LibSepSimpl]
\exists _ .. _ , _ (heap_scope) [notation, in LibSepSimpl]
_ \−−∗ _ (heap_scope) [notation, in LibSepSimpl]
_ \−∗ _ (heap_scope) [notation, in LibSepSimpl]
_ \*+ _ (heap_scope) [notation, in LibSepSimpl]
_ \* _ (heap_scope) [notation, in LibSepSimpl]
\GC (heap_scope) [notation, in LibSepSimpl]
\Top (heap_scope) [notation, in LibSepSimpl]
\[ _ ] (heap_scope) [notation, in LibSepSimpl]
\[] (heap_scope) [notation, in LibSepSimpl]
_ ===> _ (heap_scope) [notation, in LibSepSimpl]
_ ==> _ (heap_scope) [notation, in LibSepSimpl]
XsimplSetup [module, in LibSepSimpl]
XsimplSetup.demo_hstars_simpl_2 [lemma, in LibSepSimpl]
XsimplSetup.demo_hstars_simpl_1 [lemma, in LibSepSimpl]
XsimplSetup.demo_hstars_pick_1 [lemma, in LibSepSimpl]
XsimplSetup.himpl_lr_hgc [lemma, in LibSepSimpl]
XsimplSetup.himpl_lr_htop [lemma, in LibSepSimpl]
XsimplSetup.himpl_lr_qwand_unify [lemma, in LibSepSimpl]
XsimplSetup.himpl_lr_refl [lemma, in LibSepSimpl]
XsimplSetup.himpl_hstar_trans_l [lemma, in LibSepSimpl]
XsimplSetup.himpl_of_eq_sym [lemma, in LibSepSimpl]
XsimplSetup.himpl_of_eq [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_demo_0 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_demo [lemma, in LibSepSimpl]
XsimplSetup.hstars_simpl_pick_lemma [lemma, in LibSepSimpl]
XsimplSetup.hstars_simpl_cancel [lemma, in LibSepSimpl]
XsimplSetup.hstars_simpl_keep [lemma, in LibSepSimpl]
XsimplSetup.hstars_simpl_start [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_9 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_8 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_7 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_6 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_5 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_4 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_3 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_2 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_last_1 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_9 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_8 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_7 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_6 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_5 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_4 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_3 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_2 [lemma, in LibSepSimpl]
XsimplSetup.hstars_pick_1 [lemma, in LibSepSimpl]
XsimplSetup.hstars_last [definition, in LibSepSimpl]
XsimplSetup.hstars_flip_9 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_8 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_7 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_6 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_5 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_4 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_3 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_2 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_1 [lemma, in LibSepSimpl]
XsimplSetup.hstars_flip_0 [lemma, in LibSepSimpl]
XsimplSetup.hstar_comm_assoc [lemma, in LibSepSimpl]
XsimplSetup.Id [definition, in LibSepSimpl]
XsimplSetup.protect [definition, in LibSepSimpl]
XsimplSetup.qimpl_antisym [lemma, in LibSepSimpl]
XsimplSetup.qimpl_trans [lemma, in LibSepSimpl]
XsimplSetup.qimpl_refl [lemma, in LibSepSimpl]
XsimplSetup.repr [definition, in LibSepSimpl]
XsimplSetup.repr_id [lemma, in LibSepSimpl]
XsimplSetup.repr_eq [lemma, in LibSepSimpl]
XsimplSetup.rew_heap_demo_with_evar [lemma, in LibSepSimpl]
XsimplSetup.star_post_empty [lemma, in LibSepSimpl]
XsimplSetup.xchange_demo_hforall_l [lemma, in LibSepSimpl]
XsimplSetup.xchange_demo_4 [lemma, in LibSepSimpl]
XsimplSetup.xchange_demo_2 [lemma, in LibSepSimpl]
XsimplSetup.xchange_demo_1 [lemma, in LibSepSimpl]
XsimplSetup.xchange_hidden [definition, in LibSepSimpl]
XsimplSetup.xchange_lemma [lemma, in LibSepSimpl]
XsimplSetup.xpull_demo [lemma, in LibSepSimpl]
XsimplSetup.xpull_protect [lemma, in LibSepSimpl]
XsimplSetup.Xsimpl [definition, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hfalse [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_4 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_3 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_2 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_1 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_0 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_4 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_3 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_2 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_1 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_iter [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_hstar_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_multiple_2 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_multiple_1 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_qwand_r [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_r [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_qwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hgc_multiple [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_htop_multiple [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_htop_both_sides [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_evar_2 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_evar_1 [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars_gc [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hint [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars_top [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_keep_order [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_pick_demo [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_demo_hints [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_pick_lemma [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_flip_acc_r [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_flip_acc_l [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_exit [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_exit_nogc [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_hforall [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_qwand_unit [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_qwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_hwand_hfalse [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_hwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_eq_repr [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_eq [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_hgc [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_htop [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_same [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_htop_drop [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hgc_drop [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_htop_replace_hgc [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hgc_or_htop [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_keep [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_id_unify [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_id [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hexists [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hpure [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hwand_same [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_r_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hstar_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hstar [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_hwand_reorder [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_keep_wand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_qwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_acc_other [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_acc_wand [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_hexists [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_hpure [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_l_hempty [lemma, in LibSepSimpl]
XsimplSetup.xsimpl_start [lemma, in LibSepSimpl]
XsimplSetup.Xsimpl_trans [lemma, in LibSepSimpl]
XsimplSetup.Xsimpl_trans_r [lemma, in LibSepSimpl]
XsimplSetup.Xsimpl_trans_l [lemma, in LibSepSimpl]
XsimplSetup.Xsimpl_hint_sind [definition, in LibSepSimpl]
XsimplSetup.Xsimpl_hint_rec [definition, in LibSepSimpl]
XsimplSetup.Xsimpl_hint_ind [definition, in LibSepSimpl]
XsimplSetup.Xsimpl_hint_rect [definition, in LibSepSimpl]
XsimplSetup.xsimpl_hint [constructor, in LibSepSimpl]
XsimplSetup.Xsimpl_hint [inductive, in LibSepSimpl]
_ ~> _ (heap_scope) [notation, in LibSepSimpl]
HSIMPL _ _ _ =====> _ _ _ (xsimpl_scope) [notation, in LibSepSimpl]
__XCHANGE_FAILED_TO_MATCH_PRECONDITION__ [notation, in LibSepSimpl]
XsimplTactic [module, in Himpl]
XsimplTactic.EntailmentProofs [module, in Himpl]
XsimplTactic.EntailmentProofs.himpl_example_3 [lemma, in Himpl]
XsimplTactic.EntailmentProofs.himpl_example_2 [lemma, in Himpl]
XsimplTactic.EntailmentProofs.himpl_example_1 [lemma, in Himpl]
XsimplTactic.EntailmentQuiz [module, in Himpl]
XsimplTactic.EntailmentQuizAnswers [module, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_12 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_11 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_10 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_8 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_7 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_6 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_4 [lemma, in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_1 [lemma, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_12 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_11 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_10 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_9 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_8 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_7 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_6 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_5 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_4 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_3 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_2 [axiom, in Himpl]
XsimplTactic.EntailmentQuiz.case_study_1 [axiom, in Himpl]
XsimplTactic.qimpl_example_1 [lemma, in Himpl]
XsimplTactic.xchange_lemma [lemma, in Himpl]
XsimplTactic.xchange_demo_inst [lemma, in Himpl]
XsimplTactic.xchange_demo_eq [lemma, in Himpl]
XsimplTactic.xchange_demo_base [lemma, in Himpl]
XsimplTactic.xpull_example_3 [lemma, in Himpl]
XsimplTactic.xpull_example_2 [lemma, in Himpl]
XsimplTactic.xpull_example_1 [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hints_evar [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hints [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_exists_solved_2 [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_exists_solved_1 [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists_unify_view [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists_unify [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists [lemma, in Himpl]
XsimplTactic.xsimpl_demo_rhs_hpure [lemma, in Himpl]
XsimplTactic.xsimpl_demo_cancel_all [lemma, in Himpl]
XsimplTactic.xsimpl_demo_cancel_many [lemma, in Himpl]
XsimplTactic.xsimpl_demo_cancel_one [lemma, in Himpl]
XsimplTactic.xsimpl_demo_lhs_several [lemma, in Himpl]
XsimplTactic.xsimpl_demo_lhs_hexists [lemma, in Himpl]
XsimplTactic.xsimpl_demo_lhs_hpure [lemma, in Himpl]
XsimplTactic.xsimpl_demo_lhs_hpure [lemma, in Himpl]
xstruct_lemma [lemma, in LibSepReference]
xstruct_lemma [lemma, in WPgen]
xtriple_lemma [lemma, in LibSepReference]
xval_lemma [lemma, in LibSepReference]
xval_lemma [lemma, in WPgen]
xwp_lemma_fixs [lemma, in LibSepReference]
xwp_lemma_funs [lemma, in LibSepReference]
xwp_lemma_fix [lemma, in LibSepReference]
xwp_lemma_fun [lemma, in LibSepReference]
xwp_lemma [lemma, in WPgen]
other
trm:delete (trm_scope) [notation, in LibSepReference]trm:`{ _ := _ ; _ := _ ; _ := _ } (trm_scope) [notation, in LibSepReference]
trm:`{ _ := _ ; _ := _ } (trm_scope) [notation, in LibSepReference]
trm:_ `. _ := _ (trm_scope) [notation, in LibSepReference]
trm:_ `. _ (trm_scope) [notation, in LibSepReference]
trm:_ > _ (trm_scope) [notation, in LibSepReference]
trm:_ >= _ (trm_scope) [notation, in LibSepReference]
trm:_ < _ (trm_scope) [notation, in LibSepReference]
trm:_ <= _ (trm_scope) [notation, in LibSepReference]
trm:_ <> _ (trm_scope) [notation, in LibSepReference]
trm:_ = _ (trm_scope) [notation, in LibSepReference]
trm:_ mod _ (trm_scope) [notation, in LibSepReference]
trm:_ / _ (trm_scope) [notation, in LibSepReference]
trm:_ * _ (trm_scope) [notation, in LibSepReference]
trm:_ - _ (trm_scope) [notation, in LibSepReference]
trm:'- _ (trm_scope) [notation, in LibSepReference]
trm:_ + _ (trm_scope) [notation, in LibSepReference]
trm:_ := _ (trm_scope) [notation, in LibSepReference]
trm:! _ (trm_scope) [notation, in LibSepReference]
trm:not (trm_scope) [notation, in LibSepReference]
trm:free (trm_scope) [notation, in LibSepReference]
trm:ref (trm_scope) [notation, in LibSepReference]
trm:() (trm_scope) [notation, in LibSepReference]
trm:fix_ _ _ _ .. _ => _ (trm_scope) [notation, in LibSepReference]
trm:fix_ _ _ => _ (trm_scope) [notation, in LibSepReference]
trm:fun_ _ .. _ => _ (trm_scope) [notation, in LibSepReference]
trm:fun_ _ => _ (trm_scope) [notation, in LibSepReference]
trm:let _ = _ in _ (trm_scope) [notation, in LibSepReference]
trm:_ ; _ (trm_scope) [notation, in LibSepReference]
trm:if _ then _ end (trm_scope) [notation, in LibSepReference]
trm:if _ then _ else _ (trm_scope) [notation, in LibSepReference]
trm:_ _ (trm_scope) [notation, in LibSepReference]
trm:_ (trm_scope) [notation, in LibSepReference]
trm:{ _ } (trm_scope) [notation, in LibSepReference]
trm:begin _ end (trm_scope) [notation, in LibSepReference]
trm:( _ ) (trm_scope) [notation, in LibSepReference]
trm:_ `. _ := _ (trm_scope_ext) [notation, in Records]
trm:_ `. _ (trm_scope_ext) [notation, in Records]
trm:fix _ _ _ .. _ => _ (val_scope) [notation, in LibSepReference]
trm:fix _ _ => _ (val_scope) [notation, in LibSepReference]
trm:fun _ _ .. _ => _ (val_scope) [notation, in LibSepReference]
trm:fun _ => _ (val_scope) [notation, in LibSepReference]
trm:let rec _ _ _ .. _ = _ in _ (val_scope) [notation, in LibSepReference]
trm:let rec _ _ = _ in _ (val_scope) [notation, in LibSepReference]
trm:let _ _ .. _ = _ in _ (val_scope) [notation, in LibSepReference]
trm:let _ _ = _ in _ (val_scope) [notation, in LibSepReference]
trm:`{ _ := _ ; _ := _ } [notation, in Records]
wp:Fix _ _ => _ (wp_scope) [notation, in LibSepReference]
wp:Fun _ => _ (wp_scope) [notation, in LibSepReference]
wp:If_ _ Then _ Else _ (wp_scope) [notation, in LibSepReference]
wp:App _ _ .. _ (wp_scope) [notation, in LibSepReference]
wp:Seq _ ; _ (wp_scope) [notation, in LibSepReference]
wp:Let _ := _ in _ (wp_scope) [notation, in LibSepReference]
wp:Val _ (wp_scope) [notation, in LibSepReference]
wp:Fail (wp_scope) [notation, in LibSepReference]
wp:_ (wp_scope) [notation, in LibSepReference]
wp:{ _ } (wp_scope) [notation, in LibSepReference]
wp:( _ ) (wp_scope) [notation, in LibSepReference]
wp:` _ (wp_scope) [notation, in LibSepReference]
_ \+ _ (fmap_scope) [notation, in LibSepFmap]
\GC (hgc_scope) [notation, in Affine]
_ ~~~> _ (hprop_scope) [notation, in LibSepReference]
funloc _ => _ (hprop_scope) [notation, in LibSepReference]
_ ===> _ (hprop_scope) [notation, in LibSepMinimal]
_ ==> _ (hprop_scope) [notation, in LibSepMinimal]
\forall _ .. _ , _ (hprop_scope) [notation, in LibSepMinimal]
\exists _ .. _ , _ (hprop_scope) [notation, in LibSepMinimal]
_ \*+ _ (hprop_scope) [notation, in LibSepMinimal]
_ \* _ (hprop_scope) [notation, in LibSepMinimal]
_ ~~> _ (hprop_scope) [notation, in LibSepMinimal]
\[ _ ] (hprop_scope) [notation, in LibSepMinimal]
\[] (hprop_scope) [notation, in LibSepMinimal]
<{ _ }> (trm_scope) [notation, in LibSepReference]
`{ _ := _ ; _ := _ ; _ := _ } (val_scope) [notation, in LibSepReference]
`{ _ := _ ; _ := _ } (val_scope) [notation, in LibSepReference]
`{ _ := _ } (val_scope) [notation, in LibSepReference]
`{ _ := _ ; _ := _ ; _ := _ } (val_scope) [notation, in LibSepReference]
`{ _ := _ ; _ := _ } (val_scope) [notation, in LibSepReference]
`{ _ := _ } (val_scope) [notation, in LibSepReference]
() (val_scope) [notation, in LibSepReference]
` _ (wpgen_scope) [notation, in WPgen]
App _ _ _ (wpgen_scope) [notation, in WPgen]
App _ _ (wpgen_scope) [notation, in WPgen]
Fail (wpgen_scope) [notation, in WPgen]
If_ _ Then _ Else _ (wpgen_scope) [notation, in WPgen]
Let _ := _ in _ (wpgen_scope) [notation, in WPgen]
Val _ (wpgen_scope) [notation, in WPgen]
<[ _ ]> (wp_scope) [notation, in LibSepReference]
` _ (wp_scope) [notation, in LibSepReference]
PRE _ CODE _ POST _ (wp_scope) [notation, in LibSepReference]
_ \u _ [notation, in LibSepReference]
_ \*+ _ [notation, in Hprop]
_ \* _ [notation, in Hprop]
_ ~~> _ [notation, in Hprop]
_ \u _ [notation, in Hprop]
_ ~~~> _ [notation, in Records]
_ `. _ ~~> _ [notation, in Records]
_ ===> _ [notation, in Himpl]
_ ==> _ [notation, in Himpl]
funloc _ => _ [notation, in Basic]
Seq _ ; _ [notation, in WPgen]
\exists _ .. _ , _ [notation, in Hprop]
\[ _ ] [notation, in Hprop]
\[] [notation, in Hprop]
`{ _ := _ ; _ := _ ; _ := _ } [notation, in Records]
`{ _ := _ ; _ := _ } [notation, in Records]
`{ _ := _ } [notation, in Records]
`{ _ := _ ; _ := _ ; _ := _ } [notation, in Records]
`{ _ := _ ; _ := _ } [notation, in Records]
`{ _ := _ } [notation, in Records]
Notation Index
H
\forall _ .. _ , _ [in Wand]_ \−∗ _ [in Wand]
N
\# _ _ _ (fmap_scope) [in LibSepFmap]\# _ _ (fmap_scope) [in LibSepFmap]
trm:'z3 (trm_scope) [in LibSepVar]
trm:'y3 (trm_scope) [in LibSepVar]
trm:'x3 (trm_scope) [in LibSepVar]
trm:'w3 (trm_scope) [in LibSepVar]
trm:'v3 (trm_scope) [in LibSepVar]
trm:'u3 (trm_scope) [in LibSepVar]
trm:'t3 (trm_scope) [in LibSepVar]
trm:'s3 (trm_scope) [in LibSepVar]
trm:'r3 (trm_scope) [in LibSepVar]
trm:'q3 (trm_scope) [in LibSepVar]
trm:'p3 (trm_scope) [in LibSepVar]
trm:'o3 (trm_scope) [in LibSepVar]
trm:'n3 (trm_scope) [in LibSepVar]
trm:'m3 (trm_scope) [in LibSepVar]
trm:'l3 (trm_scope) [in LibSepVar]
trm:'k3 (trm_scope) [in LibSepVar]
trm:'j3 (trm_scope) [in LibSepVar]
trm:'i3 (trm_scope) [in LibSepVar]
trm:'h3 (trm_scope) [in LibSepVar]
trm:'g3 (trm_scope) [in LibSepVar]
trm:'f3 (trm_scope) [in LibSepVar]
trm:'e3 (trm_scope) [in LibSepVar]
trm:'d3 (trm_scope) [in LibSepVar]
trm:'c3 (trm_scope) [in LibSepVar]
trm:'b3 (trm_scope) [in LibSepVar]
trm:'a3 (trm_scope) [in LibSepVar]
trm:'z2 (trm_scope) [in LibSepVar]
trm:'y2 (trm_scope) [in LibSepVar]
trm:'x2 (trm_scope) [in LibSepVar]
trm:'w2 (trm_scope) [in LibSepVar]
trm:'v2 (trm_scope) [in LibSepVar]
trm:'u2 (trm_scope) [in LibSepVar]
trm:'t2 (trm_scope) [in LibSepVar]
trm:'s2 (trm_scope) [in LibSepVar]
trm:'r2 (trm_scope) [in LibSepVar]
trm:'q2 (trm_scope) [in LibSepVar]
trm:'p2 (trm_scope) [in LibSepVar]
trm:'o2 (trm_scope) [in LibSepVar]
trm:'n2 (trm_scope) [in LibSepVar]
trm:'m2 (trm_scope) [in LibSepVar]
trm:'l2 (trm_scope) [in LibSepVar]
trm:'k2 (trm_scope) [in LibSepVar]
trm:'j2 (trm_scope) [in LibSepVar]
trm:'i2 (trm_scope) [in LibSepVar]
trm:'h2 (trm_scope) [in LibSepVar]
trm:'g2 (trm_scope) [in LibSepVar]
trm:'f2 (trm_scope) [in LibSepVar]
trm:'e2 (trm_scope) [in LibSepVar]
trm:'d2 (trm_scope) [in LibSepVar]
trm:'c2 (trm_scope) [in LibSepVar]
trm:'b2 (trm_scope) [in LibSepVar]
trm:'a2 (trm_scope) [in LibSepVar]
trm:'z1 (trm_scope) [in LibSepVar]
trm:'y1 (trm_scope) [in LibSepVar]
trm:'x1 (trm_scope) [in LibSepVar]
trm:'w1 (trm_scope) [in LibSepVar]
trm:'v1 (trm_scope) [in LibSepVar]
trm:'u1 (trm_scope) [in LibSepVar]
trm:'t1 (trm_scope) [in LibSepVar]
trm:'s1 (trm_scope) [in LibSepVar]
trm:'r1 (trm_scope) [in LibSepVar]
trm:'q1 (trm_scope) [in LibSepVar]
trm:'p1 (trm_scope) [in LibSepVar]
trm:'o1 (trm_scope) [in LibSepVar]
trm:'n1 (trm_scope) [in LibSepVar]
trm:'m1 (trm_scope) [in LibSepVar]
trm:'l1 (trm_scope) [in LibSepVar]
trm:'k1 (trm_scope) [in LibSepVar]
trm:'j1 (trm_scope) [in LibSepVar]
trm:'i1 (trm_scope) [in LibSepVar]
trm:'h1 (trm_scope) [in LibSepVar]
trm:'g1 (trm_scope) [in LibSepVar]
trm:'f1 (trm_scope) [in LibSepVar]
trm:'e1 (trm_scope) [in LibSepVar]
trm:'d1 (trm_scope) [in LibSepVar]
trm:'c1 (trm_scope) [in LibSepVar]
trm:'b1 (trm_scope) [in LibSepVar]
trm:'a1 (trm_scope) [in LibSepVar]
trm:'z (trm_scope) [in LibSepVar]
trm:'y (trm_scope) [in LibSepVar]
trm:'x (trm_scope) [in LibSepVar]
trm:'w (trm_scope) [in LibSepVar]
trm:'v (trm_scope) [in LibSepVar]
trm:'u (trm_scope) [in LibSepVar]
trm:'t (trm_scope) [in LibSepVar]
trm:'s (trm_scope) [in LibSepVar]
trm:'r (trm_scope) [in LibSepVar]
trm:'q (trm_scope) [in LibSepVar]
trm:'p (trm_scope) [in LibSepVar]
trm:'o (trm_scope) [in LibSepVar]
trm:'n (trm_scope) [in LibSepVar]
trm:'m (trm_scope) [in LibSepVar]
trm:'l (trm_scope) [in LibSepVar]
trm:'k (trm_scope) [in LibSepVar]
trm:'j (trm_scope) [in LibSepVar]
trm:'i (trm_scope) [in LibSepVar]
trm:'h (trm_scope) [in LibSepVar]
trm:'g (trm_scope) [in LibSepVar]
trm:'f (trm_scope) [in LibSepVar]
trm:'e (trm_scope) [in LibSepVar]
trm:'d (trm_scope) [in LibSepVar]
trm:'c (trm_scope) [in LibSepVar]
trm:'b (trm_scope) [in LibSepVar]
trm:'a (trm_scope) [in LibSepVar]
Q
_ \−−∗ _ [in Wand]R
trm:`{ _ := _ ; _ := _ } (trm_scope_ext) [in Records]trm:_ `. _ := _ [in Records]
trm:_ `. _ [in Records]
S
\GC (hprop_scope) [in LibSepReference]_ \−−∗ _ (hprop_scope) [in LibSepReference]
_ \−∗ _ (hprop_scope) [in LibSepReference]
_ \*+ _ (hprop_scope) [in LibSepReference]
\Top (hprop_scope) [in LibSepReference]
\[ _ ] (hprop_scope) [in LibSepReference]
\forall _ .. _ , _ (hprop_scope) [in LibSepReference]
\exists _ .. _ , _ (hprop_scope) [in LibSepReference]
_ \* _ (hprop_scope) [in LibSepReference]
_ ~~> _ (hprop_scope) [in LibSepReference]
\[] (hprop_scope) [in LibSepReference]
_ ===> _ (hprop_scope) [in LibSepReference]
_ ==> _ (hprop_scope) [in LibSepReference]
W
Fix _ _ := _ [in WPgen]Fun _ := _ [in WPgen]
X
\forall _ .. _ , _ (heap_scope) [in LibSepSimpl]\exists _ .. _ , _ (heap_scope) [in LibSepSimpl]
_ \−−∗ _ (heap_scope) [in LibSepSimpl]
_ \−∗ _ (heap_scope) [in LibSepSimpl]
_ \*+ _ (heap_scope) [in LibSepSimpl]
_ \* _ (heap_scope) [in LibSepSimpl]
\GC (heap_scope) [in LibSepSimpl]
\Top (heap_scope) [in LibSepSimpl]
\[ _ ] (heap_scope) [in LibSepSimpl]
\[] (heap_scope) [in LibSepSimpl]
_ ===> _ (heap_scope) [in LibSepSimpl]
_ ==> _ (heap_scope) [in LibSepSimpl]
_ ~> _ (heap_scope) [in LibSepSimpl]
HSIMPL _ _ _ =====> _ _ _ (xsimpl_scope) [in LibSepSimpl]
__XCHANGE_FAILED_TO_MATCH_PRECONDITION__ [in LibSepSimpl]
other
trm:delete (trm_scope) [in LibSepReference]trm:`{ _ := _ ; _ := _ ; _ := _ } (trm_scope) [in LibSepReference]
trm:`{ _ := _ ; _ := _ } (trm_scope) [in LibSepReference]
trm:_ `. _ := _ (trm_scope) [in LibSepReference]
trm:_ `. _ (trm_scope) [in LibSepReference]
trm:_ > _ (trm_scope) [in LibSepReference]
trm:_ >= _ (trm_scope) [in LibSepReference]
trm:_ < _ (trm_scope) [in LibSepReference]
trm:_ <= _ (trm_scope) [in LibSepReference]
trm:_ <> _ (trm_scope) [in LibSepReference]
trm:_ = _ (trm_scope) [in LibSepReference]
trm:_ mod _ (trm_scope) [in LibSepReference]
trm:_ / _ (trm_scope) [in LibSepReference]
trm:_ * _ (trm_scope) [in LibSepReference]
trm:_ - _ (trm_scope) [in LibSepReference]
trm:'- _ (trm_scope) [in LibSepReference]
trm:_ + _ (trm_scope) [in LibSepReference]
trm:_ := _ (trm_scope) [in LibSepReference]
trm:! _ (trm_scope) [in LibSepReference]
trm:not (trm_scope) [in LibSepReference]
trm:free (trm_scope) [in LibSepReference]
trm:ref (trm_scope) [in LibSepReference]
trm:() (trm_scope) [in LibSepReference]
trm:fix_ _ _ _ .. _ => _ (trm_scope) [in LibSepReference]
trm:fix_ _ _ => _ (trm_scope) [in LibSepReference]
trm:fun_ _ .. _ => _ (trm_scope) [in LibSepReference]
trm:fun_ _ => _ (trm_scope) [in LibSepReference]
trm:let _ = _ in _ (trm_scope) [in LibSepReference]
trm:_ ; _ (trm_scope) [in LibSepReference]
trm:if _ then _ end (trm_scope) [in LibSepReference]
trm:if _ then _ else _ (trm_scope) [in LibSepReference]
trm:_ _ (trm_scope) [in LibSepReference]
trm:_ (trm_scope) [in LibSepReference]
trm:{ _ } (trm_scope) [in LibSepReference]
trm:begin _ end (trm_scope) [in LibSepReference]
trm:( _ ) (trm_scope) [in LibSepReference]
trm:_ `. _ := _ (trm_scope_ext) [in Records]
trm:_ `. _ (trm_scope_ext) [in Records]
trm:fix _ _ _ .. _ => _ (val_scope) [in LibSepReference]
trm:fix _ _ => _ (val_scope) [in LibSepReference]
trm:fun _ _ .. _ => _ (val_scope) [in LibSepReference]
trm:fun _ => _ (val_scope) [in LibSepReference]
trm:let rec _ _ _ .. _ = _ in _ (val_scope) [in LibSepReference]
trm:let rec _ _ = _ in _ (val_scope) [in LibSepReference]
trm:let _ _ .. _ = _ in _ (val_scope) [in LibSepReference]
trm:let _ _ = _ in _ (val_scope) [in LibSepReference]
trm:`{ _ := _ ; _ := _ } [in Records]
wp:Fix _ _ => _ (wp_scope) [in LibSepReference]
wp:Fun _ => _ (wp_scope) [in LibSepReference]
wp:If_ _ Then _ Else _ (wp_scope) [in LibSepReference]
wp:App _ _ .. _ (wp_scope) [in LibSepReference]
wp:Seq _ ; _ (wp_scope) [in LibSepReference]
wp:Let _ := _ in _ (wp_scope) [in LibSepReference]
wp:Val _ (wp_scope) [in LibSepReference]
wp:Fail (wp_scope) [in LibSepReference]
wp:_ (wp_scope) [in LibSepReference]
wp:{ _ } (wp_scope) [in LibSepReference]
wp:( _ ) (wp_scope) [in LibSepReference]
wp:` _ (wp_scope) [in LibSepReference]
_ \+ _ (fmap_scope) [in LibSepFmap]
\GC (hgc_scope) [in Affine]
_ ~~~> _ (hprop_scope) [in LibSepReference]
funloc _ => _ (hprop_scope) [in LibSepReference]
_ ===> _ (hprop_scope) [in LibSepMinimal]
_ ==> _ (hprop_scope) [in LibSepMinimal]
\forall _ .. _ , _ (hprop_scope) [in LibSepMinimal]
\exists _ .. _ , _ (hprop_scope) [in LibSepMinimal]
_ \*+ _ (hprop_scope) [in LibSepMinimal]
_ \* _ (hprop_scope) [in LibSepMinimal]
_ ~~> _ (hprop_scope) [in LibSepMinimal]
\[ _ ] (hprop_scope) [in LibSepMinimal]
\[] (hprop_scope) [in LibSepMinimal]
<{ _ }> (trm_scope) [in LibSepReference]
`{ _ := _ ; _ := _ ; _ := _ } (val_scope) [in LibSepReference]
`{ _ := _ ; _ := _ } (val_scope) [in LibSepReference]
`{ _ := _ } (val_scope) [in LibSepReference]
`{ _ := _ ; _ := _ ; _ := _ } (val_scope) [in LibSepReference]
`{ _ := _ ; _ := _ } (val_scope) [in LibSepReference]
`{ _ := _ } (val_scope) [in LibSepReference]
() (val_scope) [in LibSepReference]
` _ (wpgen_scope) [in WPgen]
App _ _ _ (wpgen_scope) [in WPgen]
App _ _ (wpgen_scope) [in WPgen]
Fail (wpgen_scope) [in WPgen]
If_ _ Then _ Else _ (wpgen_scope) [in WPgen]
Let _ := _ in _ (wpgen_scope) [in WPgen]
Val _ (wpgen_scope) [in WPgen]
<[ _ ]> (wp_scope) [in LibSepReference]
` _ (wp_scope) [in LibSepReference]
PRE _ CODE _ POST _ (wp_scope) [in LibSepReference]
_ \u _ [in LibSepReference]
_ \*+ _ [in Hprop]
_ \* _ [in Hprop]
_ ~~> _ [in Hprop]
_ \u _ [in Hprop]
_ ~~~> _ [in Records]
_ `. _ ~~> _ [in Records]
_ ===> _ [in Himpl]
_ ==> _ [in Himpl]
funloc _ => _ [in Basic]
Seq _ ; _ [in WPgen]
\exists _ .. _ , _ [in Hprop]
\[ _ ] [in Hprop]
\[] [in Hprop]
`{ _ := _ ; _ := _ ; _ := _ } [in Records]
`{ _ := _ ; _ := _ } [in Records]
`{ _ := _ } [in Records]
`{ _ := _ ; _ := _ ; _ := _ } [in Records]
`{ _ := _ ; _ := _ } [in Records]
`{ _ := _ } [in Records]
Module Index
A
AlternativeExistentialRule [in Triples]B
BakedInFrame [in Triples]D
DefinitionsForVariables [in LibSepVar]DemoPrograms [in LibSepReference]
DemoPrograms.Def_myfun [in LibSepReference]
DemoPrograms.Def_myrec [in LibSepReference]
DemoPrograms.Def_mysucc [in LibSepReference]
DemoPrograms.Def_decr [in LibSepReference]
DemoPrograms.Def_incr [in LibSepReference]
DisjointHints [in LibSepFmap]
DivSpec [in Rules]
E
EntailmentRulesProofs [in Himpl]ExampleLocalFunWpgen [in WPgen]
ExamplePrograms [in Rules]
ExamplePrograms2 [in Rules]
Extensionality [in Hprop]
F
Facto [in Basic]Fmap [in LibSepReference]
Fmap [in LibSepMinimal]
FromPreToPostGC [in Affine]
FullyAffineLogic [in Affine]
FullyLinearLogic [in Affine]
H
HaffineQuantifiers [in Affine]Hand [in Wand]
Hforall [in Wand]
Hor [in Wand]
Hor.HorExample [in Wand]
HpropProofs [in Hprop]
HS [in LibSepReference]
Hwand [in Wand]
HwandEquiv [in Wand]
HwandFalse [in Wand]
I
IsubstProp [in WPsound]L
LetFrame [in Rules]M
MatchStyle [in Rules]MkstructProp [in WPgen]
MotivatingExample [in Affine]
MotivatingExampleSolved [in Affine]
N
NewTriples [in Affine]NewTriples.MotivatingExampleWithUpdatedXwp [in Affine]
NotationForFmapDisjoint [in LibSepFmap]
NotationForVariables [in LibSepVar]
P
Pivot [in Arrays]Preview [in Affine]
ProgramSyntax [in LibSepReference]
ProgramSyntax.Vars [in LibSepReference]
ProofsSameSemantics [in Rules]
ProofsWithAdvancedXtactics [in WPgen]
ProofsWithStructuralXtactics [in WPgen]
ProofsWithXlemmas [in WPgen]
ProofsWithXtactics [in WPgen]
Q
QuickSort [in Arrays]Qwand [in Wand]
QwandEquiv [in Wand]
R
RamifiedFrame [in Wand]Realization [in Records]
Realization [in Arrays]
S
SepSimplArgs [in LibSepReference]SizedStack [in Repr]
StructuralRules [in Triples]
SummaryHprop [in Wand]
SummaryHprop.ReaminingOperatorsDerived [in Wand]
SummaryHprop.ReaminingOperatorsDirect [in Wand]
Syntax [in Triples]
T
TexanTriples [in WPsem]W
WpFromTriple [in WPsem]WpFromTriple2 [in WPsem]
WpgenExec1 [in WPgen]
WpgenExec2 [in WPgen]
WPgenRec [in WPgen]
WPgenRec.ExampleLocalFunWpgenRec [in WPgen]
WPgenWithNotation [in WPgen]
X
Xaffine [in Affine]XGC [in Affine]
XsimplDemo [in Wand]
XsimplExtended [in Affine]
XsimplParams [in LibSepSimpl]
XsimplSetup [in LibSepSimpl]
XsimplTactic [in Himpl]
XsimplTactic.EntailmentProofs [in Himpl]
XsimplTactic.EntailmentQuiz [in Himpl]
XsimplTactic.EntailmentQuizAnswers [in Himpl]
Variable Index
F
FmapFresh.B [in LibSepFmap]FmapProp.A [in LibSepFmap]
FmapProp.B [in LibSepFmap]
M
MapOps.A [in LibSepFmap]MapOps.B [in LibSepFmap]
S
StateEq.A [in LibSepFmap]StateEq.B [in LibSepFmap]
Library Index
A
AffineArrays
B
BasicBib
H
HimplHprop
L
LibSepFmapLibSepMinimal
LibSepReference
LibSepSimpl
LibSepVar
P
PostscriptPreface
R
RecordsRepr
Rules
T
TriplesW
WandWPgen
WPsem
WPsound
Lemma Index
A
agree_union_r_inv [in LibSepFmap]agree_union_l_inv [in LibSepFmap]
agree_union_rr_inv_agree [in LibSepFmap]
agree_union_lr_inv_agree_agree [in LibSepFmap]
agree_union_rl_inv [in LibSepFmap]
agree_union_ll_inv [in LibSepFmap]
agree_union_lr [in LibSepFmap]
agree_union_r [in LibSepFmap]
agree_union_l [in LibSepFmap]
agree_empty_r [in LibSepFmap]
agree_empty_l [in LibSepFmap]
agree_of_disjoint [in LibSepFmap]
agree_sym [in LibSepFmap]
agree_refl [in LibSepFmap]
AlternativeExistentialRule.triple_hexists_of_triple_hexists2 [in Triples]
AlternativeExistentialRule.triple_hexists2 [in Triples]
B
BakedInFrame.btriple_iff_btriple_lowlevel [in Triples]BakedInFrame.btriple_frame [in Triples]
BakedInFrame.hoare_conseq [in Triples]
C
conseq_fresh [in LibSepFmap]conseq_cons' [in LibSepFmap]
conseq_cons [in LibSepFmap]
conseq_nil [in LibSepFmap]
ctx_disjoint_equiv_app [in LibSepReference]
ctx_disjoint_rem [in LibSepReference]
ctx_equiv_rem [in LibSepReference]
D
DemoPrograms.Def_myrec.triple_myrec [in LibSepReference]DemoPrograms.triple_project_32_rec [in LibSepReference]
DemoPrograms.triple_project_32 [in LibSepReference]
DemoPrograms.triple_myfun [in LibSepReference]
DemoPrograms.triple_mysucc [in LibSepReference]
DemoPrograms.triple_decr [in LibSepReference]
DemoPrograms.triple_incr' [in LibSepReference]
DemoPrograms.triple_incr [in LibSepReference]
demo_hrecord_intro_elim [in Records]
disjoint_single_conseq [in LibSepFmap]
disjoint_demo [in LibSepFmap]
disjoint_remove_l [in LibSepFmap]
disjoint_update_not_r [in LibSepFmap]
disjoint_update_l [in LibSepFmap]
disjoint_single_set [in LibSepFmap]
disjoint_3_unfold [in LibSepFmap]
disjoint_single_single_same_inv [in LibSepFmap]
disjoint_single_single [in LibSepFmap]
disjoint_union_eq_l [in LibSepFmap]
disjoint_union_eq_r [in LibSepFmap]
disjoint_empty_r [in LibSepFmap]
disjoint_empty_l [in LibSepFmap]
disjoint_comm [in LibSepFmap]
disjoint_sym [in LibSepFmap]
disjoint_single_of_not_indom [in LibSepFmap]
disjoint_inv_not_indom_both [in LibSepFmap]
disjoint_of_not_indom_both [in LibSepFmap]
disjoint_eq' [in LibSepFmap]
disjoint_eq [in LibSepFmap]
DivSpec.triple_div_from_triple_div' [in Rules]
DivSpec.triple_div'_from_triple_div [in Rules]
E
EntailmentRulesProofs.himpl_frame_lr [in Himpl]EntailmentRulesProofs.himpl_frame_r [in Himpl]
EntailmentRulesProofs.himpl_frame_l [in Himpl]
eq_inv_fmap_data_eq [in LibSepFmap]
eval_frame [in Triples]
eval_conseq [in Triples]
eval_like_trm_apps_fixs [in LibSepReference]
eval_like_trm_apps_funs [in LibSepReference]
eval_like_app_val_funs_one [in LibSepReference]
eval_like_app_val_funs_cons [in LibSepReference]
eval_like_trm_funs [in LibSepReference]
eval_frame [in LibSepReference]
eval_conseq [in LibSepReference]
eval_app_arg2' [in LibSepReference]
eval_app_arg1' [in LibSepReference]
eval_rand [in LibSepReference]
eval_div [in LibSepReference]
eval_add [in LibSepReference]
eval_val_minimal [in LibSepReference]
eval_frame [in LibSepMinimal]
eval_conseq [in LibSepMinimal]
ExampleLocalFunWpgen.triple_succtwice_using_xfun [in WPgen]
ExampleLocalFunWpgen.triple_succtwice_using_xletval [in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_with_xfun [in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_with_assert [in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xletva_and_xapp_fun [in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xletval [in WPgen]
ExampleLocalFunWpgen.triple_incrtwice_using_xval [in WPgen]
ExampleLocalFunWpgen.xappfun_lemma [in WPgen]
ExampleLocalFunWpgen.xfun_lemma [in WPgen]
ExampleLocalFunWpgen.xletval_lemma [in WPgen]
ExamplePrograms.incr_eq_incr' [in Rules]
ExamplePrograms.triple_succ_using_incr [in Rules]
ExamplePrograms.triple_incr [in Rules]
ExamplePrograms2.triple_factorec [in Rules]
exists_not_empty [in LibSepFmap]
exists_smallest_fresh [in LibSepFmap]
exists_fresh [in LibSepFmap]
Extensionality.predicate_extensionality_derived [in Hprop]
F
Facto.facto_succ [in Basic]fmap_eq_demo [in LibSepFmap]
fmap_extens [in LibSepFmap]
FromPreToPostGC.triple_hgc_post_from_hgc_pre [in Affine]
FullyAffineLogic.haffine_equiv [in Affine]
FullyAffineLogic.heap_affine_union [in Affine]
FullyAffineLogic.heap_affine_empty [in Affine]
FullyAffineLogic.hgc_eq_htop [in Affine]
FullyLinearLogic.haffine_equiv [in Affine]
FullyLinearLogic.heap_affine_union [in Affine]
FullyLinearLogic.heap_affine_empty [in Affine]
FullyLinearLogic.hgc_eq_hempty [in Affine]
H
HaffineQuantifiers.haffine_hforall [in Affine]HaffineQuantifiers.haffine_hexists [in Affine]
haffine_hgc [in LibSepReference]
haffine_hstar_hpure [in LibSepReference]
haffine_hforall [in LibSepReference]
haffine_hexists [in LibSepReference]
haffine_hstar [in LibSepReference]
haffine_hpure [in LibSepReference]
haffine_hempty [in LibSepReference]
haffine_hgc [in Affine]
haffine_hstar_hpure_l [in Affine]
haffine_hforall [in Affine]
haffine_hforall' [in Affine]
haffine_hexists [in Affine]
haffine_hstar [in Affine]
haffine_hpure [in Affine]
haffine_hempty [in Affine]
hand_sym [in LibSepReference]
Hand.hand_comm [in Wand]
Hand.hand_eq_hand' [in Wand]
Hand.himpl_hand_r [in Wand]
Hand.himpl_hand_l_l [in Wand]
Hand.himpl_hand_l_r [in Wand]
hempty_eq_hpure_true [in Hprop]
hempty_inv [in Hprop]
hempty_intro [in Hprop]
hempty_himpl_hgc [in Affine]
hexists_inv [in Hprop]
hexists_intro [in Hprop]
hexists_named_eq [in Himpl]
Hforall.hforall_specialize [in Wand]
Hforall.hforall_inv [in Wand]
Hforall.hforall_intro [in Wand]
Hforall.himpl_hforall_l [in Wand]
Hforall.himpl_hforall_r [in Wand]
Hforall.triple_hforall [in Wand]
hgc_eq_heap_affine [in Affine]
hgc_inv [in Affine]
hgc_intro [in Affine]
himpl_hand_r [in LibSepReference]
himpl_hand_l_l [in LibSepReference]
himpl_hand_l_r [in LibSepReference]
himpl_hor_l [in LibSepReference]
himpl_hor_r_r [in LibSepReference]
himpl_hor_r_l [in LibSepReference]
himpl_wpgen_wp [in LibSepReference]
himpl_hforall [in LibSepMinimal]
himpl_hforall_l [in LibSepMinimal]
himpl_hforall_r [in LibSepMinimal]
himpl_hexists [in LibSepMinimal]
himpl_hexists_r [in LibSepMinimal]
himpl_hexists_l [in LibSepMinimal]
himpl_hstar_hpure_l [in LibSepMinimal]
himpl_hstar_hpure_r [in LibSepMinimal]
himpl_frame_r [in LibSepMinimal]
himpl_frame_l [in LibSepMinimal]
himpl_antisym [in LibSepMinimal]
himpl_trans [in LibSepMinimal]
himpl_refl [in LibSepMinimal]
himpl_hexists_l [in Himpl]
himpl_hexists_r [in Himpl]
himpl_hstar_hpure_l [in Himpl]
himpl_hstar_hpure_r [in Himpl]
himpl_antisym [in Himpl]
himpl_trans [in Himpl]
himpl_refl [in Himpl]
himpl_hgc_absorb_r [in Affine]
himpl_hgc_r [in Affine]
hor_sym [in LibSepReference]
Hor.himpl_hor_l [in Wand]
Hor.himpl_hor_r_r_trans [in Wand]
Hor.himpl_hor_r_l_trans [in Wand]
Hor.himpl_hor_r_r [in Wand]
Hor.himpl_hor_r_l [in Wand]
Hor.HorExample.MList_using_hor [in Wand]
Hor.hor_comm [in Wand]
Hor.hor_eq_hor' [in Wand]
Hor.if_neg [in Wand]
HpropProofs.hprop_op_comm [in Hprop]
HpropProofs.hstar_hpure_l [in Hprop]
HpropProofs.hstar_comm_assoc [in Hprop]
HpropProofs.hstar_hempty_r [in Hprop]
HpropProofs.hstar_assoc [in Hprop]
HpropProofs.hstar_comm [in Hprop]
HpropProofs.hstar_hempty_l [in Hprop]
HpropProofs.hstar_hexists [in Hprop]
hprop_eq [in Hprop]
hpure_eq_hexists_proof [in Hprop]
hpure_inv [in Hprop]
hpure_intro [in Hprop]
hrecord_elim [in Records]
hseg_last_r [in Arrays]
hseg_app_r [in Arrays]
hseg_cons_r [in Arrays]
hseg_last [in Arrays]
hseg_cons [in Arrays]
hsingle_inv [in Hprop]
hsingle_intro [in Hprop]
hstar_inv [in Hprop]
hstar_intro [in Hprop]
hstar_hsingle_same_loc [in LibSepMinimal]
hstar_hpure_l [in LibSepMinimal]
hstar_hempty_r [in LibSepMinimal]
hstar_hforall [in LibSepMinimal]
hstar_hexists [in LibSepMinimal]
hstar_hempty_l [in LibSepMinimal]
hstar_assoc [in LibSepMinimal]
hstar_comm [in LibSepMinimal]
hstar_intro [in LibSepMinimal]
hstar_hsingle_same_loc [in Himpl]
hstar_hgc_hgc [in Affine]
HwandEquiv.hwand_characterization_3_eq_4 [in Wand]
HwandEquiv.hwand_characterization_2_eq_3 [in Wand]
HwandEquiv.hwand_characterization_1_eq_2 [in Wand]
HwandFalse.himpl_hwand_same_hempty_counterexample [in Wand]
HwandFalse.not_himpl_hwand_r_inv_reciprocal [in Wand]
Hwand.himpl_hwand_hstar_same_r [in Wand]
Hwand.himpl_hwand_hpure_lr [in Wand]
Hwand.himpl_hwand_hpure_r [in Wand]
Hwand.himpl_hempty_hwand_same [in Wand]
Hwand.himpl_hwand_r_inv [in Wand]
Hwand.himpl_hwand_r [in Wand]
Hwand.hstar_hwand [in Wand]
Hwand.hwand_inv [in Wand]
Hwand.hwand_frame [in Wand]
Hwand.hwand_cancel_part [in Wand]
Hwand.hwand_curry_eq [in Wand]
Hwand.hwand_hpure_l [in Wand]
Hwand.hwand_hempty_l [in Wand]
Hwand.hwand_trans_elim [in Wand]
Hwand.hwand_himpl [in Wand]
Hwand.hwand_cancel [in Wand]
Hwand.hwand_equiv [in Wand]
I
indom_remove_eq [in LibSepFmap]indom_update_eq [in LibSepFmap]
indom_union_r [in LibSepFmap]
indom_union_l [in LibSepFmap]
indom_union_eq [in LibSepFmap]
indom_single [in LibSepFmap]
indom_single_eq [in LibSepFmap]
injective_nat_to_var [in LibSepVar]
IsubstProp.ctx_disjoint_rem [in WPsound]
IsubstProp.ctx_equiv_rem [in WPsound]
IsubstProp.isubst_rem_2 [in WPsound]
IsubstProp.isubst_rem [in WPsound]
IsubstProp.isubst_app_swap [in WPsound]
IsubstProp.isubst_app [in WPsound]
IsubstProp.isubst_ctx_equiv [in WPsound]
IsubstProp.isubst_nil [in WPsound]
IsubstProp.lookup_app [in WPsound]
IsubstProp.lookup_rem [in WPsound]
IsubstProp.rem_app [in WPsound]
IsubstProp.subst_eq_isubst_one [in WPsound]
isubst_rem_2 [in LibSepReference]
isubst_rem [in LibSepReference]
isubst_app_swap [in LibSepReference]
isubst_cons [in LibSepReference]
isubst_app [in LibSepReference]
isubst_ctx_equiv [in LibSepReference]
isubst_nil [in LibSepReference]
L
length_var_seq [in LibSepVar]LetFrame.triple_let_frame [in Rules]
loc_fresh_nat [in LibSepFmap]
loc_fresh_nat_ge [in LibSepFmap]
loc_fresh_ind [in LibSepFmap]
lookup_rem [in LibSepReference]
lookup_app [in LibSepReference]
M
make_eq [in LibSepFmap]map_union_finite [in LibSepFmap]
map_union_comm [in LibSepFmap]
map_disjoint_sym [in LibSepFmap]
map_disjoint_eq [in LibSepFmap]
max_r [in Basic]
max_l [in Basic]
mkstruct_sound [in LibSepReference]
mkstruct_wp [in LibSepReference]
mkstruct_monotone [in LibSepReference]
mkstruct_frame [in LibSepReference]
mkstruct_conseq [in LibSepReference]
mkstruct_erase [in LibSepReference]
mkstruct_ramified [in LibSepReference]
mkstruct_monotone [in WPgen]
mkstruct_erase [in WPgen]
mkstruct_conseq [in WPgen]
mkstruct_frame [in WPgen]
mkstruct_idempotent [in WPsound]
mkstruct_sound' [in WPsound]
mkstruct_sound [in WPsound]
mkstruct_wp [in WPsound]
MList_if [in Repr]
MList_cons [in Repr]
MList_nil [in Repr]
MotivatingExampleSolved.triple_succ_using_incr' [in Affine]
MotivatingExample.triple_succ_using_incr' [in Affine]
MotivatingExample.triple_succ_using_incr [in Affine]
MTree_if [in Repr]
MTree_Node [in Repr]
MTree_Leaf [in Repr]
N
NewTriples.mkstruct_haffine_pre [in Affine]NewTriples.mkstruct_haffine_post [in Affine]
NewTriples.mkstruct_monotone [in Affine]
NewTriples.mkstruct_frame [in Affine]
NewTriples.mkstruct_conseq [in Affine]
NewTriples.mkstruct_erase [in Affine]
NewTriples.mkstruct_hgc [in Affine]
NewTriples.MotivatingExampleWithUpdatedXwp.triple_succ_using_incr [in Affine]
NewTriples.triple_ramified_frame_hgc [in Affine]
NewTriples.triple_conseq_frame_hgc [in Affine]
NewTriples.triple_haffine_pre [in Affine]
NewTriples.triple_hgc_post_from_triple_haffine_post [in Affine]
NewTriples.triple_haffine_post [in Affine]
NewTriples.triple_hgc_post [in Affine]
NewTriples.triple_seq [in Affine]
NewTriples.triple_hexists [in Affine]
NewTriples.triple_hpure [in Affine]
NewTriples.triple_frame [in Affine]
NewTriples.triple_conseq [in Affine]
NewTriples.wp_ramified [in Affine]
NewTriples.wp_haffine_pre [in Affine]
NewTriples.wp_hgc_post [in Affine]
NewTriples.wp_frame [in Affine]
NewTriples.wp_conseq [in Affine]
NewTriples.wp_equiv [in Affine]
NewTriples.xwp_lemma' [in Affine]
noduplicates_var_seq [in LibSepVar]
P
Pivot.triple_pivot' [in Arrays]Pivot.triple_array_swap_seg_self [in Arrays]
Pivot.triple_array_swap_seg_lists [in Arrays]
Pivot.triple_array_swap_seg [in Arrays]
Pivot.triple_array_get_hseg_vals_int [in Arrays]
ProofsSameSemantics.eta_same_triples [in Rules]
ProofsSameSemantics.eval_like_eta_expansion [in Rules]
ProofsSameSemantics.eval_like_eta_reduction [in Rules]
ProofsSameSemantics.triple_trm_seq_assoc [in Rules]
ProofsSameSemantics.triple_app_fun [in Rules]
ProofsSameSemantics.triple_eval_like [in Rules]
ProofsWithAdvancedXtactics.triple_incr [in WPgen]
ProofsWithStructuralXtactics.triple_incr_frame [in WPgen]
ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas [in WPgen]
ProofsWithXlemmas.triple_incr [in WPgen]
ProofsWithXtactics.triple_succ_using_incr_with_xtactics [in WPgen]
ProofsWithXtactics.triple_incr [in WPgen]
prove_eq_val_fix_trm_funs_demo [in LibSepReference]
prove_eq_val_funs_demo [in LibSepReference]
prove_eq_trm_apps_demo [in LibSepReference]
Q
qimpl_refl [in LibSepMinimal]qimpl_antisym [in Himpl]
qimpl_trans [in Himpl]
qimpl_refl [in Himpl]
qprop_eq [in Hprop]
QuickSort.length_vals_int [in Arrays]
QuickSort.permut_Forall [in Arrays]
QuickSort.permut_swap_first_last [in Arrays]
QuickSort.permut_swap_first_two [in Arrays]
QuickSort.permut_last [in Arrays]
QuickSort.permut_cons [in Arrays]
QuickSort.permut_app [in Arrays]
QuickSort.permut_length [in Arrays]
QuickSort.permut_sym [in Arrays]
QuickSort.permut_refl [in Arrays]
QuickSort.sorted_app_le [in Arrays]
QuickSort.sorted_cons_gt [in Arrays]
QuickSort.triple_quicksort_full [in Arrays]
QuickSort.triple_quicksort [in Arrays]
QuickSort.triple_quicksort_safety [in Arrays]
QuickSort.vals_int_last [in Arrays]
QuickSort.vals_int_app [in Arrays]
QuickSort.vals_int_cons [in Arrays]
QuickSort.vals_int_nil [in Arrays]
QwandEquiv.hwand_characterization_1_eq_2 [in Wand]
QwandEquiv.qwand_characterization_4_eq_5 [in Wand]
QwandEquiv.qwand_characterization_2_eq_4 [in Wand]
QwandEquiv.qwand_characterization_2_eq_3 [in Wand]
Qwand.himpl_qwand_hstar_same_r [in Wand]
Qwand.hstar_qwand [in Wand]
Qwand.qwand_cancel_part [in Wand]
Qwand.qwand_himpl [in Wand]
Qwand.qwand_cancel [in Wand]
Qwand.qwand_equiv [in Wand]
Qwand.qwand_specialize [in Wand]
R
RamifiedFrame.triple_ref_extended' [in Wand]RamifiedFrame.triple_ref_extended [in Wand]
RamifiedFrame.triple_conseq_frame_of_ramified_frame [in Wand]
RamifiedFrame.triple_ramified_frame [in Wand]
read_union_r [in LibSepFmap]
read_union_l [in LibSepFmap]
read_single [in LibSepFmap]
Realization.harray_focus_read [in Arrays]
Realization.harray_focus [in Arrays]
Realization.harray_eq [in Arrays]
Realization.hcell_nonneg [in Arrays]
Realization.hcell_eq [in Arrays]
Realization.hfields_eq_hrange [in Records]
Realization.hfields_update_preserves_maps_all_fields [in Records]
Realization.hfields_update_preserves_fields [in Records]
Realization.hheader_eq [in Arrays]
Realization.hrange_intro [in Arrays]
Realization.hseg_eq_hrange [in Arrays]
Realization.hseg_focus [in Arrays]
Realization.hseg_focus_relative [in Arrays]
Realization.hseg_app [in Arrays]
Realization.hseg_cons [in Arrays]
Realization.hseg_one [in Arrays]
Realization.hseg_nil [in Arrays]
Realization.hseg_start_eq [in Arrays]
Realization.triple_new_hrecord_2 [in Records]
Realization.triple_alloc_mcons [in Records]
Realization.triple_alloc_hrecord [in Records]
Realization.triple_set_field_hrecord [in Records]
Realization.triple_get_field_hrecord [in Records]
Realization.triple_set_field_hfields [in Records]
Realization.triple_get_field_hfields [in Records]
Realization.triple_set_field [in Records]
Realization.triple_get_field [in Records]
Realization.triple_array_make [in Arrays]
Realization.triple_array_length [in Arrays]
Realization.triple_array_set [in Arrays]
Realization.triple_array_get [in Arrays]
Realization.triple_array_make_hseg [in Arrays]
Realization.triple_array_fill [in Arrays]
Realization.triple_array_set_hseg [in Arrays]
Realization.triple_array_get_hseg [in Arrays]
Realization.triple_array_set_hcell [in Arrays]
Realization.triple_array_get_hcell [in Arrays]
Realization.triple_array_length_hheader [in Arrays]
Realization.triple_alloc [in Arrays]
Realization.triple_ptr_add_nonneg [in Arrays]
Realization.triple_ptr_add [in Arrays]
reducible_val_inv [in Triples]
remove_union_single_l [in LibSepFmap]
remove_disjoint_union_l [in LibSepFmap]
remove_single [in LibSepFmap]
rem_app [in LibSepReference]
S
SepSimplArgs.haffine_hgc [in LibSepReference]SepSimplArgs.haffine_hempty [in LibSepReference]
SepSimplArgs.haffine_hany [in LibSepReference]
SepSimplArgs.hempty_eq_hpure_true [in LibSepReference]
SepSimplArgs.hempty_inv [in LibSepReference]
SepSimplArgs.hempty_intro [in LibSepReference]
SepSimplArgs.hexists_inv [in LibSepReference]
SepSimplArgs.hexists_intro [in LibSepReference]
SepSimplArgs.hfalse_hstar_any [in LibSepReference]
SepSimplArgs.hforall_specialize [in LibSepReference]
SepSimplArgs.hforall_inv [in LibSepReference]
SepSimplArgs.hforall_intro [in LibSepReference]
SepSimplArgs.himpl_hgc_r [in LibSepReference]
SepSimplArgs.himpl_htop_r [in LibSepReference]
SepSimplArgs.himpl_qwand_r [in LibSepReference]
SepSimplArgs.himpl_hempty_hwand_same [in LibSepReference]
SepSimplArgs.himpl_hwand_r_inv [in LibSepReference]
SepSimplArgs.himpl_hwand_r [in LibSepReference]
SepSimplArgs.himpl_hforall [in LibSepReference]
SepSimplArgs.himpl_hforall_l [in LibSepReference]
SepSimplArgs.himpl_hforall_r [in LibSepReference]
SepSimplArgs.himpl_hexists [in LibSepReference]
SepSimplArgs.himpl_hexists_r [in LibSepReference]
SepSimplArgs.himpl_hexists_l [in LibSepReference]
SepSimplArgs.himpl_hstar_hpure_l [in LibSepReference]
SepSimplArgs.himpl_hempty_hpure [in LibSepReference]
SepSimplArgs.himpl_hstar_hpure_r [in LibSepReference]
SepSimplArgs.himpl_hstar_trans_r [in LibSepReference]
SepSimplArgs.himpl_hstar_trans_l [in LibSepReference]
SepSimplArgs.himpl_frame_lr [in LibSepReference]
SepSimplArgs.himpl_frame_r [in LibSepReference]
SepSimplArgs.himpl_frame_l [in LibSepReference]
SepSimplArgs.himpl_antisym [in LibSepReference]
SepSimplArgs.himpl_trans_r [in LibSepReference]
SepSimplArgs.himpl_trans [in LibSepReference]
SepSimplArgs.himpl_refl [in LibSepReference]
SepSimplArgs.hprop_op_comm [in LibSepReference]
SepSimplArgs.hpure_intro_hempty [in LibSepReference]
SepSimplArgs.hpure_inv_hempty [in LibSepReference]
SepSimplArgs.hpure_inv [in LibSepReference]
SepSimplArgs.hpure_intro [in LibSepReference]
SepSimplArgs.hsingle_inv [in LibSepReference]
SepSimplArgs.hsingle_intro [in LibSepReference]
SepSimplArgs.hstar_hgc_hgc [in LibSepReference]
SepSimplArgs.hstar_hsingle_same_loc [in LibSepReference]
SepSimplArgs.hstar_htop_htop [in LibSepReference]
SepSimplArgs.hstar_hpure_r [in LibSepReference]
SepSimplArgs.hstar_hpure_l [in LibSepReference]
SepSimplArgs.hstar_hforall [in LibSepReference]
SepSimplArgs.hstar_hexists [in LibSepReference]
SepSimplArgs.hstar_hempty_r [in LibSepReference]
SepSimplArgs.hstar_hempty_l [in LibSepReference]
SepSimplArgs.hstar_assoc [in LibSepReference]
SepSimplArgs.hstar_comm [in LibSepReference]
SepSimplArgs.hstar_inv [in LibSepReference]
SepSimplArgs.hstar_intro [in LibSepReference]
SepSimplArgs.htop_eq [in LibSepReference]
SepSimplArgs.htop_intro [in LibSepReference]
SepSimplArgs.hwand_inv [in LibSepReference]
SepSimplArgs.hwand_curry_eq [in LibSepReference]
SepSimplArgs.hwand_uncurry [in LibSepReference]
SepSimplArgs.hwand_curry [in LibSepReference]
SepSimplArgs.hwand_hpure_l [in LibSepReference]
SepSimplArgs.hwand_hempty_l [in LibSepReference]
SepSimplArgs.hwand_cancel [in LibSepReference]
SepSimplArgs.hwand_equiv [in LibSepReference]
SepSimplArgs.qimpl_refl [in LibSepReference]
SepSimplArgs.qwand_specialize [in LibSepReference]
SepSimplArgs.qwand_cancel [in LibSepReference]
SepSimplArgs.qwand_equiv [in LibSepReference]
seval_frame [in Triples]
seval_conseq [in Triples]
seval_of_eval [in Triples]
seval_if [in Triples]
seval_let [in Triples]
seval_seq [in Triples]
seval_app_fix [in Triples]
seval_app_fun [in Triples]
seval_fix [in Triples]
seval_fun [in Triples]
seval_sound [in Triples]
seval_correct [in Triples]
seval_safe [in Triples]
seval_terminates [in Triples]
seval_val_inv [in Triples]
seval_of_eval [in LibSepReference]
seval_if [in LibSepReference]
seval_app_arg2 [in LibSepReference]
seval_app_arg1 [in LibSepReference]
seval_let [in LibSepReference]
seval_seq [in LibSepReference]
seval_app_fix [in LibSepReference]
seval_app_fun [in LibSepReference]
seval_fix [in LibSepReference]
seval_fun [in LibSepReference]
seval_correct [in LibSepReference]
seval_safe [in LibSepReference]
seval_terminates [in LibSepReference]
single_fresh [in LibSepFmap]
SizedStack.triple_top [in Repr]
SizedStack.triple_pop [in Repr]
SizedStack.triple_push [in Repr]
SizedStack.triple_sizeof [in Repr]
SizedStack.triple_create [in Repr]
soundness_small_step [in Triples]
steps_trans [in Triples]
steps_of_step [in Triples]
steps_trans [in LibSepReference]
steps_of_step [in LibSepReference]
striple_frame [in Triples]
striple_conseq [in Triples]
striple_sound [in Triples]
StructuralRules.triple_hpure' [in Triples]
StructuralRules.triple_conseq_frame [in Triples]
subst_trm_funs [in LibSepReference]
subst_eq_isubst_one [in LibSepReference]
T
TexanTriples.texan_triple_equiv [in WPsem]TexanTriples.wp_free' [in WPsem]
TexanTriples.wp_set' [in WPsem]
TexanTriples.wp_free [in WPsem]
TexanTriples.wp_set [in WPsem]
TexanTriples.wp_get [in WPsem]
TexanTriples.wp_ref_3 [in WPsem]
TexanTriples.wp_ref_2 [in WPsem]
TexanTriples.wp_ref_1 [in WPsem]
TexanTriples.wp_ref_0 [in WPsem]
tree_sub_wf [in Repr]
triple_named_heap [in Triples]
triple_hexists [in Triples]
triple_hpure [in Triples]
triple_frame [in Triples]
triple_conseq [in Triples]
triple_hand_r [in LibSepReference]
triple_hand_l [in LibSepReference]
triple_hor [in LibSepReference]
triple_of_wpgen [in LibSepReference]
triple_ptr_add_nat [in LibSepReference]
triple_ptr_add [in LibSepReference]
triple_gt [in LibSepReference]
triple_ge [in LibSepReference]
triple_lt [in LibSepReference]
triple_le [in LibSepReference]
triple_mod [in LibSepReference]
triple_mul [in LibSepReference]
triple_sub [in LibSepReference]
triple_neq [in LibSepReference]
triple_eq [in LibSepReference]
triple_opp [in LibSepReference]
triple_neg [in LibSepReference]
triple_rand [in LibSepReference]
triple_div [in LibSepReference]
triple_add [in LibSepReference]
triple_binop [in LibSepReference]
triple_unop [in LibSepReference]
triple_binop' [in LibSepReference]
triple_unop' [in LibSepReference]
triple_free [in LibSepReference]
triple_free' [in LibSepReference]
triple_set [in LibSepReference]
triple_get [in LibSepReference]
triple_ref [in LibSepReference]
triple_app_fix_direct [in LibSepReference]
triple_app_fix [in LibSepReference]
triple_app_fun_direct [in LibSepReference]
triple_app_fun [in LibSepReference]
triple_if [in LibSepReference]
triple_let_val [in LibSepReference]
triple_let [in LibSepReference]
triple_seq [in LibSepReference]
triple_fix [in LibSepReference]
triple_fun [in LibSepReference]
triple_val_minimal [in LibSepReference]
triple_val [in LibSepReference]
triple_eval_like [in LibSepReference]
triple_ramified_frame [in LibSepReference]
triple_conseq_frame [in LibSepReference]
triple_named_heap [in LibSepReference]
triple_hwand_hpure_l [in LibSepReference]
triple_hforall [in LibSepReference]
triple_hexists [in LibSepReference]
triple_hpure [in LibSepReference]
triple_frame [in LibSepReference]
triple_conseq [in LibSepReference]
triple_sound [in LibSepReference]
triple_cps_append [in Repr]
triple_cps_append_aux [in Repr]
triple_cps_facto [in Repr]
triple_cps_facto_aux [in Repr]
triple_mlength_using_miter [in Repr]
triple_miter [in Repr]
triple_repeat [in Repr]
triple_test_counter [in Repr]
triple_apply_counter_abstract [in Repr]
triple_create_counter_abstract [in Repr]
triple_create_counter [in Repr]
triple_mtreesum [in Repr]
triple_tree_copy [in Repr]
triple_mnode' [in Repr]
triple_mnode [in Repr]
triple_mrev [in Repr]
triple_mfree [in Repr]
triple_mlength' [in Repr]
triple_mlength [in Repr]
triple_mcopy' [in Repr]
triple_mcopy [in Repr]
triple_mcons' [in Repr]
triple_mcons [in Repr]
triple_mnil' [in Repr]
triple_mnil [in Repr]
triple_append [in Repr]
triple_var' [in WPgen]
triple_var [in WPgen]
triple_set [in Rules]
triple_get [in Rules]
triple_free [in Rules]
triple_free' [in Rules]
triple_ref' [in Rules]
triple_ref [in Rules]
triple_rand [in Rules]
triple_div [in Rules]
triple_add' [in Rules]
triple_add [in Rules]
triple_app_fix [in Rules]
triple_app_fun [in Rules]
triple_fix [in Rules]
triple_fun [in Rules]
triple_val' [in Rules]
triple_val_minimal [in Rules]
triple_val [in Rules]
triple_if [in Rules]
triple_if_case [in Rules]
triple_let [in Rules]
triple_seq [in Rules]
triple_incr [in LibSepMinimal]
triple_free [in LibSepMinimal]
triple_set [in LibSepMinimal]
triple_get [in LibSepMinimal]
triple_ref [in LibSepMinimal]
triple_rand [in LibSepMinimal]
triple_div [in LibSepMinimal]
triple_add [in LibSepMinimal]
triple_let [in LibSepMinimal]
triple_app_fix [in LibSepMinimal]
triple_if [in LibSepMinimal]
triple_fix [in LibSepMinimal]
triple_val [in LibSepMinimal]
triple_hpure [in LibSepMinimal]
triple_hexists [in LibSepMinimal]
triple_frame [in LibSepMinimal]
triple_conseq [in LibSepMinimal]
triple_mcons [in Records]
triple_app_fix_from_wpgen [in WPsound]
triple_app_fun_from_wpgen [in WPsound]
triple_of_wpgen [in WPsound]
triple_factoimp' [in Basic]
triple_factoimp_aux' [in Basic]
triple_factoimp_zero [in Basic]
triple_factoimp_aux_zero [in Basic]
triple_factoimp [in Basic]
triple_factoimp_aux [in Basic]
triple_step_transfer [in Basic]
triple_repeat_incr' [in Basic]
triple_repeat_incr_incorrect [in Basic]
triple_repeat_incr' [in Basic]
triple_repeat_incr [in Basic]
triple_factorec [in Basic]
triple_two_dice [in Basic]
triple_get_and_free [in Basic]
triple_succ_using_incr [in Basic]
triple_succ_using_incr_attempt' [in Basic]
triple_succ_using_incr_attempt [in Basic]
triple_ref_greater [in Basic]
triple_incr_first_derived [in Basic]
triple_incr_first' [in Basic]
triple_incr_first [in Basic]
triple_aliased_call [in Basic]
triple_incr_two_aliased [in Basic]
triple_aliased_call [in Basic]
triple_incr_two [in Basic]
triple_example_let [in Basic]
triple_incr' [in Basic]
triple_incr [in Basic]
triple_hpure_with_wp [in WPsem]
trms_to_vals_spec [in LibSepReference]
trms_vals_cons [in LibSepReference]
trms_vals_nil [in LibSepReference]
trm_apps_of_trm_demo [in LibSepReference]
U
union_eq_cancel_4' [in LibSepFmap]union_eq_cancel_4 [in LibSepFmap]
union_eq_cancel_3' [in LibSepFmap]
union_eq_cancel_3 [in LibSepFmap]
union_eq_cancel_2' [in LibSepFmap]
union_eq_cancel_2 [in LibSepFmap]
union_eq_cancel_1' [in LibSepFmap]
union_eq_cancel_1 [in LibSepFmap]
union_eq_inv_of_disjoint [in LibSepFmap]
union_assoc [in LibSepFmap]
union_comm_of_agree [in LibSepFmap]
union_comm_of_disjoint [in LibSepFmap]
union_eq_empty_inv_r [in LibSepFmap]
union_eq_empty_inv_l [in LibSepFmap]
union_empty_r [in LibSepFmap]
union_empty_l [in LibSepFmap]
union_self [in LibSepFmap]
update_union_not_l [in LibSepFmap]
update_union_not_r [in LibSepFmap]
update_union_r [in LibSepFmap]
update_union_l [in LibSepFmap]
update_single [in LibSepFmap]
update_empty [in LibSepFmap]
update_eq_union_single [in LibSepFmap]
V
var_funs_exec_eq [in LibSepReference]var_fresh_var_seq_ge [in LibSepVar]
var_fresh_var_seq_lt [in LibSepVar]
var_fresh_mem_inv [in LibSepVar]
var_eq_spec [in LibSepVar]
W
WpFromTriple.wp_equiv_1 [in WPsem]WpFromTriple2.wp_equiv_2 [in WPsem]
WpgenExec1.triple_incr [in WPgen]
WpgenExec1.wpgen_frame [in WPgen]
WpgenExec1.wpgen_conseq [in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_forloop [in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_incrtwice' [in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.triple_incrtwice [in WPgen]
WPgenRec.wpgen_fun_eq [in WPgen]
WPgenRec.xfun_nospec_lemma [in WPgen]
WPgenRec.xfun_spec_lemma [in WPgen]
WPgenWithNotation.triple_incr [in WPgen]
wpgen_sound [in LibSepReference]
wpgen_app_sound [in LibSepReference]
wpgen_if_sound [in LibSepReference]
wpgen_let_sound [in LibSepReference]
wpgen_seq_sound [in LibSepReference]
wpgen_fix_sound [in LibSepReference]
wpgen_fun_sound [in LibSepReference]
wpgen_val_sound [in LibSepReference]
wpgen_fail_sound [in LibSepReference]
wpgen_sound [in WPsound]
wpgen_sound_induct [in WPsound]
wpgen_fix_val_sound [in WPsound]
wpgen_fun_val_sound [in WPsound]
wpgen_fix_sound [in WPsound]
wpgen_fun_sound [in WPsound]
wpgen_fail_sound [in WPsound]
wpgen_app_sound [in WPsound]
wpgen_if_sound [in WPsound]
wpgen_let_sound [in WPsound]
wpgen_val_sound [in WPsound]
wpgen_seq_sound [in WPsound]
wp_sound [in LibSepReference]
wp_if_case [in LibSepReference]
wp_if [in LibSepReference]
wp_let [in LibSepReference]
wp_seq [in LibSepReference]
wp_app_fix [in LibSepReference]
wp_app_fun [in LibSepReference]
wp_fix [in LibSepReference]
wp_fun [in LibSepReference]
wp_val [in LibSepReference]
wp_eval_like [in LibSepReference]
wp_ramified_trans [in LibSepReference]
wp_conseq_frame [in LibSepReference]
wp_ramified [in LibSepReference]
wp_frame [in LibSepReference]
wp_conseq [in LibSepReference]
wp_equiv [in LibSepReference]
wp_var [in WPgen]
wp_equiv_iff_wp_pre_and_wp_weakest [in WPsem]
wp_unique [in WPsem]
wp_conseq_frame [in WPsem]
wp_conseq_frame_trans [in WPsem]
wp_app_fix [in WPsem]
wp_app_fun [in WPsem]
wp_if' [in WPsem]
wp_if [in WPsem]
wp_fix [in WPsem]
wp_fun [in WPsem]
wp_let [in WPsem]
wp_seq [in WPsem]
wp_val [in WPsem]
wp_frame_of_wp_ramified [in WPsem]
wp_conseq_of_wp_ramified [in WPsem]
wp_ramified_trans [in WPsem]
wp_ramified [in WPsem]
wp_conseq_trans [in WPsem]
wp_conseq [in WPsem]
wp_frame_trans [in WPsem]
wp_frame [in WPsem]
wp_weakest [in WPsem]
wp_pre [in WPsem]
wp_equiv [in WPsem]
X
Xaffine.xaffine_demo [in Affine]xapp_simpl_lemma [in LibSepReference]
xapp_lemma [in LibSepReference]
xapp_lemma [in WPgen]
xapp_set_field_lemma [in Records]
xapp_get_field_lemma [in Records]
xchange_lemma [in LibSepMinimal]
xconseq_lemma [in WPgen]
xfix_nospec_lemma [in LibSepReference]
xfix_spec_lemma [in LibSepReference]
xframe_lemma [in WPgen]
xfun_nospec_lemma [in LibSepReference]
xfun_spec_lemma [in LibSepReference]
XGC.xgc_keep_demo [in Affine]
XGC.xgc_post_lemma [in Affine]
XGC.xgc_keep_demo [in Affine]
XGC.xgc_demo [in Affine]
XGC.xgc_lemma [in Affine]
xif_lemma [in LibSepReference]
xlet_lemma [in LibSepReference]
xlet_lemma [in WPgen]
xseq_lemma [in LibSepReference]
xseq_lemma [in WPgen]
XsimplDemo.xsimpl_hwand_frame [in Wand]
XsimplDemo.xsimpl_demo_qwand_cancel [in Wand]
XsimplDemo.xsimpl_demo_hwand_iter_2 [in Wand]
XsimplDemo.xsimpl_demo_hwand_iter [in Wand]
XsimplDemo.xsimpl_demo_himpl_hwand_r [in Wand]
XsimplDemo.xsimpl_demo_hwand_cancel_partial [in Wand]
XsimplDemo.xsimpl_demo_hwand_cancel [in Wand]
XsimplExtended.xsimpl_xaffine_demo [in Affine]
XsimplExtended.xsimpl_xgc_demo [in Affine]
XsimplSetup.demo_hstars_simpl_2 [in LibSepSimpl]
XsimplSetup.demo_hstars_simpl_1 [in LibSepSimpl]
XsimplSetup.demo_hstars_pick_1 [in LibSepSimpl]
XsimplSetup.himpl_lr_hgc [in LibSepSimpl]
XsimplSetup.himpl_lr_htop [in LibSepSimpl]
XsimplSetup.himpl_lr_qwand_unify [in LibSepSimpl]
XsimplSetup.himpl_lr_refl [in LibSepSimpl]
XsimplSetup.himpl_hstar_trans_l [in LibSepSimpl]
XsimplSetup.himpl_of_eq_sym [in LibSepSimpl]
XsimplSetup.himpl_of_eq [in LibSepSimpl]
XsimplSetup.hstars_flip_demo_0 [in LibSepSimpl]
XsimplSetup.hstars_flip_demo [in LibSepSimpl]
XsimplSetup.hstars_simpl_pick_lemma [in LibSepSimpl]
XsimplSetup.hstars_simpl_cancel [in LibSepSimpl]
XsimplSetup.hstars_simpl_keep [in LibSepSimpl]
XsimplSetup.hstars_simpl_start [in LibSepSimpl]
XsimplSetup.hstars_pick_last_9 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_8 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_7 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_6 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_5 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_4 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_3 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_2 [in LibSepSimpl]
XsimplSetup.hstars_pick_last_1 [in LibSepSimpl]
XsimplSetup.hstars_pick_9 [in LibSepSimpl]
XsimplSetup.hstars_pick_8 [in LibSepSimpl]
XsimplSetup.hstars_pick_7 [in LibSepSimpl]
XsimplSetup.hstars_pick_6 [in LibSepSimpl]
XsimplSetup.hstars_pick_5 [in LibSepSimpl]
XsimplSetup.hstars_pick_4 [in LibSepSimpl]
XsimplSetup.hstars_pick_3 [in LibSepSimpl]
XsimplSetup.hstars_pick_2 [in LibSepSimpl]
XsimplSetup.hstars_pick_1 [in LibSepSimpl]
XsimplSetup.hstars_flip_9 [in LibSepSimpl]
XsimplSetup.hstars_flip_8 [in LibSepSimpl]
XsimplSetup.hstars_flip_7 [in LibSepSimpl]
XsimplSetup.hstars_flip_6 [in LibSepSimpl]
XsimplSetup.hstars_flip_5 [in LibSepSimpl]
XsimplSetup.hstars_flip_4 [in LibSepSimpl]
XsimplSetup.hstars_flip_3 [in LibSepSimpl]
XsimplSetup.hstars_flip_2 [in LibSepSimpl]
XsimplSetup.hstars_flip_1 [in LibSepSimpl]
XsimplSetup.hstars_flip_0 [in LibSepSimpl]
XsimplSetup.hstar_comm_assoc [in LibSepSimpl]
XsimplSetup.qimpl_antisym [in LibSepSimpl]
XsimplSetup.qimpl_trans [in LibSepSimpl]
XsimplSetup.qimpl_refl [in LibSepSimpl]
XsimplSetup.repr_id [in LibSepSimpl]
XsimplSetup.repr_eq [in LibSepSimpl]
XsimplSetup.rew_heap_demo_with_evar [in LibSepSimpl]
XsimplSetup.star_post_empty [in LibSepSimpl]
XsimplSetup.xchange_demo_hforall_l [in LibSepSimpl]
XsimplSetup.xchange_demo_4 [in LibSepSimpl]
XsimplSetup.xchange_demo_2 [in LibSepSimpl]
XsimplSetup.xchange_demo_1 [in LibSepSimpl]
XsimplSetup.xchange_lemma [in LibSepSimpl]
XsimplSetup.xpull_demo [in LibSepSimpl]
XsimplSetup.xpull_protect [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hfalse [in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_4 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_3 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_2 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_1 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_gc_0 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_4 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_3 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_2 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_repr_1 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_iter [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_hstar_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_multiple_2 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_multiple_1 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_qwand_r [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand_r [in LibSepSimpl]
XsimplSetup.xsimpl_demo_qwand [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hwand [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hgc_multiple [in LibSepSimpl]
XsimplSetup.xsimpl_demo_htop_multiple [in LibSepSimpl]
XsimplSetup.xsimpl_demo_htop_both_sides [in LibSepSimpl]
XsimplSetup.xsimpl_demo_evar_2 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_evar_1 [in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars_gc [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hint [in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars_top [in LibSepSimpl]
XsimplSetup.xsimpl_demo_keep_order [in LibSepSimpl]
XsimplSetup.xsimpl_demo_stars [in LibSepSimpl]
XsimplSetup.xsimpl_pick_demo [in LibSepSimpl]
XsimplSetup.xsimpl_demo_hints [in LibSepSimpl]
XsimplSetup.xsimpl_pick_lemma [in LibSepSimpl]
XsimplSetup.xsimpl_flip_acc_r [in LibSepSimpl]
XsimplSetup.xsimpl_flip_acc_l [in LibSepSimpl]
XsimplSetup.xsimpl_lr_exit [in LibSepSimpl]
XsimplSetup.xsimpl_lr_exit_nogc [in LibSepSimpl]
XsimplSetup.xsimpl_lr_hforall [in LibSepSimpl]
XsimplSetup.xsimpl_lr_qwand_unit [in LibSepSimpl]
XsimplSetup.xsimpl_lr_qwand [in LibSepSimpl]
XsimplSetup.xsimpl_lr_hwand_hfalse [in LibSepSimpl]
XsimplSetup.xsimpl_lr_hwand [in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_eq_repr [in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_eq [in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_hgc [in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_htop [in LibSepSimpl]
XsimplSetup.xsimpl_lr_cancel_same [in LibSepSimpl]
XsimplSetup.xsimpl_r_htop_drop [in LibSepSimpl]
XsimplSetup.xsimpl_r_hgc_drop [in LibSepSimpl]
XsimplSetup.xsimpl_r_htop_replace_hgc [in LibSepSimpl]
XsimplSetup.xsimpl_r_hgc_or_htop [in LibSepSimpl]
XsimplSetup.xsimpl_r_keep [in LibSepSimpl]
XsimplSetup.xsimpl_r_id_unify [in LibSepSimpl]
XsimplSetup.xsimpl_r_id [in LibSepSimpl]
XsimplSetup.xsimpl_r_hexists [in LibSepSimpl]
XsimplSetup.xsimpl_r_hpure [in LibSepSimpl]
XsimplSetup.xsimpl_r_hwand_same [in LibSepSimpl]
XsimplSetup.xsimpl_r_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hstar_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hstar [in LibSepSimpl]
XsimplSetup.xsimpl_l_hwand_reorder [in LibSepSimpl]
XsimplSetup.xsimpl_l_keep_wand [in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_qwand [in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand [in LibSepSimpl]
XsimplSetup.xsimpl_l_cancel_hwand_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_l_acc_other [in LibSepSimpl]
XsimplSetup.xsimpl_l_acc_wand [in LibSepSimpl]
XsimplSetup.xsimpl_l_hexists [in LibSepSimpl]
XsimplSetup.xsimpl_l_hpure [in LibSepSimpl]
XsimplSetup.xsimpl_l_hempty [in LibSepSimpl]
XsimplSetup.xsimpl_start [in LibSepSimpl]
XsimplSetup.Xsimpl_trans [in LibSepSimpl]
XsimplSetup.Xsimpl_trans_r [in LibSepSimpl]
XsimplSetup.Xsimpl_trans_l [in LibSepSimpl]
XsimplTactic.EntailmentProofs.himpl_example_3 [in Himpl]
XsimplTactic.EntailmentProofs.himpl_example_2 [in Himpl]
XsimplTactic.EntailmentProofs.himpl_example_1 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_12 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_11 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_10 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_8 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_7 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_6 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_4 [in Himpl]
XsimplTactic.EntailmentQuizAnswers.case_study_1 [in Himpl]
XsimplTactic.qimpl_example_1 [in Himpl]
XsimplTactic.xchange_lemma [in Himpl]
XsimplTactic.xchange_demo_inst [in Himpl]
XsimplTactic.xchange_demo_eq [in Himpl]
XsimplTactic.xchange_demo_base [in Himpl]
XsimplTactic.xpull_example_3 [in Himpl]
XsimplTactic.xpull_example_2 [in Himpl]
XsimplTactic.xpull_example_1 [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hints_evar [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hints [in Himpl]
XsimplTactic.xsimpl_demo_rhs_exists_solved_2 [in Himpl]
XsimplTactic.xsimpl_demo_rhs_exists_solved_1 [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists_unify_view [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists_unify [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hexists [in Himpl]
XsimplTactic.xsimpl_demo_rhs_hpure [in Himpl]
XsimplTactic.xsimpl_demo_cancel_all [in Himpl]
XsimplTactic.xsimpl_demo_cancel_many [in Himpl]
XsimplTactic.xsimpl_demo_cancel_one [in Himpl]
XsimplTactic.xsimpl_demo_lhs_several [in Himpl]
XsimplTactic.xsimpl_demo_lhs_hexists [in Himpl]
XsimplTactic.xsimpl_demo_lhs_hpure [in Himpl]
XsimplTactic.xsimpl_demo_lhs_hpure [in Himpl]
xstruct_lemma [in LibSepReference]
xstruct_lemma [in WPgen]
xtriple_lemma [in LibSepReference]
xval_lemma [in LibSepReference]
xval_lemma [in WPgen]
xwp_lemma_fixs [in LibSepReference]
xwp_lemma_funs [in LibSepReference]
xwp_lemma_fix [in LibSepReference]
xwp_lemma_fun [in LibSepReference]
xwp_lemma [in WPgen]
Axiom Index
B
BakedInFrame.eval [in Triples]D
DivSpec.triple_div' [in Rules]DivSpec.triple_div [in Rules]
E
eval_rand [in Rules]eval_div [in Rules]
eval_add [in Rules]
ExamplePrograms2.triple_hpure' [in Rules]
Extensionality.functional_extensionality [in Hprop]
Extensionality.propositional_extensionality [in Hprop]
F
Facto.facto [in Basic]Facto.facto_step [in Basic]
Facto.facto_init [in Basic]
FromPreToPostGC.eta_same_triples [in Affine]
FromPreToPostGC.triple_hgc_post [in Affine]
FromPreToPostGC.triple_hgc_pre [in Affine]
FullyAffineLogic.heap_affine_def [in Affine]
FullyLinearLogic.heap_affine_def [in Affine]
functional_extensionality [in LibSepReference]
functional_extensionality [in Hprop]
functional_extensionality [in LibSepMinimal]
H
harray [in Arrays]hcell [in Arrays]
heap_affine_union [in Affine]
heap_affine_empty [in Affine]
heap_affine [in Affine]
hheader [in Arrays]
himpl_frame_l [in Himpl]
hrecord [in LibSepReference]
hrecord_not_null [in LibSepReference]
hseg_app [in Arrays]
hseg_one [in Arrays]
hseg_nil [in Arrays]
hstar_hpure_l [in Hprop]
hstar_hexists [in Hprop]
hstar_hempty_l [in Hprop]
hstar_comm [in Hprop]
hstar_assoc [in Hprop]
hstar_assoc_statement [in Hprop]
I
isubst_rem [in WPsound]isubst_nil [in WPsound]
L
LetFrame.triple_let [in Rules]M
MatchStyle.triple_ref' [in Rules]MatchStyle.triple_ref [in Rules]
MkstructProp.mkstruct [in WPgen]
MkstructProp.mkstruct_monotone [in WPgen]
MkstructProp.mkstruct_erase [in WPgen]
MkstructProp.mkstruct_conseq [in WPgen]
MkstructProp.mkstruct_frame [in WPgen]
N
NewTriples.MotivatingExampleWithUpdatedXwp.haffine_hany [in Affine]NewTriples.xwp_lemma [in Affine]
P
predicate_extensionality [in Hprop]Preview.haffine [in Affine]
Preview.triple_haffine_pre [in Affine]
Preview.triple_haffine_post [in Affine]
propositional_extensionality [in LibSepReference]
propositional_extensionality [in LibSepMinimal]
Q
QuickSort.harray_eq [in Arrays]QuickSort.triple_pivot [in Arrays]
QuickSort.triple_pivot_safety [in Arrays]
QuickSort.val_pivot [in Arrays]
R
RamifiedFrame.triple_ref [in Wand]RamifiedFrame.triple_conseq_frame' [in Wand]
RamifiedFrame.triple_conseq_frame [in Wand]
Realization.eval_alloc [in Arrays]
Realization.eval_ptr_add [in Arrays]
Realization.harray_focus' [in Arrays]
Realization.harray_focus_read' [in Arrays]
Realization.val_alloc [in Arrays]
Realization.val_ptr_add [in Arrays]
S
StructuralRules.triple_hexists [in Triples]StructuralRules.triple_hpure [in Triples]
StructuralRules.triple_conseq [in Triples]
StructuralRules.triple_frame [in Triples]
T
TexanTriples.incr [in WPsem]TexanTriples.triple_incr [in WPsem]
TexanTriples.triple_free' [in WPsem]
TexanTriples.triple_set' [in WPsem]
TexanTriples.triple_ref [in WPsem]
TexanTriples.wp_ref [in WPsem]
triple_dealloc_hrecord [in LibSepReference]
triple_new_hrecord_3 [in LibSepReference]
triple_new_hrecord_2 [in LibSepReference]
triple_alloc_hrecord [in LibSepReference]
triple_set_field_hrecord [in LibSepReference]
triple_get_field_hrecord [in LibSepReference]
triple_hpure' [in LibSepReference]
triple_app_fun_from_wpgen [in WPgen]
triple_new_hrecord_2 [in Records]
triple_set_field_hrecord [in Records]
triple_set_field_hfields [in Records]
triple_set_field [in Records]
triple_get_field_hrecord [in Records]
triple_get_field_hfields [in Records]
triple_get_field [in Records]
triple_rand [in Basic]
triple_ref_with_frame [in Basic]
triple_ref' [in Basic]
triple_ref [in Basic]
triple_hgc_post [in Affine]
triple_hany_pre [in Affine]
triple_hany_post [in Affine]
triple_conseq_frame [in WPsem]
triple_app_fun [in WPsem]
triple_if [in WPsem]
triple_fun [in WPsem]
triple_let [in WPsem]
triple_seq [in WPsem]
triple_val [in WPsem]
triple_ramified_frame [in WPsem]
triple_hpure [in WPsem]
triple_array_set_hseg [in Arrays]
triple_array_get_hseg [in Arrays]
triple_array_make_hseg [in Arrays]
triple_array_set_hcell [in Arrays]
triple_array_get_hcell [in Arrays]
triple_array_length_hheader [in Arrays]
triple_array_set [in Arrays]
triple_array_get [in Arrays]
triple_array_length [in Arrays]
triple_array_make' [in Arrays]
triple_array_make [in Arrays]
V
val_dealloc_hrecord [in LibSepReference]val_new_hrecord_3 [in LibSepReference]
val_new_hrecord_2 [in LibSepReference]
val_alloc_hrecord [in LibSepReference]
val_set_field [in LibSepReference]
val_get_field [in LibSepReference]
val_new_hrecord_2 [in Records]
val_set_field [in Records]
val_get_field [in Records]
val_array_set [in Arrays]
val_array_get [in Arrays]
val_array_length [in Arrays]
val_array_make [in Arrays]
W
WpgenExec1.triple_app_fun_from_wpgen [in WPgen]WpgenExec1.triple_app_fun [in WPgen]
WpgenExec1.wpgen_sound [in WPgen]
WPgenRec.triple_app_fun_from_wpgen [in WPgen]
WPgenWithNotation.triple_app_fun_from_wpgen [in WPgen]
wpgen_sound_seq_3 [in WPsound]
wpgen_sound_seq_2 [in WPsound]
wpgen_sound_seq_1 [in WPsound]
wp_if [in WPgen]
wp_let [in WPgen]
wp_seq [in WPgen]
wp_fun [in WPgen]
wp_val [in WPgen]
X
xapp_set_field_lemma [in LibSepReference]xapp_get_field_lemma [in LibSepReference]
XGC.mkstruct_hgc [in Affine]
XsimplParams.haffine [in LibSepSimpl]
XsimplParams.haffine_hempty [in LibSepSimpl]
XsimplParams.hempty [in LibSepSimpl]
XsimplParams.hexists [in LibSepSimpl]
XsimplParams.hforall [in LibSepSimpl]
XsimplParams.hgc [in LibSepSimpl]
XsimplParams.himpl [in LibSepSimpl]
XsimplParams.himpl_hgc_r [in LibSepSimpl]
XsimplParams.himpl_htop_r [in LibSepSimpl]
XsimplParams.himpl_hforall_r [in LibSepSimpl]
XsimplParams.himpl_hexists_r [in LibSepSimpl]
XsimplParams.himpl_hexists_l [in LibSepSimpl]
XsimplParams.himpl_hstar_hpure_l [in LibSepSimpl]
XsimplParams.himpl_hempty_hpure [in LibSepSimpl]
XsimplParams.himpl_frame_lr [in LibSepSimpl]
XsimplParams.himpl_antisym [in LibSepSimpl]
XsimplParams.himpl_trans [in LibSepSimpl]
XsimplParams.himpl_refl [in LibSepSimpl]
XsimplParams.hprop [in LibSepSimpl]
XsimplParams.hpure [in LibSepSimpl]
XsimplParams.hstar [in LibSepSimpl]
XsimplParams.hstar_hgc_hgc [in LibSepSimpl]
XsimplParams.hstar_htop_htop [in LibSepSimpl]
XsimplParams.hstar_hforall [in LibSepSimpl]
XsimplParams.hstar_hexists [in LibSepSimpl]
XsimplParams.hstar_assoc [in LibSepSimpl]
XsimplParams.hstar_comm [in LibSepSimpl]
XsimplParams.hstar_hempty_r [in LibSepSimpl]
XsimplParams.hstar_hempty_l [in LibSepSimpl]
XsimplParams.htop [in LibSepSimpl]
XsimplParams.hwand [in LibSepSimpl]
XsimplParams.hwand_cancel [in LibSepSimpl]
XsimplParams.hwand_hempty_l [in LibSepSimpl]
XsimplParams.hwand_curry_eq [in LibSepSimpl]
XsimplParams.hwand_equiv [in LibSepSimpl]
XsimplParams.qwand [in LibSepSimpl]
XsimplParams.qwand_specialize [in LibSepSimpl]
XsimplParams.qwand_equiv [in LibSepSimpl]
XsimplTactic.EntailmentQuiz.case_study_12 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_11 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_10 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_9 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_8 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_7 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_6 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_5 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_4 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_3 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_2 [in Himpl]
XsimplTactic.EntailmentQuiz.case_study_1 [in Himpl]
Constructor Index
B
big_free [in Triples]big_set [in Triples]
big_get [in Triples]
big_ref [in Triples]
big_rand [in Triples]
big_div [in Triples]
big_add [in Triples]
big_if [in Triples]
big_let [in Triples]
big_seq [in Triples]
big_app_fix [in Triples]
big_app_fun [in Triples]
big_fix [in Triples]
big_fun [in Triples]
big_val [in Triples]
E
evalbinop_ptr_add [in LibSepReference]evalbinop_gt [in LibSepReference]
evalbinop_ge [in LibSepReference]
evalbinop_lt [in LibSepReference]
evalbinop_le [in LibSepReference]
evalbinop_mod [in LibSepReference]
evalbinop_div [in LibSepReference]
evalbinop_mul [in LibSepReference]
evalbinop_sub [in LibSepReference]
evalbinop_add [in LibSepReference]
evalbinop_neq [in LibSepReference]
evalbinop_eq [in LibSepReference]
evalunop_rand [in LibSepReference]
evalunop_opp [in LibSepReference]
evalunop_neg [in LibSepReference]
eval_free [in Triples]
eval_set [in Triples]
eval_get [in Triples]
eval_ref [in Triples]
eval_rand [in Triples]
eval_div [in Triples]
eval_add [in Triples]
eval_if [in Triples]
eval_let [in Triples]
eval_seq [in Triples]
eval_app_fix [in Triples]
eval_app_fun [in Triples]
eval_fix [in Triples]
eval_fun [in Triples]
eval_val [in Triples]
eval_free [in LibSepReference]
eval_set [in LibSepReference]
eval_get [in LibSepReference]
eval_ref [in LibSepReference]
eval_binop [in LibSepReference]
eval_unop [in LibSepReference]
eval_if [in LibSepReference]
eval_let [in LibSepReference]
eval_seq [in LibSepReference]
eval_app_fix [in LibSepReference]
eval_app_fun [in LibSepReference]
eval_app_arg2 [in LibSepReference]
eval_app_arg1 [in LibSepReference]
eval_fix [in LibSepReference]
eval_fun [in LibSepReference]
eval_val [in LibSepReference]
eval_free [in LibSepMinimal]
eval_set [in LibSepMinimal]
eval_get [in LibSepMinimal]
eval_ref [in LibSepMinimal]
eval_rand [in LibSepMinimal]
eval_div [in LibSepMinimal]
eval_add [in LibSepMinimal]
eval_if [in LibSepMinimal]
eval_let [in LibSepMinimal]
eval_app_fix [in LibSepMinimal]
eval_fix [in LibSepMinimal]
eval_val [in LibSepMinimal]
L
Leaf [in Repr]N
Node [in Repr]Q
QuickSort.permut_trans [in Arrays]QuickSort.permut_mid [in Arrays]
QuickSort.sorted_cons [in Arrays]
QuickSort.sorted_one [in Arrays]
QuickSort.sorted_nil [in Arrays]
S
seval_step [in Triples]seval_val [in Triples]
seval_step [in LibSepReference]
seval_val [in LibSepReference]
steps_step [in Triples]
steps_refl [in Triples]
steps_step [in LibSepReference]
steps_refl [in LibSepReference]
step_free [in Triples]
step_set [in Triples]
step_get [in Triples]
step_ref [in Triples]
step_rand [in Triples]
step_div [in Triples]
step_add [in Triples]
step_let [in Triples]
step_seq [in Triples]
step_if [in Triples]
step_app_fix [in Triples]
step_app_fun [in Triples]
step_fix [in Triples]
step_fun [in Triples]
step_let_ctx [in Triples]
step_seq_ctx [in Triples]
step_free [in LibSepReference]
step_set [in LibSepReference]
step_get [in LibSepReference]
step_ref [in LibSepReference]
step_ptr_add [in LibSepReference]
step_gt [in LibSepReference]
step_ge [in LibSepReference]
step_lt [in LibSepReference]
step_le [in LibSepReference]
step_mod [in LibSepReference]
step_div [in LibSepReference]
step_mul [in LibSepReference]
step_sub [in LibSepReference]
step_add [in LibSepReference]
step_neq [in LibSepReference]
step_eq [in LibSepReference]
step_rand [in LibSepReference]
step_opp [in LibSepReference]
step_neg [in LibSepReference]
step_let [in LibSepReference]
step_seq [in LibSepReference]
step_if [in LibSepReference]
step_app_fix [in LibSepReference]
step_app_fun [in LibSepReference]
step_fix [in LibSepReference]
step_fun [in LibSepReference]
step_app_arg2 [in LibSepReference]
step_app_arg1 [in LibSepReference]
step_let_ctx [in LibSepReference]
step_seq_ctx [in LibSepReference]
Syntax.trm_if [in Triples]
Syntax.trm_let [in Triples]
Syntax.trm_seq [in Triples]
Syntax.trm_app [in Triples]
Syntax.trm_fix [in Triples]
Syntax.trm_fun [in Triples]
Syntax.trm_var [in Triples]
Syntax.trm_val [in Triples]
Syntax.val_rand [in Triples]
Syntax.val_div [in Triples]
Syntax.val_add [in Triples]
Syntax.val_free [in Triples]
Syntax.val_set [in Triples]
Syntax.val_get [in Triples]
Syntax.val_ref [in Triples]
Syntax.val_fix [in Triples]
Syntax.val_fun [in Triples]
Syntax.val_loc [in Triples]
Syntax.val_int [in Triples]
Syntax.val_bool [in Triples]
Syntax.val_unit [in Triples]
T
terminates_step [in Triples]terminates_step [in LibSepReference]
tree_sub_2 [in Repr]
tree_sub_1 [in Repr]
trm_if [in LibSepReference]
trm_let [in LibSepReference]
trm_seq [in LibSepReference]
trm_app [in LibSepReference]
trm_fix [in LibSepReference]
trm_fun [in LibSepReference]
trm_var [in LibSepReference]
trm_val [in LibSepReference]
trm_if [in LibSepMinimal]
trm_let [in LibSepMinimal]
trm_app [in LibSepMinimal]
trm_fix [in LibSepMinimal]
trm_var [in LibSepMinimal]
trm_val [in LibSepMinimal]
V
val_error [in LibSepReference]val_uninit [in LibSepReference]
val_fix [in LibSepReference]
val_fun [in LibSepReference]
val_prim [in LibSepReference]
val_loc [in LibSepReference]
val_int [in LibSepReference]
val_bool [in LibSepReference]
val_unit [in LibSepReference]
val_ptr_add [in LibSepReference]
val_gt [in LibSepReference]
val_ge [in LibSepReference]
val_lt [in LibSepReference]
val_le [in LibSepReference]
val_rand [in LibSepReference]
val_mod [in LibSepReference]
val_div [in LibSepReference]
val_mul [in LibSepReference]
val_sub [in LibSepReference]
val_neq [in LibSepReference]
val_add [in LibSepReference]
val_eq [in LibSepReference]
val_opp [in LibSepReference]
val_neg [in LibSepReference]
val_free [in LibSepReference]
val_set [in LibSepReference]
val_get [in LibSepReference]
val_ref [in LibSepReference]
val_fix [in LibSepMinimal]
val_prim [in LibSepMinimal]
val_loc [in LibSepMinimal]
val_int [in LibSepMinimal]
val_bool [in LibSepMinimal]
val_unit [in LibSepMinimal]
val_rand [in LibSepMinimal]
val_div [in LibSepMinimal]
val_add [in LibSepMinimal]
val_free [in LibSepMinimal]
val_set [in LibSepMinimal]
val_get [in LibSepMinimal]
val_ref [in LibSepMinimal]
X
XsimplSetup.xsimpl_hint [in LibSepSimpl]Inductive Index
B
big [in Triples]E
eval [in Triples]eval [in LibSepReference]
eval [in LibSepMinimal]
evalbinop [in LibSepReference]
evalunop [in LibSepReference]
P
prim [in LibSepReference]prim [in LibSepMinimal]
Q
QuickSort.permut [in Arrays]QuickSort.sorted [in Arrays]
S
seval [in Triples]seval [in LibSepReference]
step [in Triples]
step [in LibSepReference]
steps [in Triples]
steps [in LibSepReference]
Syntax.trm [in Triples]
Syntax.val [in Triples]
T
terminates [in Triples]terminates [in LibSepReference]
tree [in Repr]
tree_sub [in Repr]
trm [in LibSepReference]
trm [in LibSepMinimal]
V
val [in LibSepReference]val [in LibSepMinimal]
X
XsimplSetup.Xsimpl_hint [in LibSepSimpl]Projection Index
F
fmap_finite [in LibSepFmap]fmap_data [in LibSepFmap]
Section Index
C
CtxOps [in LibSepReference]E
Eval [in LibSepReference]EvalProp [in LibSepReference]
F
FmapFresh [in LibSepFmap]FmapProp [in LibSepFmap]
M
MapOps [in LibSepFmap]Q
QuickSort.SortedLists [in Arrays]S
StateEq [in LibSepFmap]stepsFrame [in Triples]
T
TexanTriples.WpSpecRef [in WPsem]V
Var_funs_exec [in LibSepReference]Var_seq [in LibSepVar]
Instance Index
I
Inhab_trm [in LibSepReference]Inhab_val [in LibSepReference]
Inhab_fmap [in LibSepFmap]
Inhab_val [in LibSepMinimal]
S
Syntax.Inhab_val [in Triples]Definition Index
A
acclength [in Repr]agree [in LibSepFmap]
aliased_call [in Basic]
append [in Repr]
B
BakedInFrame.btriple [in Triples]BakedInFrame.btriple_lowlevel [in Triples]
BakedInFrame.hoare [in Triples]
big_sind [in Triples]
big_ind [in Triples]
C
conseq [in LibSepFmap]correct [in Triples]
correct [in LibSepReference]
CounterSpec [in Repr]
cps_append [in Repr]
cps_append_aux [in Repr]
cps_facto [in Repr]
cps_facto_aux [in Repr]
create_counter [in Repr]
ctx [in LibSepReference]
ctx [in WPgen]
ctx_equiv [in LibSepReference]
ctx_disjoint [in LibSepReference]
D
DefinitionsForVariables.a [in LibSepVar]DefinitionsForVariables.a1 [in LibSepVar]
DefinitionsForVariables.a2 [in LibSepVar]
DefinitionsForVariables.a3 [in LibSepVar]
DefinitionsForVariables.b [in LibSepVar]
DefinitionsForVariables.b1 [in LibSepVar]
DefinitionsForVariables.b2 [in LibSepVar]
DefinitionsForVariables.b3 [in LibSepVar]
DefinitionsForVariables.c [in LibSepVar]
DefinitionsForVariables.c1 [in LibSepVar]
DefinitionsForVariables.c2 [in LibSepVar]
DefinitionsForVariables.c3 [in LibSepVar]
DefinitionsForVariables.d [in LibSepVar]
DefinitionsForVariables.d1 [in LibSepVar]
DefinitionsForVariables.d2 [in LibSepVar]
DefinitionsForVariables.d3 [in LibSepVar]
DefinitionsForVariables.e [in LibSepVar]
DefinitionsForVariables.e1 [in LibSepVar]
DefinitionsForVariables.e2 [in LibSepVar]
DefinitionsForVariables.e3 [in LibSepVar]
DefinitionsForVariables.f [in LibSepVar]
DefinitionsForVariables.f1 [in LibSepVar]
DefinitionsForVariables.f2 [in LibSepVar]
DefinitionsForVariables.f3 [in LibSepVar]
DefinitionsForVariables.g [in LibSepVar]
DefinitionsForVariables.g1 [in LibSepVar]
DefinitionsForVariables.g2 [in LibSepVar]
DefinitionsForVariables.g3 [in LibSepVar]
DefinitionsForVariables.h [in LibSepVar]
DefinitionsForVariables.h1 [in LibSepVar]
DefinitionsForVariables.h2 [in LibSepVar]
DefinitionsForVariables.h3 [in LibSepVar]
DefinitionsForVariables.i [in LibSepVar]
DefinitionsForVariables.i1 [in LibSepVar]
DefinitionsForVariables.i2 [in LibSepVar]
DefinitionsForVariables.i3 [in LibSepVar]
DefinitionsForVariables.j [in LibSepVar]
DefinitionsForVariables.j1 [in LibSepVar]
DefinitionsForVariables.j2 [in LibSepVar]
DefinitionsForVariables.j3 [in LibSepVar]
DefinitionsForVariables.k [in LibSepVar]
DefinitionsForVariables.k1 [in LibSepVar]
DefinitionsForVariables.k2 [in LibSepVar]
DefinitionsForVariables.k3 [in LibSepVar]
DefinitionsForVariables.l [in LibSepVar]
DefinitionsForVariables.l1 [in LibSepVar]
DefinitionsForVariables.l2 [in LibSepVar]
DefinitionsForVariables.l3 [in LibSepVar]
DefinitionsForVariables.m [in LibSepVar]
DefinitionsForVariables.m1 [in LibSepVar]
DefinitionsForVariables.m2 [in LibSepVar]
DefinitionsForVariables.m3 [in LibSepVar]
DefinitionsForVariables.n [in LibSepVar]
DefinitionsForVariables.n1 [in LibSepVar]
DefinitionsForVariables.n2 [in LibSepVar]
DefinitionsForVariables.n3 [in LibSepVar]
DefinitionsForVariables.o [in LibSepVar]
DefinitionsForVariables.o1 [in LibSepVar]
DefinitionsForVariables.o2 [in LibSepVar]
DefinitionsForVariables.o3 [in LibSepVar]
DefinitionsForVariables.p [in LibSepVar]
DefinitionsForVariables.p1 [in LibSepVar]
DefinitionsForVariables.p2 [in LibSepVar]
DefinitionsForVariables.p3 [in LibSepVar]
DefinitionsForVariables.q [in LibSepVar]
DefinitionsForVariables.q1 [in LibSepVar]
DefinitionsForVariables.q2 [in LibSepVar]
DefinitionsForVariables.q3 [in LibSepVar]
DefinitionsForVariables.r [in LibSepVar]
DefinitionsForVariables.r1 [in LibSepVar]
DefinitionsForVariables.r2 [in LibSepVar]
DefinitionsForVariables.r3 [in LibSepVar]
DefinitionsForVariables.s [in LibSepVar]
DefinitionsForVariables.s1 [in LibSepVar]
DefinitionsForVariables.s2 [in LibSepVar]
DefinitionsForVariables.s3 [in LibSepVar]
DefinitionsForVariables.t [in LibSepVar]
DefinitionsForVariables.t1 [in LibSepVar]
DefinitionsForVariables.t2 [in LibSepVar]
DefinitionsForVariables.t3 [in LibSepVar]
DefinitionsForVariables.u [in LibSepVar]
DefinitionsForVariables.u1 [in LibSepVar]
DefinitionsForVariables.u2 [in LibSepVar]
DefinitionsForVariables.u3 [in LibSepVar]
DefinitionsForVariables.v [in LibSepVar]
DefinitionsForVariables.v1 [in LibSepVar]
DefinitionsForVariables.v2 [in LibSepVar]
DefinitionsForVariables.v3 [in LibSepVar]
DefinitionsForVariables.w [in LibSepVar]
DefinitionsForVariables.w1 [in LibSepVar]
DefinitionsForVariables.w2 [in LibSepVar]
DefinitionsForVariables.w3 [in LibSepVar]
DefinitionsForVariables.x [in LibSepVar]
DefinitionsForVariables.x1 [in LibSepVar]
DefinitionsForVariables.x2 [in LibSepVar]
DefinitionsForVariables.x3 [in LibSepVar]
DefinitionsForVariables.y [in LibSepVar]
DefinitionsForVariables.y1 [in LibSepVar]
DefinitionsForVariables.y2 [in LibSepVar]
DefinitionsForVariables.y3 [in LibSepVar]
DefinitionsForVariables.z [in LibSepVar]
DefinitionsForVariables.z1 [in LibSepVar]
DefinitionsForVariables.z2 [in LibSepVar]
DefinitionsForVariables.z3 [in LibSepVar]
DemoPrograms.decr [in LibSepReference]
DemoPrograms.Def_myfun.myfun [in LibSepReference]
DemoPrograms.Def_myrec.myrec [in LibSepReference]
DemoPrograms.Def_mysucc.mysucc [in LibSepReference]
DemoPrograms.Def_decr.decr [in LibSepReference]
DemoPrograms.Def_incr.incr' [in LibSepReference]
DemoPrograms.incr [in LibSepReference]
DemoPrograms.myfield [in LibSepReference]
DemoPrograms.project_32_rec [in LibSepReference]
DemoPrograms.project_32 [in LibSepReference]
disjoint [in LibSepFmap]
disjoint_3 [in LibSepFmap]
dummy_char [in LibSepVar]
E
empty [in LibSepFmap]evalbinop_sind [in LibSepReference]
evalbinop_ind [in LibSepReference]
evalunop_sind [in LibSepReference]
evalunop_ind [in LibSepReference]
eval_sind [in Triples]
eval_ind [in Triples]
eval_like [in LibSepReference]
eval_sind [in LibSepReference]
eval_ind [in LibSepReference]
eval_sind [in LibSepMinimal]
eval_ind [in LibSepMinimal]
ExampleLocalFunWpgen.incrtwice [in WPgen]
ExampleLocalFunWpgen.succtwice [in WPgen]
ExamplePrograms.incr [in Rules]
ExamplePrograms.incr' [in Rules]
ExamplePrograms.succ_using_incr [in Rules]
ExamplePrograms2.factorec [in Rules]
example_let [in Basic]
F
factoimp [in Basic]factoimp_aux [in Basic]
factorec [in Basic]
field [in LibSepReference]
field [in Records]
filter [in LibSepFmap]
fmap_sind [in LibSepFmap]
fmap_rec [in LibSepFmap]
fmap_ind [in LibSepFmap]
fmap_rect [in LibSepFmap]
formula [in LibSepReference]
formula [in WPgen]
formula_sound [in LibSepReference]
formula_sound [in WPsound]
fresh [in LibSepFmap]
FullyAffineLogic.htop [in Affine]
G
get_and_free [in Basic]H
haffine [in Affine]HaffineQuantifiers.haffine_post [in Affine]
hand [in LibSepReference]
Hand.hand [in Wand]
Hand.hand' [in Wand]
head [in Repr]
head [in Records]
heap [in LibSepReference]
heap [in Hprop]
heap [in LibSepMinimal]
hempty [in Hprop]
hempty [in LibSepMinimal]
hempty' [in Hprop]
hexists [in Hprop]
hexists [in LibSepMinimal]
hfield [in Records]
hfields [in Records]
hfields_update [in LibSepReference]
hfields_lookup [in LibSepReference]
hfields_update [in Records]
hfields_lookup [in Records]
hforall [in LibSepMinimal]
Hforall.hforall [in Wand]
hgc [in Affine]
himpl [in LibSepMinimal]
himpl [in Himpl]
hor [in LibSepReference]
Hor.hor [in Wand]
Hor.hor' [in Wand]
hprop [in Hprop]
hprop [in LibSepMinimal]
hpure [in Hprop]
hpure [in LibSepMinimal]
hpure' [in Hprop]
hrecord [in Records]
hrecord_fields [in LibSepReference]
hrecord_field [in LibSepReference]
hrecord_fields [in Records]
hrecord_field [in Records]
hseg [in Arrays]
hsingle [in Hprop]
hsingle [in LibSepMinimal]
hstar [in Hprop]
hstar [in LibSepMinimal]
HwandEquiv.hwand_characterization_4 [in Wand]
HwandEquiv.hwand_characterization_3 [in Wand]
HwandEquiv.hwand_characterization_2 [in Wand]
HwandEquiv.hwand_characterization_1 [in Wand]
Hwand.hwand [in Wand]
Hwand.hwand' [in Wand]
I
incr [in LibSepMinimal]incr [in Basic]
incr_first [in Basic]
incr_two [in Basic]
indom [in LibSepFmap]
inplace_double [in Basic]
IsCounter [in Repr]
isubst [in LibSepReference]
isubst [in WPgen]
IsubstProp.ctx_disjoint [in WPsound]
IsubstProp.ctx_equiv [in WPsound]
item [in Repr]
L
left [in Repr]loc [in LibSepReference]
loc [in LibSepMinimal]
loc_fresh_gen [in LibSepFmap]
lookup [in LibSepReference]
lookup [in WPgen]
M
map [in LibSepFmap]maps_all_fields [in Records]
map_ [in LibSepFmap]
map_map_finite [in LibSepFmap]
map_filter_finite [in LibSepFmap]
map_remove_finite [in LibSepFmap]
map_map [in LibSepFmap]
map_filter [in LibSepFmap]
map_indom [in LibSepFmap]
map_agree [in LibSepFmap]
map_disjoint [in LibSepFmap]
map_finite [in LibSepFmap]
map_remove [in LibSepFmap]
map_union [in LibSepFmap]
mcons [in Repr]
mcons [in Records]
mcopy [in Repr]
mfree [in Repr]
miter [in Repr]
mkstruct [in LibSepReference]
mkstruct [in WPgen]
mkstruct' [in WPgen]
mlength [in Repr]
mlength_using_miter [in Repr]
mlength' [in Repr]
MList [in Repr]
mnil [in Repr]
mnode [in Repr]
MotivatingExample.succ_using_incr [in Affine]
mrev [in Repr]
mrev_aux [in Repr]
MTree [in Repr]
mtreesum [in Repr]
N
nat_to_var [in LibSepVar]NewTriples.mkstruct [in Affine]
NewTriples.triple [in Affine]
NewTriples.wp [in Affine]
notstuck [in Triples]
notstuck [in LibSepReference]
null [in LibSepReference]
P
Pivot.val_pivot [in Arrays]Pivot.val_array_swap [in Arrays]
prim_sind [in LibSepReference]
prim_rec [in LibSepReference]
prim_ind [in LibSepReference]
prim_rect [in LibSepReference]
prim_sind [in LibSepMinimal]
prim_rec [in LibSepMinimal]
prim_ind [in LibSepMinimal]
prim_rect [in LibSepMinimal]
ProgramSyntax.string_to_var [in LibSepReference]
ProofsSameSemantics.eval_like [in Rules]
purepost [in LibSepReference]
purepostin [in LibSepReference]
Q
qimpl [in LibSepMinimal]qimpl [in Himpl]
quadruple [in Basic]
QuickSort.list_of_le [in Arrays]
QuickSort.list_of_gt [in Arrays]
QuickSort.permut_sind [in Arrays]
QuickSort.permut_ind [in Arrays]
QuickSort.sorted_sind [in Arrays]
QuickSort.sorted_ind [in Arrays]
QuickSort.vals_int [in Arrays]
QuickSort.val_quicksort_full [in Arrays]
QuickSort.val_quicksort [in Arrays]
QwandEquiv.qwand_characterization_5 [in Wand]
QwandEquiv.qwand_characterization_4 [in Wand]
QwandEquiv.qwand_characterization_3 [in Wand]
QwandEquiv.qwand_characterization_2 [in Wand]
QwandEquiv.qwand_characterization_1 [in Wand]
Qwand.qwand [in Wand]
Qwand.qwand' [in Wand]
R
read [in LibSepFmap]Realization.harray [in Arrays]
Realization.hcell [in Arrays]
Realization.hheader [in Arrays]
Realization.hrange [in Arrays]
Realization.hseg [in Arrays]
Realization.val_new_hrecord_2 [in Records]
Realization.val_alloc_hrecord [in Records]
Realization.val_set_field [in Records]
Realization.val_get_field [in Records]
Realization.val_array_make [in Arrays]
Realization.val_array_fill [in Arrays]
Realization.val_array_set [in Arrays]
Realization.val_array_get [in Arrays]
Realization.val_array_length [in Arrays]
reducible [in Triples]
reducible [in LibSepReference]
ref_greater [in Basic]
rem [in LibSepReference]
rem [in WPgen]
remove [in LibSepFmap]
repeat [in Repr]
repeat_incr [in Basic]
right [in Repr]
S
safe [in Triples]safe [in LibSepReference]
SepSimplArgs.haffine [in LibSepReference]
SepSimplArgs.hempty [in LibSepReference]
SepSimplArgs.hexists [in LibSepReference]
SepSimplArgs.hforall [in LibSepReference]
SepSimplArgs.hgc [in LibSepReference]
SepSimplArgs.himpl [in LibSepReference]
SepSimplArgs.hprop [in LibSepReference]
SepSimplArgs.hpure [in LibSepReference]
SepSimplArgs.hsingle [in LibSepReference]
SepSimplArgs.hstar [in LibSepReference]
SepSimplArgs.htop [in LibSepReference]
SepSimplArgs.hwand [in LibSepReference]
SepSimplArgs.qimpl [in LibSepReference]
SepSimplArgs.qwand [in LibSepReference]
seval_sind [in Triples]
seval_ind [in Triples]
seval_sind [in LibSepReference]
seval_ind [in LibSepReference]
single [in LibSepFmap]
SizedStack.create [in Repr]
SizedStack.data [in Repr]
SizedStack.pop [in Repr]
SizedStack.push [in Repr]
SizedStack.size [in Repr]
SizedStack.sizeof [in Repr]
SizedStack.Stack [in Repr]
SizedStack.top [in Repr]
smallest_fresh [in LibSepFmap]
steps_sind [in Triples]
steps_ind [in Triples]
steps_sind [in LibSepReference]
steps_ind [in LibSepReference]
step_sind [in Triples]
step_ind [in Triples]
step_sind [in LibSepReference]
step_ind [in LibSepReference]
step_transfer [in Basic]
striple [in Triples]
subst [in LibSepReference]
subst [in LibSepMinimal]
succ_using_incr [in Basic]
succ_using_incr_attempt [in Basic]
SummaryHprop.hempty [in Wand]
SummaryHprop.hexists [in Wand]
SummaryHprop.hforall [in Wand]
SummaryHprop.hsingle [in Wand]
SummaryHprop.hstar [in Wand]
SummaryHprop.ReaminingOperatorsDerived.hand [in Wand]
SummaryHprop.ReaminingOperatorsDerived.hor [in Wand]
SummaryHprop.ReaminingOperatorsDerived.hpure [in Wand]
SummaryHprop.ReaminingOperatorsDerived.hwand [in Wand]
SummaryHprop.ReaminingOperatorsDerived.qwand [in Wand]
SummaryHprop.ReaminingOperatorsDirect.hand [in Wand]
SummaryHprop.ReaminingOperatorsDirect.hor [in Wand]
SummaryHprop.ReaminingOperatorsDirect.hpure [in Wand]
SummaryHprop.ReaminingOperatorsDirect.hwand [in Wand]
SummaryHprop.ReaminingOperatorsDirect.qwand [in Wand]
Syntax.heap [in Triples]
Syntax.subst [in Triples]
Syntax.trm_sind [in Triples]
Syntax.trm_rec [in Triples]
Syntax.trm_ind [in Triples]
Syntax.trm_rect [in Triples]
Syntax.val_sind [in Triples]
Syntax.val_rec [in Triples]
Syntax.val_ind [in Triples]
Syntax.val_rect [in Triples]
T
tail [in Repr]tail [in Records]
terminates_sind [in Triples]
terminates_ind [in Triples]
terminates_sind [in LibSepReference]
terminates_ind [in LibSepReference]
test_counter [in Repr]
transfer [in Basic]
treeacc [in Repr]
treesum [in Repr]
tree_copy [in Repr]
tree_sub_sind [in Repr]
tree_sub_ind [in Repr]
tree_sind [in Repr]
tree_rec [in Repr]
tree_ind [in Repr]
tree_rect [in Repr]
triple [in Triples]
triple [in LibSepReference]
triple [in LibSepMinimal]
trms [in LibSepReference]
trms_to_vals [in LibSepReference]
trms_vals [in LibSepReference]
trm_is_val [in Triples]
trm_fixs [in LibSepReference]
trm_funs [in LibSepReference]
trm_apps [in LibSepReference]
trm_is_val [in LibSepReference]
trm_sind [in LibSepReference]
trm_rec [in LibSepReference]
trm_ind [in LibSepReference]
trm_rect [in LibSepReference]
trm_sind [in LibSepMinimal]
trm_rec [in LibSepMinimal]
trm_ind [in LibSepMinimal]
trm_rect [in LibSepMinimal]
two_dice [in Basic]
U
union [in LibSepFmap]update [in LibSepFmap]
V
vals [in LibSepReference]val_fixs [in LibSepReference]
val_funs [in LibSepReference]
val_sind [in LibSepReference]
val_rec [in LibSepReference]
val_ind [in LibSepReference]
val_rect [in LibSepReference]
val_sind [in LibSepMinimal]
val_rec [in LibSepMinimal]
val_ind [in LibSepMinimal]
val_rect [in LibSepMinimal]
var [in LibSepVar]
var [in LibSepMinimal]
vars [in LibSepReference]
vars [in LibSepVar]
var_funs_exec [in LibSepReference]
var_funs [in LibSepReference]
var_seq [in LibSepVar]
var_fresh [in LibSepVar]
var_eq [in LibSepVar]
var_eq [in LibSepMinimal]
W
wp [in LibSepReference]wp [in WPsem]
WpFromTriple.wp_1 [in WPsem]
WpFromTriple2.wp_2 [in WPsem]
wpgen [in LibSepReference]
wpgen [in WPgen]
WpgenExec1.wpgen [in WPgen]
WpgenExec2.wpgen [in WPgen]
WPgenRec.ExampleLocalFunWpgenRec.forloop [in WPgen]
WPgenRec.wpgen [in WPgen]
WPgenRec.wpgen_fix [in WPgen]
WPgenRec.wpgen_fun [in WPgen]
WPgenRec.wpgen_fun' [in WPgen]
wpgen_app [in LibSepReference]
wpgen_if_trm [in LibSepReference]
wpgen_if [in LibSepReference]
wpgen_let [in LibSepReference]
wpgen_seq [in LibSepReference]
wpgen_var [in LibSepReference]
wpgen_fix [in LibSepReference]
wpgen_fun [in LibSepReference]
wpgen_val [in LibSepReference]
wpgen_fail [in LibSepReference]
wpgen_app [in WPgen]
wpgen_var [in WPgen]
wpgen_fail [in WPgen]
wpgen_if [in WPgen]
wpgen_let [in WPgen]
wpgen_val [in WPgen]
wpgen_seq [in WPgen]
X
XsimplParams.qimpl [in LibSepSimpl]XsimplSetup.hstars_last [in LibSepSimpl]
XsimplSetup.Id [in LibSepSimpl]
XsimplSetup.protect [in LibSepSimpl]
XsimplSetup.repr [in LibSepSimpl]
XsimplSetup.xchange_hidden [in LibSepSimpl]
XsimplSetup.Xsimpl [in LibSepSimpl]
XsimplSetup.Xsimpl_hint_sind [in LibSepSimpl]
XsimplSetup.Xsimpl_hint_rec [in LibSepSimpl]
XsimplSetup.Xsimpl_hint_ind [in LibSepSimpl]
XsimplSetup.Xsimpl_hint_rect [in LibSepSimpl]
Record Index
F
fmap [in LibSepFmap]| 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 | (2374 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 | (252 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 | (82 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 | (7 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (21 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 | (1040 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 | (200 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 | (215 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 | (27 entries) |
| Projection 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 | (2 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 | (12 entries) |
| Instance 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 | (5 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 | (510 entries) |
| Record 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 | (1 entry) |
This page has been generated by coqdoc