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 (1222 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 (60 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 (84 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 (13 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 (527 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 (233 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 (89 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 (12 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 (2 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 (2 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 (200 entries)

Global Index

A

aliased_call [definition, in SLFBasic]
AlternativeExistentialRule [module, in SLFHimpl]
AlternativeExistentialRule.triple_hexists_of_triple_hexists2 [lemma, in SLFHimpl]
AlternativeExistentialRule.triple_hexists2 [lemma, in SLFHimpl]
Assertions [module, in SLFRich]
Assertions.eval_assert_no_effect [axiom, in SLFRich]
Assertions.eval_assert_disabled [axiom, in SLFRich]
Assertions.eval_assert_enabled [axiom, in SLFRich]
Assertions.hoare_assert [lemma, in SLFRich]
Assertions.triple_assert [lemma, in SLFRich]
Assertions.val_assert [axiom, in SLFRich]


C

ConjDisj [module, in SLFWand]
ConjDisj.hand [definition, in SLFWand]
ConjDisj.hand_comm [lemma, in SLFWand]
ConjDisj.hand_eq_hand' [lemma, in SLFWand]
ConjDisj.hand' [definition, in SLFWand]
ConjDisj.himpl_hand_r [lemma, in SLFWand]
ConjDisj.himpl_hand_l_l [lemma, in SLFWand]
ConjDisj.himpl_hand_l_r [lemma, in SLFWand]
ConjDisj.himpl_hor_l [lemma, in SLFWand]
ConjDisj.himpl_hor_r_l [lemma, in SLFWand]
ConjDisj.himpl_hor_r_r [lemma, in SLFWand]
ConjDisj.hor [definition, in SLFWand]
ConjDisj.hor_comm [lemma, in SLFWand]
ConjDisj.hor_eq_hor' [lemma, in SLFWand]
ConjDisj.hor' [definition, in SLFWand]
ConjDisj.if_neg [lemma, in SLFWand]
ctx [definition, in SLFWPgen]
CurriedFun [module, in SLFRich]
CurriedFun.eval_like_app_fix2 [lemma, in SLFRich]
CurriedFun.eval_app_args [axiom, in SLFRich]
CurriedFun.triple_app_fix2 [lemma, in SLFRich]
CurriedFun.trm_is_val [definition, in SLFRich]
CurriedFun.wp_app_fix2 [lemma, in SLFRich]
CurriedFun.xwp_lemma_fix2 [lemma, in SLFRich]
Fix _ _ _ := _ [notation, in SLFRich]


D

DivSpec [module, in SLFRules]
DivSpec.triple_div'_from_triple_div [lemma, in SLFRules]
DivSpec.triple_div_from_triple_div' [lemma, in SLFRules]
DivSpec.triple_div' [axiom, in SLFRules]
DivSpec.triple_div [axiom, in SLFRules]


E

eval [inductive, in SLFMinimal]
eval_if_trm [axiom, in SLFRich]
eval_free_sep [lemma, in SLFMinimal]
eval_set_sep [lemma, in SLFMinimal]
eval_get_sep [lemma, in SLFMinimal]
eval_ref_sep [lemma, in SLFMinimal]
eval_free [constructor, in SLFMinimal]
eval_set [constructor, in SLFMinimal]
eval_get [constructor, in SLFMinimal]
eval_ref [constructor, in SLFMinimal]
eval_div [constructor, in SLFMinimal]
eval_add [constructor, in SLFMinimal]
eval_if [constructor, in SLFMinimal]
eval_let [constructor, in SLFMinimal]
eval_app [constructor, in SLFMinimal]
eval_fix [constructor, in SLFMinimal]
eval_val [constructor, in SLFMinimal]
ExampleLists [module, in SLFBasic]
ExampleLists.append [definition, in SLFBasic]
ExampleLists.cps_append [definition, in SLFBasic]
ExampleLists.cps_append_aux [definition, in SLFBasic]
ExampleLists.head [definition, in SLFBasic]
ExampleLists.mcons [definition, in SLFBasic]
ExampleLists.mcopy [definition, in SLFBasic]
ExampleLists.MList [definition, in SLFBasic]
ExampleLists.MList_if [lemma, in SLFBasic]
ExampleLists.MList_cons [lemma, in SLFBasic]
ExampleLists.MList_nil [lemma, in SLFBasic]
ExampleLists.mnil [definition, in SLFBasic]
ExampleLists.tail [definition, in SLFBasic]
ExampleLists.Triple_cps_append [lemma, in SLFBasic]
ExampleLists.triple_cps_append_aux [lemma, in SLFBasic]
ExampleLists.triple_mcopy [lemma, in SLFBasic]
ExampleLists.triple_mcons' [lemma, in SLFBasic]
ExampleLists.triple_mcons [lemma, in SLFBasic]
ExampleLists.triple_mnil [lemma, in SLFBasic]
ExampleLists.Triple_append [lemma, in SLFBasic]
ExamplePrograms [module, in SLFRules]
ExamplePrograms.incr [definition, in SLFRules]
ExamplePrograms.incr_eq_incr' [lemma, in SLFRules]
ExamplePrograms.incr' [definition, in SLFRules]
ExamplePrograms.succ_using_incr [definition, in SLFRules]
ExamplePrograms.triple_succ_using_incr [lemma, in SLFRules]
ExamplePrograms.triple_incr [lemma, in SLFRules]
example_let [definition, in SLFBasic]
example_val' [definition, in SLFHprop]
example_val [definition, in SLFHprop]
Extensionality [module, in SLFHprop]
Extensionality.functional_extensionality [axiom, in SLFHprop]
Extensionality.predicate_extensionality_derived [lemma, in SLFHprop]
Extensionality.propositional_extensionality [axiom, in SLFHprop]


F

facto [axiom, in SLFBasic]
factorec [definition, in SLFBasic]
facto_step [axiom, in SLFBasic]
facto_init [axiom, in SLFBasic]
field [definition, in SLFStruct]
formula [definition, in SLFWPgen]
FromPreToPostGC [module, in SLFAffine]
FromPreToPostGC.triple_hgc_post [lemma, in SLFAffine]
FromPreToPostGC.triple_hgc_pre [axiom, in SLFAffine]
FullyAffineLogic [module, in SLFAffine]
FullyAffineLogic.haffine_equiv [lemma, in SLFAffine]
FullyAffineLogic.heap_affine_union [lemma, in SLFAffine]
FullyAffineLogic.heap_affine_empty [lemma, in SLFAffine]
FullyAffineLogic.heap_affine_def [axiom, in SLFAffine]
FullyAffineLogic.hgc_eq_htop [lemma, in SLFAffine]
FullyAffineLogic.htop [definition, in SLFAffine]
FullyLinearLogic [module, in SLFAffine]
FullyLinearLogic.haffine_equiv [lemma, in SLFAffine]
FullyLinearLogic.heap_affine_union [lemma, in SLFAffine]
FullyLinearLogic.heap_affine_empty [lemma, in SLFAffine]
FullyLinearLogic.heap_affine_def [axiom, in SLFAffine]
FullyLinearLogic.hgc_eq_hempty [lemma, in SLFAffine]
functional_extensionality [axiom, in SLFHprop]
functional_extensionality [axiom, in SLFMinimal]
FundamentalProofs [module, in SLFHimpl]
FundamentalProofs.himpl_frame_r [lemma, in SLFHimpl]
FundamentalProofs.himpl_frame_l [lemma, in SLFHimpl]
FundamentalProofs.hprop_op_comm [lemma, in SLFHimpl]
FundamentalProofs.hstar_assoc [lemma, in SLFHimpl]
FundamentalProofs.hstar_hempty_r [lemma, in SLFHimpl]
FundamentalProofs.hstar_hempty_l [lemma, in SLFHimpl]
FundamentalProofs.hstar_comm [lemma, in SLFHimpl]
FundamentalProofs.hstar_hexists [lemma, in SLFHimpl]


H

haffine [definition, in SLFAffine]
HaffineQuantifiers [module, in SLFAffine]
HaffineQuantifiers.haffine_hforall [lemma, in SLFAffine]
HaffineQuantifiers.haffine_hexists [lemma, in SLFAffine]
HaffineQuantifiers.haffine_post [definition, in SLFAffine]
haffine_hgc [lemma, in SLFAffine]
haffine_hstar_hpure_l [lemma, in SLFAffine]
haffine_hforall [lemma, in SLFAffine]
haffine_hexists [lemma, in SLFAffine]
haffine_hstar [lemma, in SLFAffine]
haffine_hpure [lemma, in SLFAffine]
haffine_hempty [lemma, in SLFAffine]
harray [definition, in SLFStruct]
hcells [definition, in SLFStruct]
hcells_concat_eq [axiom, in SLFStruct]
head [definition, in SLFStruct]
heap [definition, in SLFHprop]
heap [definition, in SLFMinimal]
heap_affine_union [axiom, in SLFAffine]
heap_affine_empty [axiom, in SLFAffine]
heap_affine [axiom, in SLFAffine]
hempty [definition, in SLFHprop]
hempty [definition, in SLFMinimal]
hempty_himpl_hgc [lemma, in SLFAffine]
hempty_eq_hpure_true [lemma, in SLFHprop]
hempty_inv [lemma, in SLFHprop]
hempty_intro [lemma, in SLFHprop]
hempty' [definition, in SLFHprop]
hexists [definition, in SLFHprop]
hexists [definition, in SLFMinimal]
hexists_inv [lemma, in SLFHprop]
hexists_intro [lemma, in SLFHprop]
hexists_named_eq [lemma, in SLFHimpl]
hfield [definition, in SLFStruct]
hfields [definition, in SLFStruct]
hfields_update [definition, in SLFStruct]
hfields_lookup [definition, in SLFStruct]
hforall [definition, in SLFMinimal]
hgc [definition, in SLFAffine]
hgc_eq_hgc' [lemma, in SLFAffine]
hgc_inv [lemma, in SLFAffine]
hgc_intro [lemma, in SLFAffine]
hgc' [definition, in SLFAffine]
hheader [axiom, in SLFStruct]
hheader_not_null [axiom, in SLFStruct]
himpl [definition, in SLFMinimal]
himpl [definition, in SLFHimpl]
himpl_hgc_r [lemma, in SLFAffine]
himpl_inv [lemma, in SLFMinimal]
himpl_hforall [lemma, in SLFMinimal]
himpl_hforall_l [lemma, in SLFMinimal]
himpl_hforall_r [lemma, in SLFMinimal]
himpl_hexists [lemma, in SLFMinimal]
himpl_hexists_r [lemma, in SLFMinimal]
himpl_hexists_l [lemma, in SLFMinimal]
himpl_hstar_hpure_l [lemma, in SLFMinimal]
himpl_hstar_hpure_r [lemma, in SLFMinimal]
himpl_frame_r [lemma, in SLFMinimal]
himpl_frame_l [lemma, in SLFMinimal]
himpl_antisym [lemma, in SLFMinimal]
himpl_trans [lemma, in SLFMinimal]
himpl_refl [lemma, in SLFMinimal]
himpl_hstar_hpure_l [lemma, in SLFHimpl]
himpl_hexists_l [lemma, in SLFHimpl]
himpl_frame_lr [lemma, in SLFHimpl]
himpl_frame_l [axiom, in SLFHimpl]
himpl_antisym [lemma, in SLFHimpl]
himpl_trans [lemma, in SLFHimpl]
himpl_refl [lemma, in SLFHimpl]
hoare [definition, in SLFHprop]
hoare [definition, in SLFMinimal]
hoare_if_trm [lemma, in SLFRich]
hoare_free [lemma, in SLFMinimal]
hoare_set [lemma, in SLFMinimal]
hoare_get [lemma, in SLFMinimal]
hoare_ref [lemma, in SLFMinimal]
hoare_div [lemma, in SLFMinimal]
hoare_add [lemma, in SLFMinimal]
hoare_if [lemma, in SLFMinimal]
hoare_let [lemma, in SLFMinimal]
hoare_app [lemma, in SLFMinimal]
hoare_fix [lemma, in SLFMinimal]
hoare_val [lemma, in SLFMinimal]
hoare_hpure [lemma, in SLFMinimal]
hoare_hexists [lemma, in SLFMinimal]
hoare_conseq [lemma, in SLFMinimal]
hoare_named_heap [lemma, in SLFHimpl]
hprop [definition, in SLFHprop]
hprop [definition, in SLFMinimal]
Hprop [module, in SLFSummary]
hprop_eq [lemma, in SLFHprop]
Hprop.hempty [definition, in SLFSummary]
Hprop.hexists [definition, in SLFSummary]
Hprop.himpl [definition, in SLFSummary]
Hprop.himpl_frame_l [axiom, in SLFSummary]
Hprop.himpl_antisym [axiom, in SLFSummary]
Hprop.himpl_trans [axiom, in SLFSummary]
Hprop.himpl_refl [axiom, in SLFSummary]
Hprop.hprop [definition, in SLFSummary]
Hprop.hpure [definition, in SLFSummary]
Hprop.hsingle [definition, in SLFSummary]
Hprop.hstar [definition, in SLFSummary]
Hprop.hstar_hexists [axiom, in SLFSummary]
Hprop.hstar_hempty_l [axiom, in SLFSummary]
Hprop.hstar_comm [axiom, in SLFSummary]
Hprop.hstar_assoc [axiom, in SLFSummary]
Hprop.predicate_extensionality [axiom, in SLFSummary]
_ ==> _ [notation, in SLFSummary]
_ \* _ [notation, in SLFSummary]
_ ~~> _ [notation, in SLFSummary]
\exists _ .. _ , _ [notation, in SLFSummary]
\[ _ ] [notation, in SLFSummary]
\[] [notation, in SLFSummary]
hpure [definition, in SLFHprop]
hpure [definition, in SLFMinimal]
hpure_eq_hexists_proof [lemma, in SLFHprop]
hpure_inv [lemma, in SLFHprop]
hpure_intro [lemma, in SLFHprop]
hpure' [definition, in SLFHprop]
hrecord [definition, in SLFStruct]
hrecord_not_null [lemma, in SLFStruct]
hrecord_fields [definition, in SLFStruct]
hrecord_field [definition, in SLFStruct]
hsingle [definition, in SLFHprop]
hsingle [definition, in SLFMinimal]
hsingle_inv [lemma, in SLFHprop]
hsingle_intro [lemma, in SLFHprop]
hsingle_not_null [lemma, in SLFMinimal]
hstar [definition, in SLFHprop]
hstar [definition, in SLFMinimal]
hstar_hgc_hgc [lemma, in SLFAffine]
hstar_hpure_l [lemma, in SLFHprop]
hstar_inv [lemma, in SLFHprop]
hstar_intro [lemma, in SLFHprop]
hstar_assoc [axiom, in SLFHprop]
hstar_hsingle_same_loc [lemma, in SLFMinimal]
hstar_hpure_l [lemma, in SLFMinimal]
hstar_hempty_r [lemma, in SLFMinimal]
hstar_hforall [lemma, in SLFMinimal]
hstar_hexists [lemma, in SLFMinimal]
hstar_hempty_l [lemma, in SLFMinimal]
hstar_assoc [lemma, in SLFMinimal]
hstar_comm [lemma, in SLFMinimal]
hstar_intro [lemma, in SLFMinimal]
hstar_hsingle_same_loc [lemma, in SLFHimpl]
hstar_hexists [axiom, in SLFHimpl]
hstar_hempty_l [axiom, in SLFHimpl]
hstar_comm [axiom, in SLFHimpl]
hstar_assoc [axiom, in SLFHimpl]
Htactics [module, in SLFHimpl]
Htactics.CaseStudy [module, in SLFHimpl]
Htactics.himpl_example_5 [lemma, in SLFHimpl]
Htactics.himpl_example_4 [lemma, in SLFHimpl]
Htactics.himpl_example_2 [lemma, in SLFHimpl]
Htactics.himpl_example_1 [lemma, in SLFHimpl]
Htactics.qimpl_example_1 [lemma, in SLFHimpl]
Htactics.xchange_demo_inst [lemma, in SLFHimpl]
Htactics.xchange_demo_eq [lemma, in SLFHimpl]
Htactics.xchange_demo_base [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hints_evar [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hints [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists_unify_view [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists_unify [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists [lemma, in SLFHimpl]
Htactics.xsimpl_demo_rhs_hpure [lemma, in SLFHimpl]
Htactics.xsimpl_demo_cancel_all [lemma, in SLFHimpl]
Htactics.xsimpl_demo_cancel_many [lemma, in SLFHimpl]
Htactics.xsimpl_demo_cancel_one [lemma, in SLFHimpl]
Htactics.xsimpl_demo_lhs_several [lemma, in SLFHimpl]
Htactics.xsimpl_demo_lhs_hexists [lemma, in SLFHimpl]
Htactics.xsimpl_demo_lhs_hpure [lemma, in SLFHimpl]
Htactics.xsimpl_demo_lhs_hpure [lemma, in SLFHimpl]
hprop' [notation, in SLFHimpl]
hwand [definition, in SLFSummary]
HwandEquiv [module, in SLFWand]
HwandEquiv.hwand_characterization_3_eq_4 [lemma, in SLFWand]
HwandEquiv.hwand_characterization_2_eq_3 [lemma, in SLFWand]
HwandEquiv.hwand_characterization_1_eq_2 [lemma, in SLFWand]
HwandEquiv.hwand_characterization_4 [definition, in SLFWand]
HwandEquiv.hwand_characterization_3 [definition, in SLFWand]
HwandEquiv.hwand_characterization_2 [definition, in SLFWand]
HwandEquiv.hwand_characterization_1 [definition, in SLFWand]
hwand_elim [axiom, in SLFSummary]


I

incr [definition, in SLFBasic]
incr [axiom, in SLFHprop]
incr [definition, in SLFMinimal]
incr_first [definition, in SLFBasic]
incr_two [definition, in SLFBasic]
incr_applied [lemma, in SLFHprop]
Inhab_val [instance, in SLFMinimal]
inplace_double [definition, in SLFBasic]
isubst [definition, in SLFWPgen]
IsubstProp [module, in SLFWPgen]
IsubstProp.ctx_disjoint_rem [lemma, in SLFWPgen]
IsubstProp.ctx_disjoint [definition, in SLFWPgen]
IsubstProp.ctx_equiv_rem [lemma, in SLFWPgen]
IsubstProp.ctx_equiv [definition, in SLFWPgen]
IsubstProp.isubst_rem_2 [lemma, in SLFWPgen]
IsubstProp.isubst_rem [lemma, in SLFWPgen]
IsubstProp.isubst_app_swap [lemma, in SLFWPgen]
IsubstProp.isubst_app [lemma, in SLFWPgen]
IsubstProp.isubst_ctx_equiv [lemma, in SLFWPgen]
IsubstProp.isubst_nil [lemma, in SLFWPgen]
IsubstProp.lookup_app [lemma, in SLFWPgen]
IsubstProp.lookup_rem [lemma, in SLFWPgen]
IsubstProp.rem_app [lemma, in SLFWPgen]
IsubstProp.subst_eq_isubst_one [lemma, in SLFWPgen]


L

Language [module, in SLFSummary]
Language.loc [definition, in SLFSummary]
Language.trm [inductive, in SLFSummary]
Language.trm_if [constructor, in SLFSummary]
Language.trm_let [constructor, in SLFSummary]
Language.trm_seq [constructor, in SLFSummary]
Language.trm_app [constructor, in SLFSummary]
Language.trm_fix [constructor, in SLFSummary]
Language.trm_fun [constructor, in SLFSummary]
Language.trm_var [constructor, in SLFSummary]
Language.trm_val [constructor, in SLFSummary]
Language.val [inductive, in SLFSummary]
Language.val_add [constructor, in SLFSummary]
Language.val_free [constructor, in SLFSummary]
Language.val_set [constructor, in SLFSummary]
Language.val_get [constructor, in SLFSummary]
Language.val_ref [constructor, in SLFSummary]
Language.val_fix [constructor, in SLFSummary]
Language.val_fun [constructor, in SLFSummary]
Language.val_loc [constructor, in SLFSummary]
Language.val_int [constructor, in SLFSummary]
Language.val_bool [constructor, in SLFSummary]
Language.val_unit [constructor, in SLFSummary]
Language.var [definition, in SLFSummary]
LetFrame [module, in SLFRules]
LetFrame.triple_let_frame [lemma, in SLFRules]
LetFrame.triple_let [axiom, in SLFRules]
ListDealloc [module, in SLFStruct]
ListDealloc.mfree_list [definition, in SLFStruct]
ListDealloc.triple_mfree_list [lemma, in SLFStruct]
loc [definition, in SLFMinimal]
lookup [definition, in SLFWPgen]
LowLevel [module, in SLFAffine]
LowLevel.triple [definition, in SLFAffine]
LowLevel.triple_eq_triple_lowlevel [lemma, in SLFAffine]
LowLevel.triple_lowlevel [definition, in SLFAffine]


M

maps_all_fields [definition, in SLFStruct]
MatchStyle [module, in SLFRules]
MatchStyle.triple_ref' [axiom, in SLFRules]
MatchStyle.triple_ref [axiom, in SLFRules]
max_r [lemma, in SLFBasic]
max_l [lemma, in SLFBasic]
mkstruct [definition, in SLFWPgen]
MkstructGuess [module, in SLFWPgen]
MkstructGuess.mkstruct [definition, in SLFWPgen]
MkstructGuess.mkstruct_introduction [axiom, in SLFWPgen]
MkstructGuess.mkstruct_conseq_idempotence_generalized [axiom, in SLFWPgen]
MkstructGuess.mkstruct_conseq_idempotence [axiom, in SLFWPgen]
MkstructGuess.mkstruct_conseq_frame [axiom, in SLFWPgen]
MkstructGuess.mkstruct_conseq [axiom, in SLFWPgen]
MkstructGuess.mkstruct_frame [axiom, in SLFWPgen]
MkstructProp [module, in SLFWPgen]
MkstructProp.mkstruct [axiom, in SLFWPgen]
MkstructProp.mkstruct_monotone [axiom, in SLFWPgen]
MkstructProp.mkstruct_erase [axiom, in SLFWPgen]
MkstructProp.mkstruct_conseq [axiom, in SLFWPgen]
MkstructProp.mkstruct_frame [axiom, in SLFWPgen]
mkstruct_idempotent [lemma, in SLFWPgen]
mkstruct_wp [lemma, in SLFWPgen]
mkstruct_monotone [lemma, in SLFWPgen]
mkstruct_erase [lemma, in SLFWPgen]
mkstruct_conseq [lemma, in SLFWPgen]
mkstruct_frame [lemma, in SLFWPgen]
MList [definition, in SLFStruct]
MList_if [lemma, in SLFStruct]
MotivatingExample [module, in SLFAffine]
MotivatingExampleSolved [module, in SLFAffine]
MotivatingExampleSolved.triple_succ_using_incr' [lemma, in SLFAffine]
MotivatingExample.succ_using_incr [definition, in SLFAffine]
MotivatingExample.triple_succ_using_incr' [lemma, in SLFAffine]
MotivatingExample.triple_succ_using_incr [lemma, in SLFAffine]


N

NewQwand [module, in SLFWand]
NewQwand.hforall [definition, in SLFWand]
NewQwand.hforall_specialize [lemma, in SLFWand]
NewQwand.hforall_inv [lemma, in SLFWand]
NewQwand.hforall_intro [lemma, in SLFWand]
NewQwand.himpl_qwand_hstar_same_r [lemma, in SLFWand]
NewQwand.himpl_hforall_l [lemma, in SLFWand]
NewQwand.himpl_hforall_r [lemma, in SLFWand]
NewQwand.hstar_qwand [lemma, in SLFWand]
NewQwand.mkstruct [definition, in SLFWand]
NewQwand.mkstruct_frame [lemma, in SLFWand]
NewQwand.mkstruct_conseq [lemma, in SLFWand]
NewQwand.mkstruct_erase [lemma, in SLFWand]
NewQwand.mkstruct' [definition, in SLFWand]
NewQwand.qwand [definition, in SLFWand]
NewQwand.QwandEquiv [module, in SLFWand]
NewQwand.QwandEquiv.hwand_characterization_1_eq_2 [lemma, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_4_eq_5 [lemma, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2_eq_4 [lemma, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2_eq_3 [lemma, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_5 [definition, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_4 [definition, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_3 [definition, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2 [definition, in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_1 [definition, in SLFWand]
NewQwand.qwand_cancel_part [lemma, in SLFWand]
NewQwand.qwand_himpl [lemma, in SLFWand]
NewQwand.qwand_cancel [lemma, in SLFWand]
NewQwand.qwand_equiv [lemma, in SLFWand]
NewQwand.qwand_specialize [lemma, in SLFWand]
NewQwand.triple_hforall [lemma, in SLFWand]
_ \--* _ (qwand_scope) [notation, in SLFWand]
\forall _ .. _ , _ [notation, in SLFWand]
NewTriples [module, in SLFAffine]
NewTriples.GCRules [module, in SLFAffine]
NewTriples.GCRules.triple_ramified_frame_hgc [lemma, in SLFAffine]
NewTriples.GCRules.triple_conseq_frame_hgc [lemma, in SLFAffine]
NewTriples.GCRules.triple_haffine_pre [lemma, in SLFAffine]
NewTriples.GCRules.triple_hgc_post_from_triple_haffine_post [lemma, in SLFAffine]
NewTriples.GCRules.triple_haffine_post [lemma, in SLFAffine]
NewTriples.GCRules.triple_hgc_post [lemma, in SLFAffine]
NewTriples.mkstruct [definition, in SLFAffine]
NewTriples.mkstruct_haffine_pre [lemma, in SLFAffine]
NewTriples.mkstruct_haffine_post [lemma, in SLFAffine]
NewTriples.mkstruct_frame [lemma, in SLFAffine]
NewTriples.mkstruct_conseq [lemma, in SLFAffine]
NewTriples.mkstruct_erase [lemma, in SLFAffine]
NewTriples.mkstruct_hgc [lemma, in SLFAffine]
NewTriples.MotivatingExampleWithUpdatedXwp [module, in SLFAffine]
NewTriples.MotivatingExampleWithUpdatedXwp.haffine_hany [axiom, in SLFAffine]
NewTriples.MotivatingExampleWithUpdatedXwp.triple_succ_using_incr [lemma, in SLFAffine]
NewTriples.triple [definition, in SLFAffine]
NewTriples.triple_seq [lemma, in SLFAffine]
NewTriples.triple_hexists [lemma, in SLFAffine]
NewTriples.triple_hpure [lemma, in SLFAffine]
NewTriples.triple_conseq [lemma, in SLFAffine]
NewTriples.triple_frame [lemma, in SLFAffine]
NewTriples.wp [definition, in SLFAffine]
NewTriples.wp_ramified [lemma, in SLFAffine]
NewTriples.wp_haffine_pre [lemma, in SLFAffine]
NewTriples.wp_hgc_post [lemma, in SLFAffine]
NewTriples.wp_equiv [lemma, in SLFAffine]
NewTriples.xwp_lemma' [lemma, in SLFAffine]
NewTriples.xwp_lemma [axiom, in SLFAffine]
null [definition, in SLFMinimal]


P

Parsing [module, in SLFSummary]
Parsing.mlength [definition, in SLFSummary]
Parsing.mlength' [definition, in SLFSummary]
predicate_extensionality [axiom, in SLFHprop]
Preview [module, in SLFAffine]
Preview.haffine [axiom, in SLFAffine]
Preview.triple_haffine_pre [axiom, in SLFAffine]
Preview.triple_haffine_post [axiom, in SLFAffine]
prim [inductive, in SLFMinimal]
PrimitiveNaryFun [module, in SLFRich]
PrimitiveNaryFun.demo_trms_to_vals [lemma, in SLFRich]
PrimitiveNaryFun.eval_apps_fixs [axiom, in SLFRich]
PrimitiveNaryFun.eval_fixs [axiom, in SLFRich]
PrimitiveNaryFun.NarySyntax [module, in SLFRich]
PrimitiveNaryFun.NarySyntax.apps [inductive, in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_demo [lemma, in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_to_trm [definition, in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_next [constructor, in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_init [constructor, in SLFRich]
PrimitiveNaryFun.NarySyntax.trm [inductive, in SLFRich]
PrimitiveNaryFun.NarySyntax.trm_apps [constructor, in SLFRich]
PrimitiveNaryFun.NarySyntax.trm_val [constructor, in SLFRich]
PrimitiveNaryFun.substn [definition, in SLFRich]
PrimitiveNaryFun.triple_apps_fixs' [lemma, in SLFRich]
PrimitiveNaryFun.triple_apps_fixs [lemma, in SLFRich]
PrimitiveNaryFun.trms [definition, in SLFRich]
PrimitiveNaryFun.trms_to_vals_spec [lemma, in SLFRich]
PrimitiveNaryFun.trms_to_vals [definition, in SLFRich]
PrimitiveNaryFun.trm_apps [axiom, in SLFRich]
PrimitiveNaryFun.trm_fixs [axiom, in SLFRich]
PrimitiveNaryFun.vals [definition, in SLFRich]
PrimitiveNaryFun.val_fixs [axiom, in SLFRich]
PrimitiveNaryFun.vars [definition, in SLFRich]
PrimitiveNaryFun.var_fixs_exec [axiom, in SLFRich]
PrimitiveNaryFun.var_fixs [definition, in SLFRich]
PrimitiveNaryFun.xwp_lemma_fixs [axiom, in SLFRich]
Proofs [module, in SLFRules]
ProofsContinued [module, in SLFRules]
ProofsContinued.eval_free_sep [axiom, in SLFRules]
ProofsContinued.eval_free [axiom, in SLFRules]
ProofsContinued.eval_set_sep [lemma, in SLFRules]
ProofsContinued.eval_set [axiom, in SLFRules]
ProofsContinued.eval_app_fun [axiom, in SLFRules]
ProofsContinued.eval_if [lemma, in SLFRules]
ProofsContinued.hoare_free [lemma, in SLFRules]
ProofsContinued.hoare_set [lemma, in SLFRules]
ProofsContinued.hoare_app_fun [lemma, in SLFRules]
ProofsContinued.hoare_if [lemma, in SLFRules]
ProofsContinued.hoare_if_case [lemma, in SLFRules]
ProofsContinued.triple_free [lemma, in SLFRules]
ProofsContinued.triple_set [lemma, in SLFRules]
ProofsContinued.triple_app_fun [lemma, in SLFRules]
ProofsContinued.triple_if [lemma, in SLFRules]
ProofsContinued.triple_if_case [lemma, in SLFRules]
ProofsFactorization [module, in SLFRules]
ProofsFactorization.triple_add' [lemma, in SLFRules]
ProofsFactorization.triple_of_hoare [lemma, in SLFRules]
ProofsSameSemantics [module, in SLFRules]
ProofsSameSemantics.eval_like_eta_expansion [lemma, in SLFRules]
ProofsSameSemantics.eval_like_eta_reduction [lemma, in SLFRules]
ProofsSameSemantics.eval_like [definition, in SLFRules]
ProofsSameSemantics.hoare_eval_like [lemma, in SLFRules]
ProofsSameSemantics.triple_trm_seq_assoc [lemma, in SLFRules]
ProofsSameSemantics.triple_app_fun [lemma, in SLFRules]
ProofsSameSemantics.triple_trm_equiv [lemma, in SLFRules]
ProofsSameSemantics.triple_eval_like [lemma, in SLFRules]
ProofsSameSemantics.trm_equiv_eta [lemma, in SLFRules]
ProofsSameSemantics.trm_equiv [definition, in SLFRules]
ProofsWithAdvancedXtactics [module, in SLFWPgen]
ProofsWithAdvancedXtactics.triple_succ_using_incr_with_xapps [lemma, in SLFWPgen]
ProofsWithAdvancedXtactics.triple_incr [lemma, in SLFWPgen]
ProofsWithStructuralXtactics [module, in SLFWPgen]
ProofsWithStructuralXtactics.triple_incr_frame [lemma, in SLFWPgen]
ProofsWithXlemmas [module, in SLFWPgen]
ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas [lemma, in SLFWPgen]
ProofsWithXlemmas.triple_incr [lemma, in SLFWPgen]
ProofsWithXtactics [module, in SLFWPgen]
ProofsWithXtactics.triple_succ_using_incr_with_xtactics [lemma, in SLFWPgen]
ProofsWithXtactics.triple_incr [lemma, in SLFWPgen]
Proofs.eval_ref_sep [lemma, in SLFRules]
Proofs.eval_ref [axiom, in SLFRules]
Proofs.eval_get_sep [lemma, in SLFRules]
Proofs.eval_get [axiom, in SLFRules]
Proofs.eval_div' [axiom, in SLFRules]
Proofs.eval_add [axiom, in SLFRules]
Proofs.eval_let [axiom, in SLFRules]
Proofs.eval_seq [axiom, in SLFRules]
Proofs.eval_val [axiom, in SLFRules]
Proofs.exists_not_indom [axiom, in SLFRules]
Proofs.hoare_ref [lemma, in SLFRules]
Proofs.hoare_get [lemma, in SLFRules]
Proofs.hoare_add [lemma, in SLFRules]
Proofs.hoare_seq [lemma, in SLFRules]
Proofs.hoare_val [lemma, in SLFRules]
Proofs.hsingle_inv [axiom, in SLFRules]
Proofs.hstar_hpure_l' [axiom, in SLFRules]
Proofs.hstar_hpure_l [axiom, in SLFRules]
Proofs.single_fresh [lemma, in SLFRules]
Proofs.triple_ref [lemma, in SLFRules]
Proofs.triple_get [lemma, in SLFRules]
Proofs.triple_add [lemma, in SLFRules]
Proofs.triple_seq [lemma, in SLFRules]
Proofs.triple_val [lemma, in SLFRules]
propositional_extensionality [axiom, in SLFMinimal]
ProveAppend [module, in SLFSummary]
ProveAppend.append [definition, in SLFSummary]
ProveAppend.head [definition, in SLFSummary]
ProveAppend.MList [definition, in SLFSummary]
ProveAppend.MList_if [axiom, in SLFSummary]
ProveAppend.MList_cons [lemma, in SLFSummary]
ProveAppend.tail [definition, in SLFSummary]
ProveAppend.Triple_append [lemma, in SLFSummary]
ProveConsequenceRules [module, in SLFHimpl]
ProveConsequenceRules.hoare_conseq [lemma, in SLFHimpl]
ProveConsequenceRules.triple_conseq [lemma, in SLFHimpl]
ProveConsequenceRules.triple_conseq' [lemma, in SLFHimpl]
ProveExtractionRules [module, in SLFHimpl]
ProveExtractionRules.hoare_hexists [lemma, in SLFHimpl]
ProveExtractionRules.hoare_hpure [lemma, in SLFHimpl]
ProveExtractionRules.hpure_encoding [axiom, in SLFHimpl]
ProveExtractionRules.hstar_hexists' [axiom, in SLFHimpl]
ProveExtractionRules.triple_hpure_from_triple_hexists [lemma, in SLFHimpl]
ProveExtractionRules.triple_hexists' [axiom, in SLFHimpl]
ProveExtractionRules.triple_hexists [lemma, in SLFHimpl]
ProveExtractionRules.triple_hpure [lemma, in SLFHimpl]
ProveExtractionRules.triple_hpure' [axiom, in SLFHimpl]
ProveIncr [module, in SLFSummary]
ProveIncrWithTactics [module, in SLFSummary]
ProveIncrWithTactics.incr [definition, in SLFSummary]
ProveIncrWithTactics.triple_incr [lemma, in SLFSummary]
ProveIncr.incr [definition, in SLFSummary]
ProveIncr.incr_eq_incr' [lemma, in SLFSummary]
ProveIncr.incr' [definition, in SLFSummary]
ProveIncr.triple_incr [lemma, in SLFSummary]


Q

qimpl [definition, in SLFMinimal]
qimpl [definition, in SLFHimpl]
qimpl_refl [lemma, in SLFMinimal]
qimpl_antisym [lemma, in SLFHimpl]
qimpl_trans [lemma, in SLFHimpl]
qimpl_refl [lemma, in SLFHimpl]
Qprop [module, in SLFSummary]
qprop_eq [lemma, in SLFHprop]
Qprop.qimpl [definition, in SLFSummary]
_ ===> _ [notation, in SLFSummary]
_ \*+ _ [notation, in SLFSummary]
quadruple [definition, in SLFBasic]
qwand [definition, in SLFSummary]


R

Realization [module, in SLFStruct]
Realization.ArrayAccessDef [module, in SLFStruct]
Realization.ArrayAccessDef.abs_lt_inbound [lemma, in SLFStruct]
Realization.ArrayAccessDef.succ_int_plus_abs [lemma, in SLFStruct]
Realization.ArrayAccessDef.triple_array_set [lemma, in SLFStruct]
Realization.ArrayAccessDef.triple_array_get [lemma, in SLFStruct]
Realization.ArrayAccessDef.triple_array_length [lemma, in SLFStruct]
Realization.ArrayAccessDef.triple_array_length_header [lemma, in SLFStruct]
Realization.ArrayAccessDef.val_array_set [definition, in SLFStruct]
Realization.ArrayAccessDef.val_array_get [definition, in SLFStruct]
Realization.ArrayAccessDef.val_array_length [definition, in SLFStruct]
Realization.eval_length_sep [lemma, in SLFStruct]
Realization.eval_length [axiom, in SLFStruct]
Realization.eval_ptr_add [axiom, in SLFStruct]
Realization.eval_dealloc [axiom, in SLFStruct]
Realization.eval_alloc [axiom, in SLFStruct]
Realization.FieldAccessDef [module, in SLFStruct]
Realization.FieldAccessDef.triple_set_field [lemma, in SLFStruct]
Realization.FieldAccessDef.triple_get_field [lemma, in SLFStruct]
Realization.FieldAccessDef.val_set_field [definition, in SLFStruct]
Realization.FieldAccessDef.val_get_field [definition, in SLFStruct]
_ '. _ [notation, in SLFStruct]
Set _ '. _ ':= _ [notation, in SLFStruct]
Realization.harray_uninit_himpl_hrecord [lemma, in SLFStruct]
Realization.harray_focus [lemma, in SLFStruct]
Realization.harray_inv [lemma, in SLFStruct]
Realization.harray_intro [lemma, in SLFStruct]
Realization.hcells_focus [lemma, in SLFStruct]
Realization.hcells_focus_read [axiom, in SLFStruct]
Realization.hcells_concat_eq [lemma, in SLFStruct]
Realization.hcells_one_eq [lemma, in SLFStruct]
Realization.hcells_cons_eq [lemma, in SLFStruct]
Realization.hcells_nil_eq [lemma, in SLFStruct]
Realization.hcells_inv [lemma, in SLFStruct]
Realization.hcells_intro [lemma, in SLFStruct]
Realization.hfields_eq_hcells [lemma, in SLFStruct]
Realization.hfields_eq_hcells_ind [lemma, in SLFStruct]
Realization.hfields_update_preserves_maps_all_fields [lemma, in SLFStruct]
Realization.hfields_update_preserves_fields [lemma, in SLFStruct]
Realization.hheader_not_null [lemma, in SLFStruct]
Realization.hheader_inv [lemma, in SLFStruct]
Realization.hheader_intro [lemma, in SLFStruct]
Realization.hheader_def [axiom, in SLFStruct]
Realization.hoare_length [lemma, in SLFStruct]
Realization.hoare_ptr_add [lemma, in SLFStruct]
Realization.hoare_dealloc [lemma, in SLFStruct]
Realization.hoare_alloc_nat [lemma, in SLFStruct]
Realization.hrecord_himpl_harray [lemma, in SLFStruct]
Realization.triple_dealloc_hrecord [lemma, in SLFStruct]
Realization.triple_alloc_hrecord [lemma, in SLFStruct]
Realization.triple_set_field_hrecord [lemma, in SLFStruct]
Realization.triple_set_field_hfields [lemma, in SLFStruct]
Realization.triple_get_field_hrecord [lemma, in SLFStruct]
Realization.triple_get_field_hfields [lemma, in SLFStruct]
Realization.triple_length [lemma, in SLFStruct]
Realization.triple_ptr_add_nat [lemma, in SLFStruct]
Realization.triple_ptr_add [lemma, in SLFStruct]
Realization.triple_dealloc [lemma, in SLFStruct]
Realization.triple_alloc_array [lemma, in SLFStruct]
Realization.triple_alloc [lemma, in SLFStruct]
Realization.triple_alloc_nat [lemma, in SLFStruct]
Realization.val_length [axiom, in SLFStruct]
Realization.val_ptr_add [axiom, in SLFStruct]
Realization.val_header [axiom, in SLFStruct]
RecordInit [module, in SLFStruct]
RecordInit.mcons [definition, in SLFStruct]
RecordInit.triple_mcons [lemma, in SLFStruct]
RecordInit.triple_new_hrecord_2 [lemma, in SLFStruct]
RecordInit.val_new_hrecord_2 [definition, in SLFStruct]
New `{ _ := _ ; _ := _ } (trm_scope_ext) [notation, in SLFStruct]
ref_greater [definition, in SLFBasic]
rem [definition, in SLFWPgen]
repeat_incr [definition, in SLFBasic]
Rules [module, in SLFSummary]
Rules.hoare_seq [axiom, in SLFSummary]
Rules.triple_free [axiom, in SLFSummary]
Rules.triple_ref [axiom, in SLFSummary]
Rules.triple_set [axiom, in SLFSummary]
Rules.triple_get [axiom, in SLFSummary]
Rules.triple_seq [axiom, in SLFSummary]
Rules.triple_hexists [axiom, in SLFSummary]
Rules.triple_hpure [axiom, in SLFSummary]
Rules.triple_frame [axiom, in SLFSummary]
Rules.triple_conseq [axiom, in SLFSummary]


S

Semantics [module, in SLFSummary]
Semantics.eval [inductive, in SLFSummary]
Semantics.eval_get [constructor, in SLFSummary]
Semantics.eval_let [constructor, in SLFSummary]
Semantics.eval_val [constructor, in SLFSummary]
Semantics.state [definition, in SLFSummary]
Semantics.subst [axiom, in SLFSummary]
SLFAffine [library]
SLFBasic [library]
SLFHimpl [library]
SLFHprop [library]
SLFMinimal [library]
SLFPreface [library]
SLFRich [library]
SLFRules [library]
SLFStruct [library]
SLFSummary [library]
SLFWand [library]
SLFWPgen [library]
SLFWPsem [library]
state [definition, in SLFHprop]
step_transfer [definition, in SLFBasic]
subst [definition, in SLFMinimal]
succ_using_incr [definition, in SLFBasic]
succ_using_incr_attempt [definition, in SLFBasic]
SummaryHprop [module, in SLFWand]
SummaryHprop.hempty [definition, in SLFWand]
SummaryHprop.hexists [definition, in SLFWand]
SummaryHprop.hforall [definition, in SLFWand]
SummaryHprop.hsingle [definition, in SLFWand]
SummaryHprop.hstar [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived [module, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hand [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hor [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hpure [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hwand [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.qwand [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.qwand' [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect [module, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hand [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hor [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hpure [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hwand [definition, in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.qwand [definition, in SLFWand]
SyntaxAndSemantics [module, in SLFRules]
SyntaxAndSemantics.eval [inductive, in SLFRules]
SyntaxAndSemantics.eval_free [constructor, in SLFRules]
SyntaxAndSemantics.eval_set [constructor, in SLFRules]
SyntaxAndSemantics.eval_get [constructor, in SLFRules]
SyntaxAndSemantics.eval_ref [constructor, in SLFRules]
SyntaxAndSemantics.eval_div [constructor, in SLFRules]
SyntaxAndSemantics.eval_add [constructor, in SLFRules]
SyntaxAndSemantics.eval_if [constructor, in SLFRules]
SyntaxAndSemantics.eval_let [constructor, in SLFRules]
SyntaxAndSemantics.eval_seq [constructor, in SLFRules]
SyntaxAndSemantics.eval_app_fix [constructor, in SLFRules]
SyntaxAndSemantics.eval_app_fun [constructor, in SLFRules]
SyntaxAndSemantics.eval_fix [constructor, in SLFRules]
SyntaxAndSemantics.eval_fun [constructor, in SLFRules]
SyntaxAndSemantics.eval_val [constructor, in SLFRules]
SyntaxAndSemantics.Inhab_val [instance, in SLFRules]
SyntaxAndSemantics.state [definition, in SLFRules]
SyntaxAndSemantics.subst [definition, in SLFRules]
SyntaxAndSemantics.trm [inductive, in SLFRules]
SyntaxAndSemantics.trm_if [constructor, in SLFRules]
SyntaxAndSemantics.trm_let [constructor, in SLFRules]
SyntaxAndSemantics.trm_seq [constructor, in SLFRules]
SyntaxAndSemantics.trm_app [constructor, in SLFRules]
SyntaxAndSemantics.trm_fix [constructor, in SLFRules]
SyntaxAndSemantics.trm_fun [constructor, in SLFRules]
SyntaxAndSemantics.trm_var [constructor, in SLFRules]
SyntaxAndSemantics.trm_val [constructor, in SLFRules]
SyntaxAndSemantics.val [inductive, in SLFRules]
SyntaxAndSemantics.val_div [constructor, in SLFRules]
SyntaxAndSemantics.val_add [constructor, in SLFRules]
SyntaxAndSemantics.val_free [constructor, in SLFRules]
SyntaxAndSemantics.val_set [constructor, in SLFRules]
SyntaxAndSemantics.val_get [constructor, in SLFRules]
SyntaxAndSemantics.val_ref [constructor, in SLFRules]
SyntaxAndSemantics.val_fix [constructor, in SLFRules]
SyntaxAndSemantics.val_fun [constructor, in SLFRules]
SyntaxAndSemantics.val_loc [constructor, in SLFRules]
SyntaxAndSemantics.val_int [constructor, in SLFRules]
SyntaxAndSemantics.val_bool [constructor, in SLFRules]
SyntaxAndSemantics.val_unit [constructor, in SLFRules]


T

tail [definition, in SLFStruct]
TexanTriples [module, in SLFWand]
TexanTriples.incr [axiom, in SLFWand]
TexanTriples.texan_triple_equiv [lemma, in SLFWand]
TexanTriples.triple_incr [axiom, in SLFWand]
TexanTriples.triple_free' [axiom, in SLFWand]
TexanTriples.triple_set' [axiom, in SLFWand]
TexanTriples.triple_ref [axiom, in SLFWand]
TexanTriples.WpSpecRef [section, in SLFWand]
TexanTriples.wp_free' [lemma, in SLFWand]
TexanTriples.wp_set' [lemma, in SLFWand]
TexanTriples.wp_free [lemma, in SLFWand]
TexanTriples.wp_set [lemma, in SLFWand]
TexanTriples.wp_get [lemma, in SLFWand]
TexanTriples.wp_ref_3 [lemma, in SLFWand]
TexanTriples.wp_ref_2 [lemma, in SLFWand]
TexanTriples.wp_ref_1 [lemma, in SLFWand]
TexanTriples.wp_ref_0 [lemma, in SLFWand]
TexanTriples.wp_ref [axiom, in SLFWand]
transfer [definition, in SLFBasic]
triple [definition, in SLFHprop]
triple [definition, in SLFMinimal]
Triple [module, in SLFSummary]
triple_hgc_post [axiom, in SLFAffine]
triple_hany_pre [axiom, in SLFAffine]
triple_hany_post [axiom, in SLFAffine]
triple_app_fun_from_wpgen [axiom, in SLFWPgen]
triple_var' [lemma, in SLFWPgen]
triple_var [lemma, in SLFWPgen]
triple_step_transfer [lemma, in SLFBasic]
triple_repeat_incr' [lemma, in SLFBasic]
triple_repeat_incr_incorrect [lemma, in SLFBasic]
triple_repeat_incr' [lemma, in SLFBasic]
triple_repeat_incr [lemma, in SLFBasic]
triple_factorec' [lemma, in SLFBasic]
triple_factorec [lemma, in SLFBasic]
triple_succ_using_incr [lemma, in SLFBasic]
triple_succ_using_incr_attempt' [lemma, in SLFBasic]
triple_succ_using_incr_attempt [lemma, in SLFBasic]
triple_ref_greater [lemma, in SLFBasic]
triple_ref' [axiom, in SLFBasic]
triple_ref [axiom, in SLFBasic]
triple_incr_first_derived [lemma, in SLFBasic]
triple_incr_first' [lemma, in SLFBasic]
triple_incr_first [lemma, in SLFBasic]
triple_aliased_call [lemma, in SLFBasic]
triple_incr_two_aliased [lemma, in SLFBasic]
triple_aliased_call [lemma, in SLFBasic]
triple_incr_two [lemma, in SLFBasic]
triple_example_let [lemma, in SLFBasic]
triple_incr [lemma, in SLFBasic]
triple_iff_triple_lowlevel [lemma, in SLFHprop]
triple_lowlevel [definition, in SLFHprop]
triple_ref_with_frame [axiom, in SLFHprop]
triple_ref [axiom, in SLFHprop]
triple_incr_3 [axiom, in SLFHprop]
triple_incr_2 [lemma, in SLFHprop]
triple_incr [axiom, in SLFHprop]
triple_frame [lemma, in SLFHprop]
triple_if_trm [lemma, in SLFRich]
triple_dealloc_mcons [lemma, in SLFStruct]
triple_dealloc_hrecord [axiom, in SLFStruct]
triple_alloc_mcons [lemma, in SLFStruct]
triple_alloc_hrecord [axiom, in SLFStruct]
triple_set_field_hrecord [axiom, in SLFStruct]
triple_set_field_hfields [axiom, in SLFStruct]
triple_set_field [axiom, in SLFStruct]
triple_get_field_hrecord [axiom, in SLFStruct]
triple_get_field_hfields [axiom, in SLFStruct]
triple_get_field [axiom, in SLFStruct]
triple_array_length_header [axiom, in SLFStruct]
triple_array_length [axiom, in SLFStruct]
triple_array_set [axiom, in SLFStruct]
triple_array_get [axiom, in SLFStruct]
triple_dealloc [axiom, in SLFStruct]
triple_alloc_array [axiom, in SLFStruct]
triple_alloc [axiom, in SLFStruct]
triple_alloc_nat [axiom, in SLFStruct]
triple_incr [lemma, in SLFMinimal]
triple_free [lemma, in SLFMinimal]
triple_set [lemma, in SLFMinimal]
triple_get [lemma, in SLFMinimal]
triple_ref [lemma, in SLFMinimal]
triple_div [lemma, in SLFMinimal]
triple_add [lemma, in SLFMinimal]
triple_app [lemma, in SLFMinimal]
triple_if [lemma, in SLFMinimal]
triple_let [lemma, in SLFMinimal]
triple_fix [lemma, in SLFMinimal]
triple_val [lemma, in SLFMinimal]
triple_hpure [lemma, in SLFMinimal]
triple_hexists [lemma, in SLFMinimal]
triple_frame [lemma, in SLFMinimal]
triple_conseq [lemma, in SLFMinimal]
triple_ramified_frame [axiom, in SLFSummary]
triple_conseq_frame [axiom, in SLFSummary]
triple_named_heap [lemma, in SLFHimpl]
triple_hexists [axiom, in SLFHimpl]
triple_hpure [axiom, in SLFHimpl]
triple_conseq_frame [lemma, in SLFHimpl]
triple_frame [axiom, in SLFHimpl]
triple_conseq [axiom, in SLFHimpl]
triple_conseq_frame [axiom, in SLFWPsem]
triple_hexists_in_wp [lemma, in SLFWPsem]
triple_hexists [axiom, in SLFWPsem]
triple_app_fun [axiom, in SLFWPsem]
triple_let [axiom, in SLFWPsem]
triple_if [axiom, in SLFWPsem]
triple_fun [axiom, in SLFWPsem]
triple_seq_from_wp_seq [lemma, in SLFWPsem]
triple_seq [axiom, in SLFWPsem]
triple_val_derived_from_wp_val [lemma, in SLFWPsem]
triple_val [axiom, in SLFWPsem]
triple_hpure_with_wp [lemma, in SLFWPsem]
triple_hpure [axiom, in SLFWPsem]
triple_app_fix [axiom, in SLFRules]
triple_fix [axiom, in SLFRules]
triple_val' [lemma, in SLFRules]
triple_val_minimal [lemma, in SLFRules]
triple_hexists [axiom, in SLFRules]
triple_hpure [axiom, in SLFRules]
triple_conseq_frame [axiom, in SLFRules]
triple_conseq [axiom, in SLFRules]
triple_frame [axiom, in SLFRules]
triple_free [axiom, in SLFRules]
triple_ref' [axiom, in SLFRules]
triple_ref [axiom, in SLFRules]
triple_set [axiom, in SLFRules]
triple_get [axiom, in SLFRules]
triple_div' [axiom, in SLFRules]
triple_div [axiom, in SLFRules]
triple_add [axiom, in SLFRules]
triple_app_fun [axiom, in SLFRules]
triple_fun [axiom, in SLFRules]
triple_val [axiom, in SLFRules]
triple_if_case [axiom, in SLFRules]
triple_let [axiom, in SLFRules]
triple_seq [axiom, in SLFRules]
Triple.hoare [definition, in SLFSummary]
Triple.triple [definition, in SLFSummary]
Triple.triple_incr [axiom, in SLFSummary]
trm [inductive, in SLFMinimal]
trm_if [constructor, in SLFMinimal]
trm_let [constructor, in SLFMinimal]
trm_app [constructor, in SLFMinimal]
trm_fix [constructor, in SLFMinimal]
trm_var [constructor, in SLFMinimal]
trm_val [constructor, in SLFMinimal]


V

val [inductive, in SLFMinimal]
val_dealloc_hrecord [definition, in SLFStruct]
val_alloc_hrecord [definition, in SLFStruct]
val_set_field [axiom, in SLFStruct]
val_get_field [axiom, in SLFStruct]
val_array_length [axiom, in SLFStruct]
val_array_set [axiom, in SLFStruct]
val_array_get [axiom, in SLFStruct]
val_dealloc [axiom, in SLFStruct]
val_uninit [axiom, in SLFStruct]
val_alloc [axiom, in SLFStruct]
val_fix [constructor, in SLFMinimal]
val_prim [constructor, in SLFMinimal]
val_loc [constructor, in SLFMinimal]
val_int [constructor, in SLFMinimal]
val_bool [constructor, in SLFMinimal]
val_unit [constructor, in SLFMinimal]
val_div [constructor, in SLFMinimal]
val_add [constructor, in SLFMinimal]
val_free [constructor, in SLFMinimal]
val_set [constructor, in SLFMinimal]
val_get [constructor, in SLFMinimal]
val_ref [constructor, in SLFMinimal]
var [definition, in SLFMinimal]
var_eq [definition, in SLFMinimal]


W

WandBenefits [module, in SLFWand]
WandBenefits.triple_ref_extended' [lemma, in SLFWand]
WandBenefits.triple_ref_extended [lemma, in SLFWand]
WandBenefits.triple_ref [axiom, in SLFWand]
WandBenefits.triple_conseq_frame [axiom, in SLFWand]
WandDef [module, in SLFWand]
WandDef.himpl_hwand_r_inv [lemma, in SLFWand]
WandDef.himpl_hwand_r [lemma, in SLFWand]
WandDef.hwand [definition, in SLFWand]
WandDef.hwand_cancel [lemma, in SLFWand]
WandDef.hwand_equiv [lemma, in SLFWand]
WandDef.hwand' [definition, in SLFWand]
WandDef.qwand [definition, in SLFWand]
WandDef.qwand_specialize [lemma, in SLFWand]
WandDef.qwand_cancel [lemma, in SLFWand]
WandDef.qwand_equiv [lemma, in SLFWand]
WandDef.triple_conseq_frame_of_ramified_frame [lemma, in SLFWand]
WandDef.triple_ramified_frame [lemma, in SLFWand]
WandDef.triple_conseq_frame [axiom, in SLFWand]
WandDef.wp_ramified_trans [lemma, in SLFWand]
WandDef.wp_conseq_frame_of_wp_ramified [lemma, in SLFWand]
WandDef.wp_ramified [lemma, in SLFWand]
WandDef.wp_conseq_frame [axiom, in SLFWand]
_ \--* _ [notation, in SLFWand]
_ \-* _ [notation, in SLFWand]
WandProperties [module, in SLFWand]
WandProperties.himpl_hwand_hstar_same_r [lemma, in SLFWand]
WandProperties.himpl_hwand_hpure_lr [lemma, in SLFWand]
WandProperties.himpl_hwand_hpure_r [lemma, in SLFWand]
WandProperties.himpl_hwand_same_hempty_counterexample [lemma, in SLFWand]
WandProperties.himpl_hempty_hwand_same [lemma, in SLFWand]
WandProperties.hstar_hwand [lemma, in SLFWand]
WandProperties.hwand_cancel_part [lemma, in SLFWand]
WandProperties.hwand_curry_eq [lemma, in SLFWand]
WandProperties.hwand_hpure_l [lemma, in SLFWand]
WandProperties.hwand_hempty_l [lemma, in SLFWand]
WandProperties.hwand_trans_elim [lemma, in SLFWand]
WandProperties.hwand_himpl [lemma, in SLFWand]
WandProperties.not_himpl_hwand_r_inv_reciprocal [lemma, in SLFWand]
WhileLoops [module, in SLFRich]
WhileLoops.DemoLoopFrame [section, in SLFRich]
WhileLoops.eval_while [axiom, in SLFRich]
WhileLoops.hoare_while [lemma, in SLFRich]
WhileLoops.LoopRuleAffine [module, in SLFRich]
WhileLoops.LoopRuleAffine.triple_while_inv_conseq_frame_hgc [lemma, in SLFRich]
WhileLoops.LoopRuleAffine.triple_conseq_frame_hgc [axiom, in SLFRich]
WhileLoops.mkstruct_apply [lemma, in SLFRich]
WhileLoops.mlength_loop [definition, in SLFRich]
WhileLoops.Triple_mlength_loop [lemma, in SLFRich]
WhileLoops.triple_while_inv_conseq_frame [lemma, in SLFRich]
WhileLoops.triple_while_inv [lemma, in SLFRich]
WhileLoops.triple_while_abstract [lemma, in SLFRich]
WhileLoops.triple_while_inv_not_framable [lemma, in SLFRich]
WhileLoops.triple_while [lemma, in SLFRich]
WhileLoops.trm_while [axiom, in SLFRich]
WhileLoops.wpgen_while_sound [lemma, in SLFRich]
WhileLoops.wpgen_while_eq [axiom, in SLFRich]
WhileLoops.wpgen_while [definition, in SLFRich]
WhileLoops.wpgen_if_trm_sound [lemma, in SLFRich]
WhileLoops.wpgen_if_trm [definition, in SLFRich]
WhileLoops.wp_while_inv_conseq [lemma, in SLFRich]
WhileLoops.wp_while [lemma, in SLFRich]
WhileLoops.xwhile_lemma [lemma, in SLFRich]
While _ Do _ Done (trm_scope) [notation, in SLFRich]
While _ Do _ Done (wpgen_scope) [notation, in SLFRich]
If_trm _ Then _ Else _ (wp_scope) [notation, in SLFRich]
wp [axiom, in SLFWPsem]
WpFromHoare [module, in SLFWand]
WpFromHoare [module, in SLFWPsem]
WpFromHoare.wp [definition, in SLFWPsem]
WpFromHoare.wp_ramified [lemma, in SLFWand]
WpFromHoare.wp_app_fix [lemma, in SLFWPsem]
WpFromHoare.wp_app_fun [lemma, in SLFWPsem]
WpFromHoare.wp_let [lemma, in SLFWPsem]
WpFromHoare.wp_seq [lemma, in SLFWPsem]
WpFromHoare.wp_if [lemma, in SLFWPsem]
WpFromHoare.wp_fix [lemma, in SLFWPsem]
WpFromHoare.wp_fun [lemma, in SLFWPsem]
WpFromHoare.wp_val [lemma, in SLFWPsem]
WpFromHoare.wp_conseq_frame [lemma, in SLFWPsem]
WpFromHoare.wp_equiv [lemma, in SLFWPsem]
wpgen [definition, in SLFWPgen]
Wpgen [module, in SLFSummary]
WpgenExec1 [module, in SLFWPgen]
WpgenExec1.triple_incr [lemma, in SLFWPgen]
WpgenExec1.triple_app_fun_from_wpgen [axiom, in SLFWPgen]
WpgenExec1.triple_app_fun [axiom, in SLFWPgen]
WpgenExec1.wpgen [definition, in SLFWPgen]
WpgenExec1.wpgen_sound [axiom, in SLFWPgen]
WpgenExec2 [module, in SLFWPgen]
WpgenExec2.triple_app_fun_from_wpgen [axiom, in SLFWPgen]
WpgenExec2.wpgen [definition, in SLFWPgen]
WpgenExec2.wpgen_sound [axiom, in SLFWPgen]
WPgenRec [module, in SLFWand]
WPgenRec.myfun [definition, in SLFWand]
WPgenRec.triple_myfun' [lemma, in SLFWand]
WPgenRec.triple_myfun [lemma, in SLFWand]
WPgenRec.triple_app_fix_from_wpgen [axiom, in SLFWand]
WPgenRec.triple_app_fun_from_wpgen [axiom, in SLFWand]
WPgenRec.wpgen [definition, in SLFWand]
WPgenRec.wpgen_fix_proof_obligation [lemma, in SLFWand]
WPgenRec.wpgen_fix_sound [lemma, in SLFWand]
WPgenRec.wpgen_fix [definition, in SLFWand]
WPgenRec.wpgen_fun_proof_obligation [lemma, in SLFWand]
WPgenRec.wpgen_fun_sound [lemma, in SLFWand]
WPgenRec.wpgen_fun [definition, in SLFWand]
WPgenRec.xfun_nospec_lemma [lemma, in SLFWand]
WPgenRec.xfun_spec_lemma [lemma, in SLFWand]
Fix' _ _ := _ [notation, in SLFWand]
Fun' _ := _ [notation, in SLFWand]
WPgenSound [module, in SLFWPgen]
WPgenSound.formula_sound [definition, in SLFWPgen]
WPgenSound.isubst_rem [axiom, in SLFWPgen]
WPgenSound.isubst_nil [axiom, in SLFWPgen]
WPgenSound.mkstruct_sound' [lemma, in SLFWPgen]
WPgenSound.mkstruct_sound [lemma, in SLFWPgen]
WPgenSound.triple_app_fix_from_wpgen [lemma, in SLFWPgen]
WPgenSound.triple_app_fun_from_wpgen [lemma, in SLFWPgen]
WPgenSound.triple_of_wpgen [lemma, in SLFWPgen]
WPgenSound.wpgen_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_sound_induct [lemma, in SLFWPgen]
WPgenSound.wpgen_fail_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_if_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_let_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_fix_val_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_fun_val_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_val_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_seq_sound [lemma, in SLFWPgen]
WPgenSound.wpgen_sound_seq' [axiom, in SLFWPgen]
WPgenSound.wpgen_sound_seq [axiom, in SLFWPgen]
WPgenSound.wpgen_sound' [axiom, in SLFWPgen]
WPgenSound.wp_sound [lemma, in SLFWPgen]
WPgenWithMkstruct [module, in SLFWPgen]
WPgenWithMkstruct.triple_incr [lemma, in SLFWPgen]
WPgenWithNotation [module, in SLFWPgen]
WPgenWithNotation.triple_incr [lemma, in SLFWPgen]
wpgen_sound [axiom, in SLFWPgen]
wpgen_var [definition, in SLFWPgen]
wpgen_fail [definition, in SLFWPgen]
wpgen_if [definition, in SLFWPgen]
wpgen_let [definition, in SLFWPgen]
wpgen_val [definition, in SLFWPgen]
wpgen_seq [definition, in SLFWPgen]
Wpgen.formula [definition, in SLFSummary]
Wpgen.mkstruct [definition, in SLFSummary]
Wpgen.mkstruct_conseq [axiom, in SLFSummary]
Wpgen.mkstruct_frame [axiom, in SLFSummary]
Wpgen.mkstruct_erase [axiom, in SLFSummary]
Wpgen.triple_of_wpgen [axiom, in SLFSummary]
Wpgen.wp_equiv [axiom, in SLFSummary]
Wpgen.wp_of_wpgen [axiom, in SLFSummary]
Wpgen.wp_seq [axiom, in SLFSummary]
WpHighLevel [module, in SLFWPsem]
WpHighLevel.wp [definition, in SLFWPsem]
WpHighLevel.wp_equiv [lemma, in SLFWPsem]
WpIfAlt [module, in SLFWPsem]
WpIfAlt.wp_if' [lemma, in SLFWPsem]
WpIfAlt.wp_if [axiom, in SLFWPsem]
WpLowLevel [module, in SLFWPsem]
WpLowLevel.wp [definition, in SLFWPsem]
WpLowLevel.wp_equiv_wp_low [lemma, in SLFWPsem]
Wpsem [module, in SLFSummary]
Wpsem.himpl_hstar_hpure_l [axiom, in SLFSummary]
Wpsem.triple_hpure [axiom, in SLFSummary]
Wpsem.wp [definition, in SLFSummary]
Wpsem.wp_frame [axiom, in SLFSummary]
Wpsem.wp_conseq [axiom, in SLFSummary]
Wpsem.wp_seq [axiom, in SLFSummary]
Wpsem.wp_equiv [axiom, in SLFSummary]
Wpsem.wp_weakest [axiom, in SLFSummary]
Wpsem.wp_pre [axiom, in SLFSummary]
wp_frame [axiom, in SLFWPgen]
wp_if [axiom, in SLFWPgen]
wp_var [lemma, in SLFWPgen]
wp_let [axiom, in SLFWPgen]
wp_seq [axiom, in SLFWPgen]
wp_fun [axiom, in SLFWPgen]
wp_val [axiom, in SLFWPgen]
wp_if_trm [lemma, in SLFRich]
wp_ramified [axiom, in SLFSummary]
wp_conseq_frame [lemma, in SLFWPsem]
wp_conseq_frame_trans [lemma, in SLFWPsem]
wp_from_weakest_pre [lemma, in SLFWPsem]
wp_unique [lemma, in SLFWPsem]
wp_app_fun [lemma, in SLFWPsem]
wp_let [lemma, in SLFWPsem]
wp_if [lemma, in SLFWPsem]
wp_fix [lemma, in SLFWPsem]
wp_fun [lemma, in SLFWPsem]
wp_seq [lemma, in SLFWPsem]
wp_val [lemma, in SLFWPsem]
wp_conseq_trans [lemma, in SLFWPsem]
wp_conseq [lemma, in SLFWPsem]
wp_frame_trans [lemma, in SLFWPsem]
wp_frame [lemma, in SLFWPsem]
wp_weakest [lemma, in SLFWPsem]
wp_pre [lemma, in SLFWPsem]
wp_equiv [axiom, in SLFWPsem]


X

Xaffine [module, in SLFAffine]
Xaffine.xaffine_demo [lemma, in SLFAffine]
xapp_lemma [lemma, in SLFWPgen]
xapp_set_field_lemma [lemma, in SLFStruct]
xapp_get_field_lemma [lemma, in SLFStruct]
xchange_lemma [lemma, in SLFMinimal]
xconseq_lemma [lemma, in SLFWPgen]
xframe_lemma [lemma, in SLFWPgen]
XGC [module, in SLFAffine]
XGC.mkstruct_hgc [axiom, in SLFAffine]
XGC.xgc_keep_demo [lemma, in SLFAffine]
XGC.xgc_post_lemma [lemma, in SLFAffine]
XGC.xgc_keep_demo [lemma, in SLFAffine]
XGC.xgc_demo [lemma, in SLFAffine]
XGC.xgc_lemma [lemma, in SLFAffine]
xlet_lemma [lemma, in SLFWPgen]
xseq_lemma [lemma, in SLFWPgen]
XsimplDemo [module, in SLFWand]
XsimplDemo.xsimpl_demo_qwand_cancel [lemma, in SLFWand]
XsimplDemo.xsimpl_demo_hwand_iter [lemma, in SLFWand]
XsimplDemo.xsimpl_demo_himpl_hwand_r [lemma, in SLFWand]
XsimplDemo.xsimpl_demo_hwand_cancel_partial [lemma, in SLFWand]
XsimplDemo.xsimpl_demo_hwand_cancel [lemma, in SLFWand]
XsimplExtended [module, in SLFAffine]
XsimplExtended.xsimpl_xaffine_demo [lemma, in SLFAffine]
XsimplExtended.xsimpl_xgc_demo [lemma, in SLFAffine]
xstruct_lemma [lemma, in SLFWPgen]
xval_lemma [lemma, in SLFWPgen]
xwp_lemma [lemma, in SLFWPgen]


other

\GC (hgc_scope) [notation, in SLFAffine]
_ ===> _ (hprop_scope) [notation, in SLFMinimal]
_ ==> _ (hprop_scope) [notation, in SLFMinimal]
\forall _ .. _ , _ (hprop_scope) [notation, in SLFMinimal]
\exists _ .. _ , _ (hprop_scope) [notation, in SLFMinimal]
_ \*+ _ (hprop_scope) [notation, in SLFMinimal]
_ \* _ (hprop_scope) [notation, in SLFMinimal]
_ ~~> _ (hprop_scope) [notation, in SLFMinimal]
\[ _ ] (hprop_scope) [notation, in SLFMinimal]
\[] (hprop_scope) [notation, in SLFMinimal]
Delete _ (trm_scope_ext) [notation, in SLFStruct]
Set _ '. _ ':= _ (trm_scope_ext) [notation, in SLFStruct]
_ '. _ (trm_scope_ext) [notation, in SLFStruct]
` _ (wpgen_scope) [notation, in SLFWPgen]
App _ _ (wpgen_scope) [notation, in SLFWPgen]
Fail (wpgen_scope) [notation, in SLFWPgen]
If' _ Then _ Else _ (wpgen_scope) [notation, in SLFWPgen]
Let' _ := _ in _ (wpgen_scope) [notation, in SLFWPgen]
Val _ (wpgen_scope) [notation, in SLFWPgen]
_ \u _ [notation, in SLFHprop]
_ \*+ _ [notation, in SLFHprop]
_ \* _ [notation, in SLFHprop]
_ ~~> _ [notation, in SLFHprop]
_ ~~~> _ [notation, in SLFStruct]
_ `. _ ~~> _ [notation, in SLFStruct]
_ ===> _ [notation, in SLFHimpl]
_ ==> _ [notation, in SLFHimpl]
funloc _ => _ [notation, in SLFBasic]
Seq _ ; _ [notation, in SLFWPgen]
\exists _ .. _ , _ [notation, in SLFHprop]
\[ _ ] [notation, in SLFHprop]
\[] [notation, in SLFHprop]
`{ _ := _ ; _ := _ ; _ := _ } [notation, in SLFStruct]
`{ _ := _ ; _ := _ } [notation, in SLFStruct]
`{ _ := _ } [notation, in SLFStruct]
`{ _ := _ ; _ := _ ; _ := _ } [notation, in SLFStruct]
`{ _ := _ ; _ := _ } [notation, in SLFStruct]
`{ _ := _ } [notation, in SLFStruct]



Notation Index

C

Fix _ _ _ := _ [in SLFRich]


H

_ ==> _ [in SLFSummary]
_ \* _ [in SLFSummary]
_ ~~> _ [in SLFSummary]
\exists _ .. _ , _ [in SLFSummary]
\[ _ ] [in SLFSummary]
\[] [in SLFSummary]
hprop' [in SLFHimpl]


N

_ \--* _ (qwand_scope) [in SLFWand]
\forall _ .. _ , _ [in SLFWand]


Q

_ ===> _ [in SLFSummary]
_ \*+ _ [in SLFSummary]


R

_ '. _ [in SLFStruct]
Set _ '. _ ':= _ [in SLFStruct]
New `{ _ := _ ; _ := _ } (trm_scope_ext) [in SLFStruct]


W

_ \--* _ [in SLFWand]
_ \-* _ [in SLFWand]
While _ Do _ Done (trm_scope) [in SLFRich]
While _ Do _ Done (wpgen_scope) [in SLFRich]
If_trm _ Then _ Else _ (wp_scope) [in SLFRich]
Fix' _ _ := _ [in SLFWand]
Fun' _ := _ [in SLFWand]


other

\GC (hgc_scope) [in SLFAffine]
_ ===> _ (hprop_scope) [in SLFMinimal]
_ ==> _ (hprop_scope) [in SLFMinimal]
\forall _ .. _ , _ (hprop_scope) [in SLFMinimal]
\exists _ .. _ , _ (hprop_scope) [in SLFMinimal]
_ \*+ _ (hprop_scope) [in SLFMinimal]
_ \* _ (hprop_scope) [in SLFMinimal]
_ ~~> _ (hprop_scope) [in SLFMinimal]
\[ _ ] (hprop_scope) [in SLFMinimal]
\[] (hprop_scope) [in SLFMinimal]
Delete _ (trm_scope_ext) [in SLFStruct]
Set _ '. _ ':= _ (trm_scope_ext) [in SLFStruct]
_ '. _ (trm_scope_ext) [in SLFStruct]
` _ (wpgen_scope) [in SLFWPgen]
App _ _ (wpgen_scope) [in SLFWPgen]
Fail (wpgen_scope) [in SLFWPgen]
If' _ Then _ Else _ (wpgen_scope) [in SLFWPgen]
Let' _ := _ in _ (wpgen_scope) [in SLFWPgen]
Val _ (wpgen_scope) [in SLFWPgen]
_ \u _ [in SLFHprop]
_ \*+ _ [in SLFHprop]
_ \* _ [in SLFHprop]
_ ~~> _ [in SLFHprop]
_ ~~~> _ [in SLFStruct]
_ `. _ ~~> _ [in SLFStruct]
_ ===> _ [in SLFHimpl]
_ ==> _ [in SLFHimpl]
funloc _ => _ [in SLFBasic]
Seq _ ; _ [in SLFWPgen]
\exists _ .. _ , _ [in SLFHprop]
\[ _ ] [in SLFHprop]
\[] [in SLFHprop]
`{ _ := _ ; _ := _ ; _ := _ } [in SLFStruct]
`{ _ := _ ; _ := _ } [in SLFStruct]
`{ _ := _ } [in SLFStruct]
`{ _ := _ ; _ := _ ; _ := _ } [in SLFStruct]
`{ _ := _ ; _ := _ } [in SLFStruct]
`{ _ := _ } [in SLFStruct]



Module Index

A

AlternativeExistentialRule [in SLFHimpl]
Assertions [in SLFRich]


C

ConjDisj [in SLFWand]
CurriedFun [in SLFRich]


D

DivSpec [in SLFRules]


E

ExampleLists [in SLFBasic]
ExamplePrograms [in SLFRules]
Extensionality [in SLFHprop]


F

FromPreToPostGC [in SLFAffine]
FullyAffineLogic [in SLFAffine]
FullyLinearLogic [in SLFAffine]
FundamentalProofs [in SLFHimpl]


H

HaffineQuantifiers [in SLFAffine]
Hprop [in SLFSummary]
Htactics [in SLFHimpl]
Htactics.CaseStudy [in SLFHimpl]
HwandEquiv [in SLFWand]


I

IsubstProp [in SLFWPgen]


L

Language [in SLFSummary]
LetFrame [in SLFRules]
ListDealloc [in SLFStruct]
LowLevel [in SLFAffine]


M

MatchStyle [in SLFRules]
MkstructGuess [in SLFWPgen]
MkstructProp [in SLFWPgen]
MotivatingExample [in SLFAffine]
MotivatingExampleSolved [in SLFAffine]


N

NewQwand [in SLFWand]
NewQwand.QwandEquiv [in SLFWand]
NewTriples [in SLFAffine]
NewTriples.GCRules [in SLFAffine]
NewTriples.MotivatingExampleWithUpdatedXwp [in SLFAffine]


P

Parsing [in SLFSummary]
Preview [in SLFAffine]
PrimitiveNaryFun [in SLFRich]
PrimitiveNaryFun.NarySyntax [in SLFRich]
Proofs [in SLFRules]
ProofsContinued [in SLFRules]
ProofsFactorization [in SLFRules]
ProofsSameSemantics [in SLFRules]
ProofsWithAdvancedXtactics [in SLFWPgen]
ProofsWithStructuralXtactics [in SLFWPgen]
ProofsWithXlemmas [in SLFWPgen]
ProofsWithXtactics [in SLFWPgen]
ProveAppend [in SLFSummary]
ProveConsequenceRules [in SLFHimpl]
ProveExtractionRules [in SLFHimpl]
ProveIncr [in SLFSummary]
ProveIncrWithTactics [in SLFSummary]


Q

Qprop [in SLFSummary]


R

Realization [in SLFStruct]
Realization.ArrayAccessDef [in SLFStruct]
Realization.FieldAccessDef [in SLFStruct]
RecordInit [in SLFStruct]
Rules [in SLFSummary]


S

Semantics [in SLFSummary]
SummaryHprop [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect [in SLFWand]
SyntaxAndSemantics [in SLFRules]


T

TexanTriples [in SLFWand]
Triple [in SLFSummary]


W

WandBenefits [in SLFWand]
WandDef [in SLFWand]
WandProperties [in SLFWand]
WhileLoops [in SLFRich]
WhileLoops.LoopRuleAffine [in SLFRich]
WpFromHoare [in SLFWand]
WpFromHoare [in SLFWPsem]
Wpgen [in SLFSummary]
WpgenExec1 [in SLFWPgen]
WpgenExec2 [in SLFWPgen]
WPgenRec [in SLFWand]
WPgenSound [in SLFWPgen]
WPgenWithMkstruct [in SLFWPgen]
WPgenWithNotation [in SLFWPgen]
WpHighLevel [in SLFWPsem]
WpIfAlt [in SLFWPsem]
WpLowLevel [in SLFWPsem]
Wpsem [in SLFSummary]


X

Xaffine [in SLFAffine]
XGC [in SLFAffine]
XsimplDemo [in SLFWand]
XsimplExtended [in SLFAffine]



Library Index

S

SLFAffine
SLFBasic
SLFHimpl
SLFHprop
SLFMinimal
SLFPreface
SLFRich
SLFRules
SLFStruct
SLFSummary
SLFWand
SLFWPgen
SLFWPsem



Lemma Index

A

AlternativeExistentialRule.triple_hexists_of_triple_hexists2 [in SLFHimpl]
AlternativeExistentialRule.triple_hexists2 [in SLFHimpl]
Assertions.hoare_assert [in SLFRich]
Assertions.triple_assert [in SLFRich]


C

ConjDisj.hand_comm [in SLFWand]
ConjDisj.hand_eq_hand' [in SLFWand]
ConjDisj.himpl_hand_r [in SLFWand]
ConjDisj.himpl_hand_l_l [in SLFWand]
ConjDisj.himpl_hand_l_r [in SLFWand]
ConjDisj.himpl_hor_l [in SLFWand]
ConjDisj.himpl_hor_r_l [in SLFWand]
ConjDisj.himpl_hor_r_r [in SLFWand]
ConjDisj.hor_comm [in SLFWand]
ConjDisj.hor_eq_hor' [in SLFWand]
ConjDisj.if_neg [in SLFWand]
CurriedFun.eval_like_app_fix2 [in SLFRich]
CurriedFun.triple_app_fix2 [in SLFRich]
CurriedFun.wp_app_fix2 [in SLFRich]
CurriedFun.xwp_lemma_fix2 [in SLFRich]


D

DivSpec.triple_div'_from_triple_div [in SLFRules]
DivSpec.triple_div_from_triple_div' [in SLFRules]


E

eval_free_sep [in SLFMinimal]
eval_set_sep [in SLFMinimal]
eval_get_sep [in SLFMinimal]
eval_ref_sep [in SLFMinimal]
ExampleLists.MList_if [in SLFBasic]
ExampleLists.MList_cons [in SLFBasic]
ExampleLists.MList_nil [in SLFBasic]
ExampleLists.Triple_cps_append [in SLFBasic]
ExampleLists.triple_cps_append_aux [in SLFBasic]
ExampleLists.triple_mcopy [in SLFBasic]
ExampleLists.triple_mcons' [in SLFBasic]
ExampleLists.triple_mcons [in SLFBasic]
ExampleLists.triple_mnil [in SLFBasic]
ExampleLists.Triple_append [in SLFBasic]
ExamplePrograms.incr_eq_incr' [in SLFRules]
ExamplePrograms.triple_succ_using_incr [in SLFRules]
ExamplePrograms.triple_incr [in SLFRules]
Extensionality.predicate_extensionality_derived [in SLFHprop]


F

FromPreToPostGC.triple_hgc_post [in SLFAffine]
FullyAffineLogic.haffine_equiv [in SLFAffine]
FullyAffineLogic.heap_affine_union [in SLFAffine]
FullyAffineLogic.heap_affine_empty [in SLFAffine]
FullyAffineLogic.hgc_eq_htop [in SLFAffine]
FullyLinearLogic.haffine_equiv [in SLFAffine]
FullyLinearLogic.heap_affine_union [in SLFAffine]
FullyLinearLogic.heap_affine_empty [in SLFAffine]
FullyLinearLogic.hgc_eq_hempty [in SLFAffine]
FundamentalProofs.himpl_frame_r [in SLFHimpl]
FundamentalProofs.himpl_frame_l [in SLFHimpl]
FundamentalProofs.hprop_op_comm [in SLFHimpl]
FundamentalProofs.hstar_assoc [in SLFHimpl]
FundamentalProofs.hstar_hempty_r [in SLFHimpl]
FundamentalProofs.hstar_hempty_l [in SLFHimpl]
FundamentalProofs.hstar_comm [in SLFHimpl]
FundamentalProofs.hstar_hexists [in SLFHimpl]


H

HaffineQuantifiers.haffine_hforall [in SLFAffine]
HaffineQuantifiers.haffine_hexists [in SLFAffine]
haffine_hgc [in SLFAffine]
haffine_hstar_hpure_l [in SLFAffine]
haffine_hforall [in SLFAffine]
haffine_hexists [in SLFAffine]
haffine_hstar [in SLFAffine]
haffine_hpure [in SLFAffine]
haffine_hempty [in SLFAffine]
hempty_himpl_hgc [in SLFAffine]
hempty_eq_hpure_true [in SLFHprop]
hempty_inv [in SLFHprop]
hempty_intro [in SLFHprop]
hexists_inv [in SLFHprop]
hexists_intro [in SLFHprop]
hexists_named_eq [in SLFHimpl]
hgc_eq_hgc' [in SLFAffine]
hgc_inv [in SLFAffine]
hgc_intro [in SLFAffine]
himpl_hgc_r [in SLFAffine]
himpl_inv [in SLFMinimal]
himpl_hforall [in SLFMinimal]
himpl_hforall_l [in SLFMinimal]
himpl_hforall_r [in SLFMinimal]
himpl_hexists [in SLFMinimal]
himpl_hexists_r [in SLFMinimal]
himpl_hexists_l [in SLFMinimal]
himpl_hstar_hpure_l [in SLFMinimal]
himpl_hstar_hpure_r [in SLFMinimal]
himpl_frame_r [in SLFMinimal]
himpl_frame_l [in SLFMinimal]
himpl_antisym [in SLFMinimal]
himpl_trans [in SLFMinimal]
himpl_refl [in SLFMinimal]
himpl_hstar_hpure_l [in SLFHimpl]
himpl_hexists_l [in SLFHimpl]
himpl_frame_lr [in SLFHimpl]
himpl_antisym [in SLFHimpl]
himpl_trans [in SLFHimpl]
himpl_refl [in SLFHimpl]
hoare_if_trm [in SLFRich]
hoare_free [in SLFMinimal]
hoare_set [in SLFMinimal]
hoare_get [in SLFMinimal]
hoare_ref [in SLFMinimal]
hoare_div [in SLFMinimal]
hoare_add [in SLFMinimal]
hoare_if [in SLFMinimal]
hoare_let [in SLFMinimal]
hoare_app [in SLFMinimal]
hoare_fix [in SLFMinimal]
hoare_val [in SLFMinimal]
hoare_hpure [in SLFMinimal]
hoare_hexists [in SLFMinimal]
hoare_conseq [in SLFMinimal]
hoare_named_heap [in SLFHimpl]
hprop_eq [in SLFHprop]
hpure_eq_hexists_proof [in SLFHprop]
hpure_inv [in SLFHprop]
hpure_intro [in SLFHprop]
hrecord_not_null [in SLFStruct]
hsingle_inv [in SLFHprop]
hsingle_intro [in SLFHprop]
hsingle_not_null [in SLFMinimal]
hstar_hgc_hgc [in SLFAffine]
hstar_hpure_l [in SLFHprop]
hstar_inv [in SLFHprop]
hstar_intro [in SLFHprop]
hstar_hsingle_same_loc [in SLFMinimal]
hstar_hpure_l [in SLFMinimal]
hstar_hempty_r [in SLFMinimal]
hstar_hforall [in SLFMinimal]
hstar_hexists [in SLFMinimal]
hstar_hempty_l [in SLFMinimal]
hstar_assoc [in SLFMinimal]
hstar_comm [in SLFMinimal]
hstar_intro [in SLFMinimal]
hstar_hsingle_same_loc [in SLFHimpl]
Htactics.himpl_example_5 [in SLFHimpl]
Htactics.himpl_example_4 [in SLFHimpl]
Htactics.himpl_example_2 [in SLFHimpl]
Htactics.himpl_example_1 [in SLFHimpl]
Htactics.qimpl_example_1 [in SLFHimpl]
Htactics.xchange_demo_inst [in SLFHimpl]
Htactics.xchange_demo_eq [in SLFHimpl]
Htactics.xchange_demo_base [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hints_evar [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hints [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists_unify_view [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists_unify [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hexists [in SLFHimpl]
Htactics.xsimpl_demo_rhs_hpure [in SLFHimpl]
Htactics.xsimpl_demo_cancel_all [in SLFHimpl]
Htactics.xsimpl_demo_cancel_many [in SLFHimpl]
Htactics.xsimpl_demo_cancel_one [in SLFHimpl]
Htactics.xsimpl_demo_lhs_several [in SLFHimpl]
Htactics.xsimpl_demo_lhs_hexists [in SLFHimpl]
Htactics.xsimpl_demo_lhs_hpure [in SLFHimpl]
Htactics.xsimpl_demo_lhs_hpure [in SLFHimpl]
HwandEquiv.hwand_characterization_3_eq_4 [in SLFWand]
HwandEquiv.hwand_characterization_2_eq_3 [in SLFWand]
HwandEquiv.hwand_characterization_1_eq_2 [in SLFWand]


I

incr_applied [in SLFHprop]
IsubstProp.ctx_disjoint_rem [in SLFWPgen]
IsubstProp.ctx_equiv_rem [in SLFWPgen]
IsubstProp.isubst_rem_2 [in SLFWPgen]
IsubstProp.isubst_rem [in SLFWPgen]
IsubstProp.isubst_app_swap [in SLFWPgen]
IsubstProp.isubst_app [in SLFWPgen]
IsubstProp.isubst_ctx_equiv [in SLFWPgen]
IsubstProp.isubst_nil [in SLFWPgen]
IsubstProp.lookup_app [in SLFWPgen]
IsubstProp.lookup_rem [in SLFWPgen]
IsubstProp.rem_app [in SLFWPgen]
IsubstProp.subst_eq_isubst_one [in SLFWPgen]


L

LetFrame.triple_let_frame [in SLFRules]
ListDealloc.triple_mfree_list [in SLFStruct]
LowLevel.triple_eq_triple_lowlevel [in SLFAffine]


M

max_r [in SLFBasic]
max_l [in SLFBasic]
mkstruct_idempotent [in SLFWPgen]
mkstruct_wp [in SLFWPgen]
mkstruct_monotone [in SLFWPgen]
mkstruct_erase [in SLFWPgen]
mkstruct_conseq [in SLFWPgen]
mkstruct_frame [in SLFWPgen]
MList_if [in SLFStruct]
MotivatingExampleSolved.triple_succ_using_incr' [in SLFAffine]
MotivatingExample.triple_succ_using_incr' [in SLFAffine]
MotivatingExample.triple_succ_using_incr [in SLFAffine]


N

NewQwand.hforall_specialize [in SLFWand]
NewQwand.hforall_inv [in SLFWand]
NewQwand.hforall_intro [in SLFWand]
NewQwand.himpl_qwand_hstar_same_r [in SLFWand]
NewQwand.himpl_hforall_l [in SLFWand]
NewQwand.himpl_hforall_r [in SLFWand]
NewQwand.hstar_qwand [in SLFWand]
NewQwand.mkstruct_frame [in SLFWand]
NewQwand.mkstruct_conseq [in SLFWand]
NewQwand.mkstruct_erase [in SLFWand]
NewQwand.QwandEquiv.hwand_characterization_1_eq_2 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_4_eq_5 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2_eq_4 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2_eq_3 [in SLFWand]
NewQwand.qwand_cancel_part [in SLFWand]
NewQwand.qwand_himpl [in SLFWand]
NewQwand.qwand_cancel [in SLFWand]
NewQwand.qwand_equiv [in SLFWand]
NewQwand.qwand_specialize [in SLFWand]
NewQwand.triple_hforall [in SLFWand]
NewTriples.GCRules.triple_ramified_frame_hgc [in SLFAffine]
NewTriples.GCRules.triple_conseq_frame_hgc [in SLFAffine]
NewTriples.GCRules.triple_haffine_pre [in SLFAffine]
NewTriples.GCRules.triple_hgc_post_from_triple_haffine_post [in SLFAffine]
NewTriples.GCRules.triple_haffine_post [in SLFAffine]
NewTriples.GCRules.triple_hgc_post [in SLFAffine]
NewTriples.mkstruct_haffine_pre [in SLFAffine]
NewTriples.mkstruct_haffine_post [in SLFAffine]
NewTriples.mkstruct_frame [in SLFAffine]
NewTriples.mkstruct_conseq [in SLFAffine]
NewTriples.mkstruct_erase [in SLFAffine]
NewTriples.mkstruct_hgc [in SLFAffine]
NewTriples.MotivatingExampleWithUpdatedXwp.triple_succ_using_incr [in SLFAffine]
NewTriples.triple_seq [in SLFAffine]
NewTriples.triple_hexists [in SLFAffine]
NewTriples.triple_hpure [in SLFAffine]
NewTriples.triple_conseq [in SLFAffine]
NewTriples.triple_frame [in SLFAffine]
NewTriples.wp_ramified [in SLFAffine]
NewTriples.wp_haffine_pre [in SLFAffine]
NewTriples.wp_hgc_post [in SLFAffine]
NewTriples.wp_equiv [in SLFAffine]
NewTriples.xwp_lemma' [in SLFAffine]


P

PrimitiveNaryFun.demo_trms_to_vals [in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_demo [in SLFRich]
PrimitiveNaryFun.triple_apps_fixs' [in SLFRich]
PrimitiveNaryFun.triple_apps_fixs [in SLFRich]
PrimitiveNaryFun.trms_to_vals_spec [in SLFRich]
ProofsContinued.eval_set_sep [in SLFRules]
ProofsContinued.eval_if [in SLFRules]
ProofsContinued.hoare_free [in SLFRules]
ProofsContinued.hoare_set [in SLFRules]
ProofsContinued.hoare_app_fun [in SLFRules]
ProofsContinued.hoare_if [in SLFRules]
ProofsContinued.hoare_if_case [in SLFRules]
ProofsContinued.triple_free [in SLFRules]
ProofsContinued.triple_set [in SLFRules]
ProofsContinued.triple_app_fun [in SLFRules]
ProofsContinued.triple_if [in SLFRules]
ProofsContinued.triple_if_case [in SLFRules]
ProofsFactorization.triple_add' [in SLFRules]
ProofsFactorization.triple_of_hoare [in SLFRules]
ProofsSameSemantics.eval_like_eta_expansion [in SLFRules]
ProofsSameSemantics.eval_like_eta_reduction [in SLFRules]
ProofsSameSemantics.hoare_eval_like [in SLFRules]
ProofsSameSemantics.triple_trm_seq_assoc [in SLFRules]
ProofsSameSemantics.triple_app_fun [in SLFRules]
ProofsSameSemantics.triple_trm_equiv [in SLFRules]
ProofsSameSemantics.triple_eval_like [in SLFRules]
ProofsSameSemantics.trm_equiv_eta [in SLFRules]
ProofsWithAdvancedXtactics.triple_succ_using_incr_with_xapps [in SLFWPgen]
ProofsWithAdvancedXtactics.triple_incr [in SLFWPgen]
ProofsWithStructuralXtactics.triple_incr_frame [in SLFWPgen]
ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas [in SLFWPgen]
ProofsWithXlemmas.triple_incr [in SLFWPgen]
ProofsWithXtactics.triple_succ_using_incr_with_xtactics [in SLFWPgen]
ProofsWithXtactics.triple_incr [in SLFWPgen]
Proofs.eval_ref_sep [in SLFRules]
Proofs.eval_get_sep [in SLFRules]
Proofs.hoare_ref [in SLFRules]
Proofs.hoare_get [in SLFRules]
Proofs.hoare_add [in SLFRules]
Proofs.hoare_seq [in SLFRules]
Proofs.hoare_val [in SLFRules]
Proofs.single_fresh [in SLFRules]
Proofs.triple_ref [in SLFRules]
Proofs.triple_get [in SLFRules]
Proofs.triple_add [in SLFRules]
Proofs.triple_seq [in SLFRules]
Proofs.triple_val [in SLFRules]
ProveAppend.MList_cons [in SLFSummary]
ProveAppend.Triple_append [in SLFSummary]
ProveConsequenceRules.hoare_conseq [in SLFHimpl]
ProveConsequenceRules.triple_conseq [in SLFHimpl]
ProveConsequenceRules.triple_conseq' [in SLFHimpl]
ProveExtractionRules.hoare_hexists [in SLFHimpl]
ProveExtractionRules.hoare_hpure [in SLFHimpl]
ProveExtractionRules.triple_hpure_from_triple_hexists [in SLFHimpl]
ProveExtractionRules.triple_hexists [in SLFHimpl]
ProveExtractionRules.triple_hpure [in SLFHimpl]
ProveIncrWithTactics.triple_incr [in SLFSummary]
ProveIncr.incr_eq_incr' [in SLFSummary]
ProveIncr.triple_incr [in SLFSummary]


Q

qimpl_refl [in SLFMinimal]
qimpl_antisym [in SLFHimpl]
qimpl_trans [in SLFHimpl]
qimpl_refl [in SLFHimpl]
qprop_eq [in SLFHprop]


R

Realization.ArrayAccessDef.abs_lt_inbound [in SLFStruct]
Realization.ArrayAccessDef.succ_int_plus_abs [in SLFStruct]
Realization.ArrayAccessDef.triple_array_set [in SLFStruct]
Realization.ArrayAccessDef.triple_array_get [in SLFStruct]
Realization.ArrayAccessDef.triple_array_length [in SLFStruct]
Realization.ArrayAccessDef.triple_array_length_header [in SLFStruct]
Realization.eval_length_sep [in SLFStruct]
Realization.FieldAccessDef.triple_set_field [in SLFStruct]
Realization.FieldAccessDef.triple_get_field [in SLFStruct]
Realization.harray_uninit_himpl_hrecord [in SLFStruct]
Realization.harray_focus [in SLFStruct]
Realization.harray_inv [in SLFStruct]
Realization.harray_intro [in SLFStruct]
Realization.hcells_focus [in SLFStruct]
Realization.hcells_concat_eq [in SLFStruct]
Realization.hcells_one_eq [in SLFStruct]
Realization.hcells_cons_eq [in SLFStruct]
Realization.hcells_nil_eq [in SLFStruct]
Realization.hcells_inv [in SLFStruct]
Realization.hcells_intro [in SLFStruct]
Realization.hfields_eq_hcells [in SLFStruct]
Realization.hfields_eq_hcells_ind [in SLFStruct]
Realization.hfields_update_preserves_maps_all_fields [in SLFStruct]
Realization.hfields_update_preserves_fields [in SLFStruct]
Realization.hheader_not_null [in SLFStruct]
Realization.hheader_inv [in SLFStruct]
Realization.hheader_intro [in SLFStruct]
Realization.hoare_length [in SLFStruct]
Realization.hoare_ptr_add [in SLFStruct]
Realization.hoare_dealloc [in SLFStruct]
Realization.hoare_alloc_nat [in SLFStruct]
Realization.hrecord_himpl_harray [in SLFStruct]
Realization.triple_dealloc_hrecord [in SLFStruct]
Realization.triple_alloc_hrecord [in SLFStruct]
Realization.triple_set_field_hrecord [in SLFStruct]
Realization.triple_set_field_hfields [in SLFStruct]
Realization.triple_get_field_hrecord [in SLFStruct]
Realization.triple_get_field_hfields [in SLFStruct]
Realization.triple_length [in SLFStruct]
Realization.triple_ptr_add_nat [in SLFStruct]
Realization.triple_ptr_add [in SLFStruct]
Realization.triple_dealloc [in SLFStruct]
Realization.triple_alloc_array [in SLFStruct]
Realization.triple_alloc [in SLFStruct]
Realization.triple_alloc_nat [in SLFStruct]
RecordInit.triple_mcons [in SLFStruct]
RecordInit.triple_new_hrecord_2 [in SLFStruct]


T

TexanTriples.texan_triple_equiv [in SLFWand]
TexanTriples.wp_free' [in SLFWand]
TexanTriples.wp_set' [in SLFWand]
TexanTriples.wp_free [in SLFWand]
TexanTriples.wp_set [in SLFWand]
TexanTriples.wp_get [in SLFWand]
TexanTriples.wp_ref_3 [in SLFWand]
TexanTriples.wp_ref_2 [in SLFWand]
TexanTriples.wp_ref_1 [in SLFWand]
TexanTriples.wp_ref_0 [in SLFWand]
triple_var' [in SLFWPgen]
triple_var [in SLFWPgen]
triple_step_transfer [in SLFBasic]
triple_repeat_incr' [in SLFBasic]
triple_repeat_incr_incorrect [in SLFBasic]
triple_repeat_incr' [in SLFBasic]
triple_repeat_incr [in SLFBasic]
triple_factorec' [in SLFBasic]
triple_factorec [in SLFBasic]
triple_succ_using_incr [in SLFBasic]
triple_succ_using_incr_attempt' [in SLFBasic]
triple_succ_using_incr_attempt [in SLFBasic]
triple_ref_greater [in SLFBasic]
triple_incr_first_derived [in SLFBasic]
triple_incr_first' [in SLFBasic]
triple_incr_first [in SLFBasic]
triple_aliased_call [in SLFBasic]
triple_incr_two_aliased [in SLFBasic]
triple_aliased_call [in SLFBasic]
triple_incr_two [in SLFBasic]
triple_example_let [in SLFBasic]
triple_incr [in SLFBasic]
triple_iff_triple_lowlevel [in SLFHprop]
triple_incr_2 [in SLFHprop]
triple_frame [in SLFHprop]
triple_if_trm [in SLFRich]
triple_dealloc_mcons [in SLFStruct]
triple_alloc_mcons [in SLFStruct]
triple_incr [in SLFMinimal]
triple_free [in SLFMinimal]
triple_set [in SLFMinimal]
triple_get [in SLFMinimal]
triple_ref [in SLFMinimal]
triple_div [in SLFMinimal]
triple_add [in SLFMinimal]
triple_app [in SLFMinimal]
triple_if [in SLFMinimal]
triple_let [in SLFMinimal]
triple_fix [in SLFMinimal]
triple_val [in SLFMinimal]
triple_hpure [in SLFMinimal]
triple_hexists [in SLFMinimal]
triple_frame [in SLFMinimal]
triple_conseq [in SLFMinimal]
triple_named_heap [in SLFHimpl]
triple_conseq_frame [in SLFHimpl]
triple_hexists_in_wp [in SLFWPsem]
triple_seq_from_wp_seq [in SLFWPsem]
triple_val_derived_from_wp_val [in SLFWPsem]
triple_hpure_with_wp [in SLFWPsem]
triple_val' [in SLFRules]
triple_val_minimal [in SLFRules]


W

WandBenefits.triple_ref_extended' [in SLFWand]
WandBenefits.triple_ref_extended [in SLFWand]
WandDef.himpl_hwand_r_inv [in SLFWand]
WandDef.himpl_hwand_r [in SLFWand]
WandDef.hwand_cancel [in SLFWand]
WandDef.hwand_equiv [in SLFWand]
WandDef.qwand_specialize [in SLFWand]
WandDef.qwand_cancel [in SLFWand]
WandDef.qwand_equiv [in SLFWand]
WandDef.triple_conseq_frame_of_ramified_frame [in SLFWand]
WandDef.triple_ramified_frame [in SLFWand]
WandDef.wp_ramified_trans [in SLFWand]
WandDef.wp_conseq_frame_of_wp_ramified [in SLFWand]
WandDef.wp_ramified [in SLFWand]
WandProperties.himpl_hwand_hstar_same_r [in SLFWand]
WandProperties.himpl_hwand_hpure_lr [in SLFWand]
WandProperties.himpl_hwand_hpure_r [in SLFWand]
WandProperties.himpl_hwand_same_hempty_counterexample [in SLFWand]
WandProperties.himpl_hempty_hwand_same [in SLFWand]
WandProperties.hstar_hwand [in SLFWand]
WandProperties.hwand_cancel_part [in SLFWand]
WandProperties.hwand_curry_eq [in SLFWand]
WandProperties.hwand_hpure_l [in SLFWand]
WandProperties.hwand_hempty_l [in SLFWand]
WandProperties.hwand_trans_elim [in SLFWand]
WandProperties.hwand_himpl [in SLFWand]
WandProperties.not_himpl_hwand_r_inv_reciprocal [in SLFWand]
WhileLoops.hoare_while [in SLFRich]
WhileLoops.LoopRuleAffine.triple_while_inv_conseq_frame_hgc [in SLFRich]
WhileLoops.mkstruct_apply [in SLFRich]
WhileLoops.Triple_mlength_loop [in SLFRich]
WhileLoops.triple_while_inv_conseq_frame [in SLFRich]
WhileLoops.triple_while_inv [in SLFRich]
WhileLoops.triple_while_abstract [in SLFRich]
WhileLoops.triple_while_inv_not_framable [in SLFRich]
WhileLoops.triple_while [in SLFRich]
WhileLoops.wpgen_while_sound [in SLFRich]
WhileLoops.wpgen_if_trm_sound [in SLFRich]
WhileLoops.wp_while_inv_conseq [in SLFRich]
WhileLoops.wp_while [in SLFRich]
WhileLoops.xwhile_lemma [in SLFRich]
WpFromHoare.wp_ramified [in SLFWand]
WpFromHoare.wp_app_fix [in SLFWPsem]
WpFromHoare.wp_app_fun [in SLFWPsem]
WpFromHoare.wp_let [in SLFWPsem]
WpFromHoare.wp_seq [in SLFWPsem]
WpFromHoare.wp_if [in SLFWPsem]
WpFromHoare.wp_fix [in SLFWPsem]
WpFromHoare.wp_fun [in SLFWPsem]
WpFromHoare.wp_val [in SLFWPsem]
WpFromHoare.wp_conseq_frame [in SLFWPsem]
WpFromHoare.wp_equiv [in SLFWPsem]
WpgenExec1.triple_incr [in SLFWPgen]
WPgenRec.triple_myfun' [in SLFWand]
WPgenRec.triple_myfun [in SLFWand]
WPgenRec.wpgen_fix_proof_obligation [in SLFWand]
WPgenRec.wpgen_fix_sound [in SLFWand]
WPgenRec.wpgen_fun_proof_obligation [in SLFWand]
WPgenRec.wpgen_fun_sound [in SLFWand]
WPgenRec.xfun_nospec_lemma [in SLFWand]
WPgenRec.xfun_spec_lemma [in SLFWand]
WPgenSound.mkstruct_sound' [in SLFWPgen]
WPgenSound.mkstruct_sound [in SLFWPgen]
WPgenSound.triple_app_fix_from_wpgen [in SLFWPgen]
WPgenSound.triple_app_fun_from_wpgen [in SLFWPgen]
WPgenSound.triple_of_wpgen [in SLFWPgen]
WPgenSound.wpgen_sound [in SLFWPgen]
WPgenSound.wpgen_sound_induct [in SLFWPgen]
WPgenSound.wpgen_fail_sound [in SLFWPgen]
WPgenSound.wpgen_if_sound [in SLFWPgen]
WPgenSound.wpgen_let_sound [in SLFWPgen]
WPgenSound.wpgen_fix_val_sound [in SLFWPgen]
WPgenSound.wpgen_fun_val_sound [in SLFWPgen]
WPgenSound.wpgen_val_sound [in SLFWPgen]
WPgenSound.wpgen_seq_sound [in SLFWPgen]
WPgenSound.wp_sound [in SLFWPgen]
WPgenWithMkstruct.triple_incr [in SLFWPgen]
WPgenWithNotation.triple_incr [in SLFWPgen]
WpHighLevel.wp_equiv [in SLFWPsem]
WpIfAlt.wp_if' [in SLFWPsem]
WpLowLevel.wp_equiv_wp_low [in SLFWPsem]
wp_var [in SLFWPgen]
wp_if_trm [in SLFRich]
wp_conseq_frame [in SLFWPsem]
wp_conseq_frame_trans [in SLFWPsem]
wp_from_weakest_pre [in SLFWPsem]
wp_unique [in SLFWPsem]
wp_app_fun [in SLFWPsem]
wp_let [in SLFWPsem]
wp_if [in SLFWPsem]
wp_fix [in SLFWPsem]
wp_fun [in SLFWPsem]
wp_seq [in SLFWPsem]
wp_val [in SLFWPsem]
wp_conseq_trans [in SLFWPsem]
wp_conseq [in SLFWPsem]
wp_frame_trans [in SLFWPsem]
wp_frame [in SLFWPsem]
wp_weakest [in SLFWPsem]
wp_pre [in SLFWPsem]


X

Xaffine.xaffine_demo [in SLFAffine]
xapp_lemma [in SLFWPgen]
xapp_set_field_lemma [in SLFStruct]
xapp_get_field_lemma [in SLFStruct]
xchange_lemma [in SLFMinimal]
xconseq_lemma [in SLFWPgen]
xframe_lemma [in SLFWPgen]
XGC.xgc_keep_demo [in SLFAffine]
XGC.xgc_post_lemma [in SLFAffine]
XGC.xgc_keep_demo [in SLFAffine]
XGC.xgc_demo [in SLFAffine]
XGC.xgc_lemma [in SLFAffine]
xlet_lemma [in SLFWPgen]
xseq_lemma [in SLFWPgen]
XsimplDemo.xsimpl_demo_qwand_cancel [in SLFWand]
XsimplDemo.xsimpl_demo_hwand_iter [in SLFWand]
XsimplDemo.xsimpl_demo_himpl_hwand_r [in SLFWand]
XsimplDemo.xsimpl_demo_hwand_cancel_partial [in SLFWand]
XsimplDemo.xsimpl_demo_hwand_cancel [in SLFWand]
XsimplExtended.xsimpl_xaffine_demo [in SLFAffine]
XsimplExtended.xsimpl_xgc_demo [in SLFAffine]
xstruct_lemma [in SLFWPgen]
xval_lemma [in SLFWPgen]
xwp_lemma [in SLFWPgen]



Axiom Index

A

Assertions.eval_assert_no_effect [in SLFRich]
Assertions.eval_assert_disabled [in SLFRich]
Assertions.eval_assert_enabled [in SLFRich]
Assertions.val_assert [in SLFRich]


C

CurriedFun.eval_app_args [in SLFRich]


D

DivSpec.triple_div' [in SLFRules]
DivSpec.triple_div [in SLFRules]


E

eval_if_trm [in SLFRich]
Extensionality.functional_extensionality [in SLFHprop]
Extensionality.propositional_extensionality [in SLFHprop]


F

facto [in SLFBasic]
facto_step [in SLFBasic]
facto_init [in SLFBasic]
FromPreToPostGC.triple_hgc_pre [in SLFAffine]
FullyAffineLogic.heap_affine_def [in SLFAffine]
FullyLinearLogic.heap_affine_def [in SLFAffine]
functional_extensionality [in SLFHprop]
functional_extensionality [in SLFMinimal]


H

hcells_concat_eq [in SLFStruct]
heap_affine_union [in SLFAffine]
heap_affine_empty [in SLFAffine]
heap_affine [in SLFAffine]
hheader [in SLFStruct]
hheader_not_null [in SLFStruct]
himpl_frame_l [in SLFHimpl]
Hprop.himpl_frame_l [in SLFSummary]
Hprop.himpl_antisym [in SLFSummary]
Hprop.himpl_trans [in SLFSummary]
Hprop.himpl_refl [in SLFSummary]
Hprop.hstar_hexists [in SLFSummary]
Hprop.hstar_hempty_l [in SLFSummary]
Hprop.hstar_comm [in SLFSummary]
Hprop.hstar_assoc [in SLFSummary]
Hprop.predicate_extensionality [in SLFSummary]
hstar_assoc [in SLFHprop]
hstar_hexists [in SLFHimpl]
hstar_hempty_l [in SLFHimpl]
hstar_comm [in SLFHimpl]
hstar_assoc [in SLFHimpl]
hwand_elim [in SLFSummary]


I

incr [in SLFHprop]


L

LetFrame.triple_let [in SLFRules]


M

MatchStyle.triple_ref' [in SLFRules]
MatchStyle.triple_ref [in SLFRules]
MkstructGuess.mkstruct_introduction [in SLFWPgen]
MkstructGuess.mkstruct_conseq_idempotence_generalized [in SLFWPgen]
MkstructGuess.mkstruct_conseq_idempotence [in SLFWPgen]
MkstructGuess.mkstruct_conseq_frame [in SLFWPgen]
MkstructGuess.mkstruct_conseq [in SLFWPgen]
MkstructGuess.mkstruct_frame [in SLFWPgen]
MkstructProp.mkstruct [in SLFWPgen]
MkstructProp.mkstruct_monotone [in SLFWPgen]
MkstructProp.mkstruct_erase [in SLFWPgen]
MkstructProp.mkstruct_conseq [in SLFWPgen]
MkstructProp.mkstruct_frame [in SLFWPgen]


N

NewTriples.MotivatingExampleWithUpdatedXwp.haffine_hany [in SLFAffine]
NewTriples.xwp_lemma [in SLFAffine]


P

predicate_extensionality [in SLFHprop]
Preview.haffine [in SLFAffine]
Preview.triple_haffine_pre [in SLFAffine]
Preview.triple_haffine_post [in SLFAffine]
PrimitiveNaryFun.eval_apps_fixs [in SLFRich]
PrimitiveNaryFun.eval_fixs [in SLFRich]
PrimitiveNaryFun.trm_apps [in SLFRich]
PrimitiveNaryFun.trm_fixs [in SLFRich]
PrimitiveNaryFun.val_fixs [in SLFRich]
PrimitiveNaryFun.var_fixs_exec [in SLFRich]
PrimitiveNaryFun.xwp_lemma_fixs [in SLFRich]
ProofsContinued.eval_free_sep [in SLFRules]
ProofsContinued.eval_free [in SLFRules]
ProofsContinued.eval_set [in SLFRules]
ProofsContinued.eval_app_fun [in SLFRules]
Proofs.eval_ref [in SLFRules]
Proofs.eval_get [in SLFRules]
Proofs.eval_div' [in SLFRules]
Proofs.eval_add [in SLFRules]
Proofs.eval_let [in SLFRules]
Proofs.eval_seq [in SLFRules]
Proofs.eval_val [in SLFRules]
Proofs.exists_not_indom [in SLFRules]
Proofs.hsingle_inv [in SLFRules]
Proofs.hstar_hpure_l' [in SLFRules]
Proofs.hstar_hpure_l [in SLFRules]
propositional_extensionality [in SLFMinimal]
ProveAppend.MList_if [in SLFSummary]
ProveExtractionRules.hpure_encoding [in SLFHimpl]
ProveExtractionRules.hstar_hexists' [in SLFHimpl]
ProveExtractionRules.triple_hexists' [in SLFHimpl]
ProveExtractionRules.triple_hpure' [in SLFHimpl]


R

Realization.eval_length [in SLFStruct]
Realization.eval_ptr_add [in SLFStruct]
Realization.eval_dealloc [in SLFStruct]
Realization.eval_alloc [in SLFStruct]
Realization.hcells_focus_read [in SLFStruct]
Realization.hheader_def [in SLFStruct]
Realization.val_length [in SLFStruct]
Realization.val_ptr_add [in SLFStruct]
Realization.val_header [in SLFStruct]
Rules.hoare_seq [in SLFSummary]
Rules.triple_free [in SLFSummary]
Rules.triple_ref [in SLFSummary]
Rules.triple_set [in SLFSummary]
Rules.triple_get [in SLFSummary]
Rules.triple_seq [in SLFSummary]
Rules.triple_hexists [in SLFSummary]
Rules.triple_hpure [in SLFSummary]
Rules.triple_frame [in SLFSummary]
Rules.triple_conseq [in SLFSummary]


S

Semantics.subst [in SLFSummary]


T

TexanTriples.incr [in SLFWand]
TexanTriples.triple_incr [in SLFWand]
TexanTriples.triple_free' [in SLFWand]
TexanTriples.triple_set' [in SLFWand]
TexanTriples.triple_ref [in SLFWand]
TexanTriples.wp_ref [in SLFWand]
triple_hgc_post [in SLFAffine]
triple_hany_pre [in SLFAffine]
triple_hany_post [in SLFAffine]
triple_app_fun_from_wpgen [in SLFWPgen]
triple_ref' [in SLFBasic]
triple_ref [in SLFBasic]
triple_ref_with_frame [in SLFHprop]
triple_ref [in SLFHprop]
triple_incr_3 [in SLFHprop]
triple_incr [in SLFHprop]
triple_dealloc_hrecord [in SLFStruct]
triple_alloc_hrecord [in SLFStruct]
triple_set_field_hrecord [in SLFStruct]
triple_set_field_hfields [in SLFStruct]
triple_set_field [in SLFStruct]
triple_get_field_hrecord [in SLFStruct]
triple_get_field_hfields [in SLFStruct]
triple_get_field [in SLFStruct]
triple_array_length_header [in SLFStruct]
triple_array_length [in SLFStruct]
triple_array_set [in SLFStruct]
triple_array_get [in SLFStruct]
triple_dealloc [in SLFStruct]
triple_alloc_array [in SLFStruct]
triple_alloc [in SLFStruct]
triple_alloc_nat [in SLFStruct]
triple_ramified_frame [in SLFSummary]
triple_conseq_frame [in SLFSummary]
triple_hexists [in SLFHimpl]
triple_hpure [in SLFHimpl]
triple_frame [in SLFHimpl]
triple_conseq [in SLFHimpl]
triple_conseq_frame [in SLFWPsem]
triple_hexists [in SLFWPsem]
triple_app_fun [in SLFWPsem]
triple_let [in SLFWPsem]
triple_if [in SLFWPsem]
triple_fun [in SLFWPsem]
triple_seq [in SLFWPsem]
triple_val [in SLFWPsem]
triple_hpure [in SLFWPsem]
triple_app_fix [in SLFRules]
triple_fix [in SLFRules]
triple_hexists [in SLFRules]
triple_hpure [in SLFRules]
triple_conseq_frame [in SLFRules]
triple_conseq [in SLFRules]
triple_frame [in SLFRules]
triple_free [in SLFRules]
triple_ref' [in SLFRules]
triple_ref [in SLFRules]
triple_set [in SLFRules]
triple_get [in SLFRules]
triple_div' [in SLFRules]
triple_div [in SLFRules]
triple_add [in SLFRules]
triple_app_fun [in SLFRules]
triple_fun [in SLFRules]
triple_val [in SLFRules]
triple_if_case [in SLFRules]
triple_let [in SLFRules]
triple_seq [in SLFRules]
Triple.triple_incr [in SLFSummary]


V

val_set_field [in SLFStruct]
val_get_field [in SLFStruct]
val_array_length [in SLFStruct]
val_array_set [in SLFStruct]
val_array_get [in SLFStruct]
val_dealloc [in SLFStruct]
val_uninit [in SLFStruct]
val_alloc [in SLFStruct]


W

WandBenefits.triple_ref [in SLFWand]
WandBenefits.triple_conseq_frame [in SLFWand]
WandDef.triple_conseq_frame [in SLFWand]
WandDef.wp_conseq_frame [in SLFWand]
WhileLoops.eval_while [in SLFRich]
WhileLoops.LoopRuleAffine.triple_conseq_frame_hgc [in SLFRich]
WhileLoops.trm_while [in SLFRich]
WhileLoops.wpgen_while_eq [in SLFRich]
wp [in SLFWPsem]
WpgenExec1.triple_app_fun_from_wpgen [in SLFWPgen]
WpgenExec1.triple_app_fun [in SLFWPgen]
WpgenExec1.wpgen_sound [in SLFWPgen]
WpgenExec2.triple_app_fun_from_wpgen [in SLFWPgen]
WpgenExec2.wpgen_sound [in SLFWPgen]
WPgenRec.triple_app_fix_from_wpgen [in SLFWand]
WPgenRec.triple_app_fun_from_wpgen [in SLFWand]
WPgenSound.isubst_rem [in SLFWPgen]
WPgenSound.isubst_nil [in SLFWPgen]
WPgenSound.wpgen_sound_seq' [in SLFWPgen]
WPgenSound.wpgen_sound_seq [in SLFWPgen]
WPgenSound.wpgen_sound' [in SLFWPgen]
wpgen_sound [in SLFWPgen]
Wpgen.mkstruct_conseq [in SLFSummary]
Wpgen.mkstruct_frame [in SLFSummary]
Wpgen.mkstruct_erase [in SLFSummary]
Wpgen.triple_of_wpgen [in SLFSummary]
Wpgen.wp_equiv [in SLFSummary]
Wpgen.wp_of_wpgen [in SLFSummary]
Wpgen.wp_seq [in SLFSummary]
WpIfAlt.wp_if [in SLFWPsem]
Wpsem.himpl_hstar_hpure_l [in SLFSummary]
Wpsem.triple_hpure [in SLFSummary]
Wpsem.wp_frame [in SLFSummary]
Wpsem.wp_conseq [in SLFSummary]
Wpsem.wp_seq [in SLFSummary]
Wpsem.wp_equiv [in SLFSummary]
Wpsem.wp_weakest [in SLFSummary]
Wpsem.wp_pre [in SLFSummary]
wp_frame [in SLFWPgen]
wp_if [in SLFWPgen]
wp_let [in SLFWPgen]
wp_seq [in SLFWPgen]
wp_fun [in SLFWPgen]
wp_val [in SLFWPgen]
wp_ramified [in SLFSummary]
wp_equiv [in SLFWPsem]


X

XGC.mkstruct_hgc [in SLFAffine]



Constructor Index

E

eval_free [in SLFMinimal]
eval_set [in SLFMinimal]
eval_get [in SLFMinimal]
eval_ref [in SLFMinimal]
eval_div [in SLFMinimal]
eval_add [in SLFMinimal]
eval_if [in SLFMinimal]
eval_let [in SLFMinimal]
eval_app [in SLFMinimal]
eval_fix [in SLFMinimal]
eval_val [in SLFMinimal]


L

Language.trm_if [in SLFSummary]
Language.trm_let [in SLFSummary]
Language.trm_seq [in SLFSummary]
Language.trm_app [in SLFSummary]
Language.trm_fix [in SLFSummary]
Language.trm_fun [in SLFSummary]
Language.trm_var [in SLFSummary]
Language.trm_val [in SLFSummary]
Language.val_add [in SLFSummary]
Language.val_free [in SLFSummary]
Language.val_set [in SLFSummary]
Language.val_get [in SLFSummary]
Language.val_ref [in SLFSummary]
Language.val_fix [in SLFSummary]
Language.val_fun [in SLFSummary]
Language.val_loc [in SLFSummary]
Language.val_int [in SLFSummary]
Language.val_bool [in SLFSummary]
Language.val_unit [in SLFSummary]


P

PrimitiveNaryFun.NarySyntax.apps_next [in SLFRich]
PrimitiveNaryFun.NarySyntax.apps_init [in SLFRich]
PrimitiveNaryFun.NarySyntax.trm_apps [in SLFRich]
PrimitiveNaryFun.NarySyntax.trm_val [in SLFRich]


S

Semantics.eval_get [in SLFSummary]
Semantics.eval_let [in SLFSummary]
Semantics.eval_val [in SLFSummary]
SyntaxAndSemantics.eval_free [in SLFRules]
SyntaxAndSemantics.eval_set [in SLFRules]
SyntaxAndSemantics.eval_get [in SLFRules]
SyntaxAndSemantics.eval_ref [in SLFRules]
SyntaxAndSemantics.eval_div [in SLFRules]
SyntaxAndSemantics.eval_add [in SLFRules]
SyntaxAndSemantics.eval_if [in SLFRules]
SyntaxAndSemantics.eval_let [in SLFRules]
SyntaxAndSemantics.eval_seq [in SLFRules]
SyntaxAndSemantics.eval_app_fix [in SLFRules]
SyntaxAndSemantics.eval_app_fun [in SLFRules]
SyntaxAndSemantics.eval_fix [in SLFRules]
SyntaxAndSemantics.eval_fun [in SLFRules]
SyntaxAndSemantics.eval_val [in SLFRules]
SyntaxAndSemantics.trm_if [in SLFRules]
SyntaxAndSemantics.trm_let [in SLFRules]
SyntaxAndSemantics.trm_seq [in SLFRules]
SyntaxAndSemantics.trm_app [in SLFRules]
SyntaxAndSemantics.trm_fix [in SLFRules]
SyntaxAndSemantics.trm_fun [in SLFRules]
SyntaxAndSemantics.trm_var [in SLFRules]
SyntaxAndSemantics.trm_val [in SLFRules]
SyntaxAndSemantics.val_div [in SLFRules]
SyntaxAndSemantics.val_add [in SLFRules]
SyntaxAndSemantics.val_free [in SLFRules]
SyntaxAndSemantics.val_set [in SLFRules]
SyntaxAndSemantics.val_get [in SLFRules]
SyntaxAndSemantics.val_ref [in SLFRules]
SyntaxAndSemantics.val_fix [in SLFRules]
SyntaxAndSemantics.val_fun [in SLFRules]
SyntaxAndSemantics.val_loc [in SLFRules]
SyntaxAndSemantics.val_int [in SLFRules]
SyntaxAndSemantics.val_bool [in SLFRules]
SyntaxAndSemantics.val_unit [in SLFRules]


T

trm_if [in SLFMinimal]
trm_let [in SLFMinimal]
trm_app [in SLFMinimal]
trm_fix [in SLFMinimal]
trm_var [in SLFMinimal]
trm_val [in SLFMinimal]


V

val_fix [in SLFMinimal]
val_prim [in SLFMinimal]
val_loc [in SLFMinimal]
val_int [in SLFMinimal]
val_bool [in SLFMinimal]
val_unit [in SLFMinimal]
val_div [in SLFMinimal]
val_add [in SLFMinimal]
val_free [in SLFMinimal]
val_set [in SLFMinimal]
val_get [in SLFMinimal]
val_ref [in SLFMinimal]



Inductive Index

E

eval [in SLFMinimal]


L

Language.trm [in SLFSummary]
Language.val [in SLFSummary]


P

prim [in SLFMinimal]
PrimitiveNaryFun.NarySyntax.apps [in SLFRich]
PrimitiveNaryFun.NarySyntax.trm [in SLFRich]


S

Semantics.eval [in SLFSummary]
SyntaxAndSemantics.eval [in SLFRules]
SyntaxAndSemantics.trm [in SLFRules]
SyntaxAndSemantics.val [in SLFRules]


T

trm [in SLFMinimal]


V

val [in SLFMinimal]



Section Index

T

TexanTriples.WpSpecRef [in SLFWand]


W

WhileLoops.DemoLoopFrame [in SLFRich]



Instance Index

I

Inhab_val [in SLFMinimal]


S

SyntaxAndSemantics.Inhab_val [in SLFRules]



Definition Index

A

aliased_call [in SLFBasic]


C

ConjDisj.hand [in SLFWand]
ConjDisj.hand' [in SLFWand]
ConjDisj.hor [in SLFWand]
ConjDisj.hor' [in SLFWand]
ctx [in SLFWPgen]
CurriedFun.trm_is_val [in SLFRich]


E

ExampleLists.append [in SLFBasic]
ExampleLists.cps_append [in SLFBasic]
ExampleLists.cps_append_aux [in SLFBasic]
ExampleLists.head [in SLFBasic]
ExampleLists.mcons [in SLFBasic]
ExampleLists.mcopy [in SLFBasic]
ExampleLists.MList [in SLFBasic]
ExampleLists.mnil [in SLFBasic]
ExampleLists.tail [in SLFBasic]
ExamplePrograms.incr [in SLFRules]
ExamplePrograms.incr' [in SLFRules]
ExamplePrograms.succ_using_incr [in SLFRules]
example_let [in SLFBasic]
example_val' [in SLFHprop]
example_val [in SLFHprop]


F

factorec [in SLFBasic]
field [in SLFStruct]
formula [in SLFWPgen]
FullyAffineLogic.htop [in SLFAffine]


H

haffine [in SLFAffine]
HaffineQuantifiers.haffine_post [in SLFAffine]
harray [in SLFStruct]
hcells [in SLFStruct]
head [in SLFStruct]
heap [in SLFHprop]
heap [in SLFMinimal]
hempty [in SLFHprop]
hempty [in SLFMinimal]
hempty' [in SLFHprop]
hexists [in SLFHprop]
hexists [in SLFMinimal]
hfield [in SLFStruct]
hfields [in SLFStruct]
hfields_update [in SLFStruct]
hfields_lookup [in SLFStruct]
hforall [in SLFMinimal]
hgc [in SLFAffine]
hgc' [in SLFAffine]
himpl [in SLFMinimal]
himpl [in SLFHimpl]
hoare [in SLFHprop]
hoare [in SLFMinimal]
hprop [in SLFHprop]
hprop [in SLFMinimal]
Hprop.hempty [in SLFSummary]
Hprop.hexists [in SLFSummary]
Hprop.himpl [in SLFSummary]
Hprop.hprop [in SLFSummary]
Hprop.hpure [in SLFSummary]
Hprop.hsingle [in SLFSummary]
Hprop.hstar [in SLFSummary]
hpure [in SLFHprop]
hpure [in SLFMinimal]
hpure' [in SLFHprop]
hrecord [in SLFStruct]
hrecord_fields [in SLFStruct]
hrecord_field [in SLFStruct]
hsingle [in SLFHprop]
hsingle [in SLFMinimal]
hstar [in SLFHprop]
hstar [in SLFMinimal]
hwand [in SLFSummary]
HwandEquiv.hwand_characterization_4 [in SLFWand]
HwandEquiv.hwand_characterization_3 [in SLFWand]
HwandEquiv.hwand_characterization_2 [in SLFWand]
HwandEquiv.hwand_characterization_1 [in SLFWand]


I

incr [in SLFBasic]
incr [in SLFMinimal]
incr_first [in SLFBasic]
incr_two [in SLFBasic]
inplace_double [in SLFBasic]
isubst [in SLFWPgen]
IsubstProp.ctx_disjoint [in SLFWPgen]
IsubstProp.ctx_equiv [in SLFWPgen]


L

Language.loc [in SLFSummary]
Language.var [in SLFSummary]
ListDealloc.mfree_list [in SLFStruct]
loc [in SLFMinimal]
lookup [in SLFWPgen]
LowLevel.triple [in SLFAffine]
LowLevel.triple_lowlevel [in SLFAffine]


M

maps_all_fields [in SLFStruct]
mkstruct [in SLFWPgen]
MkstructGuess.mkstruct [in SLFWPgen]
MList [in SLFStruct]
MotivatingExample.succ_using_incr [in SLFAffine]


N

NewQwand.hforall [in SLFWand]
NewQwand.mkstruct [in SLFWand]
NewQwand.mkstruct' [in SLFWand]
NewQwand.qwand [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_5 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_4 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_3 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_2 [in SLFWand]
NewQwand.QwandEquiv.qwand_characterization_1 [in SLFWand]
NewTriples.mkstruct [in SLFAffine]
NewTriples.triple [in SLFAffine]
NewTriples.wp [in SLFAffine]
null [in SLFMinimal]


P

Parsing.mlength [in SLFSummary]
Parsing.mlength' [in SLFSummary]
PrimitiveNaryFun.NarySyntax.apps_to_trm [in SLFRich]
PrimitiveNaryFun.substn [in SLFRich]
PrimitiveNaryFun.trms [in SLFRich]
PrimitiveNaryFun.trms_to_vals [in SLFRich]
PrimitiveNaryFun.vals [in SLFRich]
PrimitiveNaryFun.vars [in SLFRich]
PrimitiveNaryFun.var_fixs [in SLFRich]
ProofsSameSemantics.eval_like [in SLFRules]
ProofsSameSemantics.trm_equiv [in SLFRules]
ProveAppend.append [in SLFSummary]
ProveAppend.head [in SLFSummary]
ProveAppend.MList [in SLFSummary]
ProveAppend.tail [in SLFSummary]
ProveIncrWithTactics.incr [in SLFSummary]
ProveIncr.incr [in SLFSummary]
ProveIncr.incr' [in SLFSummary]


Q

qimpl [in SLFMinimal]
qimpl [in SLFHimpl]
Qprop.qimpl [in SLFSummary]
quadruple [in SLFBasic]
qwand [in SLFSummary]


R

Realization.ArrayAccessDef.val_array_set [in SLFStruct]
Realization.ArrayAccessDef.val_array_get [in SLFStruct]
Realization.ArrayAccessDef.val_array_length [in SLFStruct]
Realization.FieldAccessDef.val_set_field [in SLFStruct]
Realization.FieldAccessDef.val_get_field [in SLFStruct]
RecordInit.mcons [in SLFStruct]
RecordInit.val_new_hrecord_2 [in SLFStruct]
ref_greater [in SLFBasic]
rem [in SLFWPgen]
repeat_incr [in SLFBasic]


S

Semantics.state [in SLFSummary]
state [in SLFHprop]
step_transfer [in SLFBasic]
subst [in SLFMinimal]
succ_using_incr [in SLFBasic]
succ_using_incr_attempt [in SLFBasic]
SummaryHprop.hempty [in SLFWand]
SummaryHprop.hexists [in SLFWand]
SummaryHprop.hforall [in SLFWand]
SummaryHprop.hsingle [in SLFWand]
SummaryHprop.hstar [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hand [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hor [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hpure [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.hwand [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.qwand [in SLFWand]
SummaryHprop.ReaminingOperatorsDerived.qwand' [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hand [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hor [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hpure [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.hwand [in SLFWand]
SummaryHprop.ReaminingOperatorsDirect.qwand [in SLFWand]
SyntaxAndSemantics.state [in SLFRules]
SyntaxAndSemantics.subst [in SLFRules]


T

tail [in SLFStruct]
transfer [in SLFBasic]
triple [in SLFHprop]
triple [in SLFMinimal]
triple_lowlevel [in SLFHprop]
Triple.hoare [in SLFSummary]
Triple.triple [in SLFSummary]


V

val_dealloc_hrecord [in SLFStruct]
val_alloc_hrecord [in SLFStruct]
var [in SLFMinimal]
var_eq [in SLFMinimal]


W

WandDef.hwand [in SLFWand]
WandDef.hwand' [in SLFWand]
WandDef.qwand [in SLFWand]
WhileLoops.mlength_loop [in SLFRich]
WhileLoops.wpgen_while [in SLFRich]
WhileLoops.wpgen_if_trm [in SLFRich]
WpFromHoare.wp [in SLFWPsem]
wpgen [in SLFWPgen]
WpgenExec1.wpgen [in SLFWPgen]
WpgenExec2.wpgen [in SLFWPgen]
WPgenRec.myfun [in SLFWand]
WPgenRec.wpgen [in SLFWand]
WPgenRec.wpgen_fix [in SLFWand]
WPgenRec.wpgen_fun [in SLFWand]
WPgenSound.formula_sound [in SLFWPgen]
wpgen_var [in SLFWPgen]
wpgen_fail [in SLFWPgen]
wpgen_if [in SLFWPgen]
wpgen_let [in SLFWPgen]
wpgen_val [in SLFWPgen]
wpgen_seq [in SLFWPgen]
Wpgen.formula [in SLFSummary]
Wpgen.mkstruct [in SLFSummary]
WpHighLevel.wp [in SLFWPsem]
WpLowLevel.wp [in SLFWPsem]
Wpsem.wp [in SLFSummary]



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 (1222 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 (60 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 (84 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 (13 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 (527 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 (233 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 (89 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 (12 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 (2 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 (2 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 (200 entries)

This page has been generated by coqdoc