Basic
triple_quadruple
triple_inplace_double
triple_transfer
triple_transfer_aliased
triple_ref_greater_abstract
triple_get_and_free
triple_two_dice
triple_repeat_incr
triple_repeat_incr'
triple_step_transfer
triple_factoimp_aux
triple_factoimp
triple_factoimp_aux'
triple_factoimp'
Repr
triple_mlength
triple_mlength'
triple_mfree
triple_mrev
SizedStack.triple_push
SizedStack.triple_pop
SizedStack.triple_top
triple_mnode'
triple_tree_copy
triple_mtreesum
triple_apply_counter_abstract
triple_test_counter
triple_miter
triple_mlength_using_miter
triple_cps_facto_aux
triple_cps_facto
triple_cps_append_aux
triple_cps_append
Hprop
HpropProofs.hstar_hempty_l
HpropProofs.hstar_assoc
HpropProofs.hstar_comm_assoc
HpropProofs.hstar_hpure_l
Extensionality.predicate_extensionality_derived
Himpl
himpl_antisym
qimpl_antisym
himpl_hstar_hpure_r
himpl_hstar_hpure_l
himpl_hexists_r
himpl_hexists_l
hexists_named_eq
XsimplTactic.EntailmentProofs.himpl_example_1
XsimplTactic.EntailmentProofs.himpl_example_2
XsimplTactic.EntailmentProofs.himpl_example_3
XsimplTactic.xchange_lemma
EntailmentRulesProofs.himpl_frame_l
EntailmentRulesProofs.himpl_frame_r
EntailmentRulesProofs.himpl_frame_lr
Triples
StructuralRules.triple_conseq_frame
StructuralRules.triple_hpure'
triple_hexists
triple_named_heap
AlternativeExistentialRule.triple_hexists2
AlternativeExistentialRule.triple_hexists_of_triple_hexists2
seval_val_inv
seval_terminates
seval_safe
seval_correct
seval_seq
seval_let
BakedInFrame.hoare_conseq
BakedInFrame.btriple_frame
Rules
triple_seq
triple_if_case
triple_val_minimal
triple_val'
triple_let_val
triple_rand
triple_free'
triple_set
ExamplePrograms.triple_succ_using_incr
ProofsSameSemantics.eval_like_eta_expansion
ProofsSameSemantics.eval_like_eta_expansion
ProofsSameSemantics.eta_same_triples
ProofsSameSemantics.triple_trm_seq_assoc
LetFrame.triple_let_frame
DivSpec.triple_div_from_triple_div'
ExamplePrograms2.triple_factorec
WPsem
wp_conseq_of_wp_ramified
wp_frame_of_wp_ramified
wp_if'
wp_conseq_frame_trans
wp_conseq_frame
WpFromTriple.wp_equiv_1
WpFromTriple2.wp_equiv_2
wp_equiv_iff_wp_pre_and_wp_weakest
TexanTriples.wp_incr
WPgen
ProofsWithXlemmas.triple_succ_using_incr_with_xlemmas
ProofsWithXtactics.triple_succ_using_incr_with_xtactics
xconseq_lemma
xframe_lemma
WPsound
mkstruct_idempotent
Wand
Hor.hor_eq_hor'
Hor.hor_comm
Hor.HorExample.MList_using_hor
Hand.hand_eq_hand'
Hand.hand_comm
Hwand.hwand_hpure_l
Hwand.himpl_hwand_hpure_lr
Hwand.himpl_hwand_hstar_same_r
Hwand.hwand_cancel_part
Hwand.hwand_frame
Hwand.hwand_inv
Qwand.himpl_qwand_hstar_same_r
Qwand.qwand_cancel_part
Affine
triple_frame
hgc_inv
himpl_hgc_absorb_r
NewTriples.triple_hgc_post
NewTriples.triple_haffine_post
NewTriples.triple_hgc_post_from_triple_haffine_post
NewTriples.triple_haffine_pre
NewTriples.triple_conseq_frame_hgc
NewTriples.triple_ramified_frame_hgc
NewTriples.wp_hgc_post
NewTriples.wp_haffine_pre
NewTriples.wp_haffine_pre
NewTriples.mkstruct_haffine_post
NewTriples.mkstruct_haffine_pre
Arrays
QuickSort.triple_quicksort_safety
QuickSort.triple_quicksort
QuickSort.triple_quicksort_full
Realization.hseg_app
Realization.hseg_focus
Realization.harray_focus_read