| 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 | \ | _ | (305 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 | _ | (92 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 | _ | (2 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 | _ | (59 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 | _ | (12 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 | _ | (80 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 | _ | (27 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 | _ | (19 entries) | |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5 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 | \ | _ | (9 entries) |
Global Index
A
AddExpr [constructor, in Language]alloc [definition, in Language]
alloc_sep [lemma, in ProofSystemFacts]
AndAsn [constructor, in ProofSystem]
ApplyAsn [constructor, in ProofSystem]
asn [inductive, in ProofSystem]
asn_mono [definition, in ProofSystem]
asn_mono_conj [lemma, in ProofSystemFacts]
asn_mono_sep [lemma, in ProofSystemFacts]
Assign [constructor, in Language]
assigns [definition, in ProofSystem]
Assoc [section, in Assoc]
assoc [definition, in Assoc]
Assoc.A [variable, in Assoc]
Assoc.B [variable, in Assoc]
Assoc.eq [variable, in Assoc]
B
BadSeed [constructor, in Language]C
Call [constructor, in Language]closure [inductive, in ProofSystem]
Closure [constructor, in ProofSystem]
closure_interp [definition, in ProofSystem]
closure_of_num [axiom, in ProofSystem]
closure_of_num_of_closure [axiom, in ProofSystem]
cmd [inductive, in Language]
config [definition, in Language]
conj_sep_pure_left [lemma, in ProofSystemFacts]
conj_sep_pure_right [lemma, in ProofSystemFacts]
Cons [constructor, in Language]
cont [inductive, in Language]
D
dealloc [definition, in Language]Dispose [constructor, in Language]
Done [constructor, in Language]
dontcare [definition, in ProofSystem]
dontcare_sep [lemma, in ProofSystemFacts]
dummy_pointstos [definition, in ProofSystem]
dummy_pointstos_dealloc [lemma, in ProofSystemFacts]
dummy_pointstos_intuit [lemma, in ProofSystemFacts]
E
EqAsn [constructor, in ProofSystem]eval [definition, in Language]
ExistsAsn [constructor, in ProofSystem]
exists_sep_left [lemma, in ProofSystemFacts]
expr [inductive, in Language]
F
funtype [definition, in Language]FunTypeAsn [constructor, in ProofSystem]
funtypedef [inductive, in ProofSystem]
FunTypeDef [constructor, in ProofSystem]
funtype_interp [definition, in ProofSystem]
H
heap [definition, in Language]heap_contains [definition, in Language]
heap_contains_heap_try_lookup [lemma, in ProofSystemFacts]
heap_remove [definition, in Language]
heap_try_lookup [definition, in Language]
heap_try_lookup_app_left [lemma, in ProofSystemFacts]
heap_try_lookup_app_right [lemma, in ProofSystemFacts]
heap_try_lookup_heap_remove [lemma, in ProofSystemFacts]
heap_try_lookup_heap_remove_diff [lemma, in ProofSystemFacts]
heap_try_lookup_heap_remove_same [lemma, in ProofSystemFacts]
heap_try_lookup_heap_update_diff [lemma, in ProofSystemFacts]
heap_try_lookup_heap_update_same [lemma, in ProofSystemFacts]
heap_update [definition, in Language]
I
IfEq [constructor, in Language]intuit [definition, in ProofSystemFacts]
is_split [definition, in ProofSystem]
is_split_assoc_left [lemma, in ProofSystemFacts]
is_split_commut [lemma, in ProofSystemFacts]
is_split_dealloc_left [lemma, in ProofSystemFacts]
is_split_dealloc_right [lemma, in ProofSystemFacts]
is_split_heap_remove [lemma, in ProofSystemFacts]
is_split_heap_try_lookup_left [lemma, in ProofSystemFacts]
is_split_heap_update_left [lemma, in ProofSystemFacts]
is_split_nil_left [lemma, in ProofSystemFacts]
L
LAdd [constructor, in ProofSystem]lambda [inductive, in Language]
Lambda [constructor, in Language]
LambdaV [constructor, in Language]
lambda_of_num [axiom, in Language]
lambda_of_num_of_lambda [axiom, in Language]
leval [definition, in ProofSystem]
lexpr [inductive, in ProofSystem]
LibAsn [constructor, in ProofSystem]
Lit [constructor, in Language]
LLambda [constructor, in ProofSystem]
LLit [constructor, in ProofSystem]
Load [constructor, in Language]
Lookup [constructor, in Language]
lstore [definition, in ProofSystem]
lvar [definition, in ProofSystem]
LVar [constructor, in ProofSystem]
M
map_compos [lemma, in ProofSystemFacts]mem_assoc [definition, in Assoc]
ModuleAsn [constructor, in ProofSystem]
moduledef [definition, in Language]
ModuleMap [module, in Language]
ModuleMapValid [module, in Soundness]
ModuleMapValid.modules_valid [axiom, in Soundness]
ModuleMap.modules [axiom, in Language]
ModuleMap.modules_try_lookup [definition, in Language]
modulename [definition, in Language]
ModuleNameV [constructor, in Language]
Module0Asn [constructor, in ProofSystem]
Mutate [constructor, in Language]
mymain [definition, in ExampleProgram]
mymainNotStuck [lemma, in ExampleProof]
MyModuleMap [module, in ExampleProgram]
MyModuleMapValid [module, in ExampleProof]
MyModuleMapValid.disposeFunc_valid [lemma, in ExampleProof]
MyModuleMapValid.incrFunc_valid [lemma, in ExampleProof]
MyModuleMapValid.main_valid [lemma, in ExampleProof]
MyModuleMapValid.modules_valid [lemma, in ExampleProof]
MyModuleMapValid.myIncrLib_valid [lemma, in ExampleProof]
MyModuleMapValid.Qbody [definition, in ExampleProof]
MyModuleMapValid.Qclosure [definition, in ExampleProof]
MyModuleMap.disposeFunc [definition, in ExampleProgram]
MyModuleMap.getIncrFunc [definition, in ExampleProgram]
MyModuleMap.incrFunc [definition, in ExampleProgram]
MyModuleMap.modules [definition, in ExampleProgram]
MyModuleMap.modules_try_lookup [definition, in ExampleProgram]
MyModuleMap2 [module, in ExampleProgram]
MyModuleMap2.modules [definition, in ExampleProgram]
MyModuleMap2.modules_try_lookup [definition, in ExampleProgram]
MySemantics [module, in ExampleProgram]
MySemantics [module, in ExampleProgram]
MySoundness [module, in ExampleProof]
MySpec [module, in ExampleSpec]
MySpec.funtypemap [definition, in ExampleSpec]
N
nat_of_Z_of_nat [lemma, in ProofSystemFacts]NewConfig [constructor, in Language]
NoDup_map_store_lookup_combine [lemma, in ProofSystemFacts]
notIn_map_store_lookup [lemma, in ProofSystemFacts]
NumV [constructor, in Language]
num_of_closure [axiom, in ProofSystem]
num_of_lambda [axiom, in Language]
num_of_lambda_of_num [axiom, in Language]
num_of_string [axiom, in Language]
num_of_string_of_num [axiom, in Language]
P
PointsTo [constructor, in ProofSystem]pointstos [definition, in ProofSystem]
pointstos' [definition, in ProofSystem]
pointstos'_dontcare [lemma, in ProofSystemFacts]
pointstos'_intuit [lemma, in ProofSystemFacts]
pointstos_intuit [lemma, in ProofSystemFacts]
pointstos_sep [lemma, in ProofSystemFacts]
ProofSystem [module, in ProofSystem]
ProofSystemFacts [module, in ProofSystemFacts]
ProofSystemFacts.asn_mono_asn_true [lemma, in ProofSystemFacts]
ProofSystemFacts.dummy_pointstos_dontcare [lemma, in ProofSystemFacts]
ProofSystemFacts.module0_dontcare [lemma, in ProofSystemFacts]
ProofSystemFacts.module_dontcare [lemma, in ProofSystemFacts]
ProofSystem.asn_true [definition, in ProofSystem]
ProofSystem.CAssign [constructor, in ProofSystem]
ProofSystem.CCall [constructor, in ProofSystem]
ProofSystem.CCons [constructor, in ProofSystem]
ProofSystem.CConseq [constructor, in ProofSystem]
ProofSystem.CDispose [constructor, in ProofSystem]
ProofSystem.CExists [constructor, in ProofSystem]
ProofSystem.CFalse [constructor, in ProofSystem]
ProofSystem.CFrame [constructor, in ProofSystem]
ProofSystem.CIfEq [constructor, in ProofSystem]
ProofSystem.CLoad [constructor, in ProofSystem]
ProofSystem.CLookup [constructor, in ProofSystem]
ProofSystem.CMutate [constructor, in ProofSystem]
ProofSystem.command_valid [definition, in ProofSystem]
ProofSystem.correct [inductive, in ProofSystem]
ProofSystem.CSeq [constructor, in ProofSystem]
ProofSystem.CUnload [constructor, in ProofSystem]
ProofSystem.funtype_try_lookup [definition, in ProofSystem]
ProofSystem.lib [definition, in ProofSystem]
ProofSystem.module [definition, in ProofSystem]
ProofSystem.module0 [definition, in ProofSystem]
ProofSystem.module_valid [definition, in ProofSystem]
ProofSystem.PCombine [constructor, in ProofSystem]
ProofSystem.PFold [constructor, in ProofSystem]
ProofSystem.PFunType [constructor, in ProofSystem]
ProofSystem.provable [inductive, in ProofSystem]
ProofSystem.PTrue [constructor, in ProofSystem]
ProofSystem.PUnfold [constructor, in ProofSystem]
pure [definition, in ProofSystem]
PVar [constructor, in ProofSystem]
R
remove [definition, in Assoc]Ret [constructor, in Language]
S
sasn [definition, in ProofSystem]seed [definition, in Language]
Semantics [module, in Language]
Semantics.nsteps [definition, in Language]
Semantics.nsteps_assoc [lemma, in Language]
Semantics.step [definition, in Language]
Sep [constructor, in ProofSystem]
sep [definition, in ProofSystem]
sep_assoc_left [lemma, in ProofSystemFacts]
sep_assoc_right [lemma, in ProofSystemFacts]
sep_commut [lemma, in ProofSystemFacts]
sep_conj_pure_left [lemma, in ProofSystemFacts]
sep_exists_left [lemma, in ProofSystemFacts]
sep_mono [lemma, in ProofSystemFacts]
sep_pure_left [lemma, in ProofSystemFacts]
sep_pure_right_destruct [lemma, in ProofSystemFacts]
sep_stores [lemma, in ProofSystemFacts]
sep_stores_backward [lemma, in ProofSystemFacts]
Seq [constructor, in Language]
SeqC [constructor, in Language]
SoundnessProof [module, in Soundness]
SoundnessProof.asn_mono_Fn_mono [lemma, in Soundness]
SoundnessProof.asn_true_mono [lemma, in Soundness]
SoundnessProof.c_ind [definition, in Soundness]
SoundnessProof.Fn [definition, in Soundness]
SoundnessProof.Fn_mono [lemma, in Soundness]
SoundnessProof.HCAssign [lemma, in Soundness]
SoundnessProof.HCCall [lemma, in Soundness]
SoundnessProof.HCCons [lemma, in Soundness]
SoundnessProof.HCConseq [lemma, in Soundness]
SoundnessProof.HCDispose [lemma, in Soundness]
SoundnessProof.HCExists [lemma, in Soundness]
SoundnessProof.HCFalse [lemma, in Soundness]
SoundnessProof.HCFrame [lemma, in Soundness]
SoundnessProof.HCIfEq [lemma, in Soundness]
SoundnessProof.HCLoad [lemma, in Soundness]
SoundnessProof.HCLookup [lemma, in Soundness]
SoundnessProof.HCMutate [lemma, in Soundness]
SoundnessProof.HCSeq [lemma, in Soundness]
SoundnessProof.HCUnload [lemma, in Soundness]
SoundnessProof.HPCombine [lemma, in Soundness]
SoundnessProof.HPFold [lemma, in Soundness]
SoundnessProof.HPFunType [lemma, in Soundness]
SoundnessProof.HPTrue [lemma, in Soundness]
SoundnessProof.HPUnfold [lemma, in Soundness]
SoundnessProof.Jdef [definition, in Soundness]
SoundnessProof.Jdef_mono [lemma, in Soundness]
SoundnessProof.Jfix [definition, in Soundness]
SoundnessProof.Jfix_fold [lemma, in Soundness]
SoundnessProof.Jfix_mono [lemma, in Soundness]
SoundnessProof.Jfix_unfold [lemma, in Soundness]
SoundnessProof.Pc [definition, in Soundness]
SoundnessProof.Pmods [definition, in Soundness]
SoundnessProof.Pmods_all [lemma, in Soundness]
SoundnessProof.Pmods_mono [lemma, in Soundness]
SoundnessProof.Pmods_mono0 [lemma, in Soundness]
SoundnessProof.Pp [definition, in Soundness]
SoundnessProof.p_ind [definition, in Soundness]
SoundnessProof.soundness [definition, in Soundness]
SoundnessProof.soundnessTheorem [lemma, in Soundness]
SoundnessProof.stuck_n [definition, in Soundness]
SoundnessProof.TheTarskiParams.is_lub [definition, in Soundness]
SoundnessProof.TheTarskiParams.L [definition, in Soundness]
SoundnessProof.TheTarskiParams.le [definition, in Soundness]
SoundnessProof.TheTarskiParams.le_trans [lemma, in Soundness]
SoundnessProof.TheTarskiParams.lub [definition, in Soundness]
SoundnessProof.TheTarskiParams.lub_is_lub [lemma, in Soundness]
SoundnessProof.TheTarskiParams.ub [definition, in Soundness]
Spec [module, in ProofSystem]
Spec.funtypemap [axiom, in ProofSystem]
stepresult [inductive, in Language]
store [definition, in Language]
store_lookup [definition, in Language]
store_lookup_store_update_diff [lemma, in ProofSystemFacts]
store_lookup_store_update_same [lemma, in ProofSystemFacts]
store_update [definition, in Language]
string_of_num [axiom, in Language]
string_of_num_of_string [axiom, in Language]
Stuck [constructor, in Language]
T
Tarski [module, in Tarski]TarskiParams [module, in Tarski]
TarskiParams.is_lub [definition, in Tarski]
TarskiParams.L [axiom, in Tarski]
TarskiParams.le [axiom, in Tarski]
TarskiParams.le_trans [axiom, in Tarski]
TarskiParams.lub [axiom, in Tarski]
TarskiParams.lub_is_lub [axiom, in Tarski]
TarskiParams.ub [definition, in Tarski]
Tarski.fp [definition, in Tarski]
Tarski.Tarski [section, in Tarski]
Tarski.Tarski.f [variable, in Tarski]
Tarski.Tarski.mono [variable, in Tarski]
Tarski.tarski_left [lemma, in Tarski]
Tarski.tarski_right [lemma, in Tarski]
Test [module, in ExampleProgram]
Test2 [module, in ExampleProgram]
TheProofSystem [module, in Soundness]
TheProofSystem [module, in Soundness]
TheProofSystem [module, in ProofSystemFacts]
TheProofSystem [module, in ExampleProof]
TheProofSystemFacts [module, in ExampleProof]
TheProofSystemFacts [module, in Soundness]
TheSemantics [module, in Soundness]
TheTarski [module, in Soundness]
TheTarskiParams [module, in Soundness]
try_assoc [definition, in Assoc]
U
Unload [constructor, in Language]update [definition, in Assoc]
V
value [inductive, in Language]var [definition, in Language]
VarExpr [constructor, in Language]
vlambda [definition, in Language]
vlambda_vnum [lemma, in ProofSystemFacts]
vlambda_vnum_easy [lemma, in ProofSystemFacts]
vmodulename [definition, in Language]
vnum [definition, in Language]
\
\Assoc [library]\ExampleProgram [library]
\ExampleProof [library]
\ExampleSpec [library]
\Language [library]
\ProofSystem [library]
\ProofSystemFacts [library]
\Soundness [library]
\Tarski [library]
Lemma Index
A
alloc_sep [in ProofSystemFacts]asn_mono_conj [in ProofSystemFacts]
asn_mono_sep [in ProofSystemFacts]
C
conj_sep_pure_left [in ProofSystemFacts]conj_sep_pure_right [in ProofSystemFacts]
D
dontcare_sep [in ProofSystemFacts]dummy_pointstos_dealloc [in ProofSystemFacts]
dummy_pointstos_intuit [in ProofSystemFacts]
E
exists_sep_left [in ProofSystemFacts]H
heap_contains_heap_try_lookup [in ProofSystemFacts]heap_try_lookup_app_left [in ProofSystemFacts]
heap_try_lookup_app_right [in ProofSystemFacts]
heap_try_lookup_heap_remove [in ProofSystemFacts]
heap_try_lookup_heap_remove_diff [in ProofSystemFacts]
heap_try_lookup_heap_remove_same [in ProofSystemFacts]
heap_try_lookup_heap_update_diff [in ProofSystemFacts]
heap_try_lookup_heap_update_same [in ProofSystemFacts]
I
is_split_assoc_left [in ProofSystemFacts]is_split_commut [in ProofSystemFacts]
is_split_dealloc_left [in ProofSystemFacts]
is_split_dealloc_right [in ProofSystemFacts]
is_split_heap_remove [in ProofSystemFacts]
is_split_heap_try_lookup_left [in ProofSystemFacts]
is_split_heap_update_left [in ProofSystemFacts]
is_split_nil_left [in ProofSystemFacts]
M
map_compos [in ProofSystemFacts]mymainNotStuck [in ExampleProof]
MyModuleMapValid.disposeFunc_valid [in ExampleProof]
MyModuleMapValid.incrFunc_valid [in ExampleProof]
MyModuleMapValid.main_valid [in ExampleProof]
MyModuleMapValid.modules_valid [in ExampleProof]
MyModuleMapValid.myIncrLib_valid [in ExampleProof]
N
nat_of_Z_of_nat [in ProofSystemFacts]NoDup_map_store_lookup_combine [in ProofSystemFacts]
notIn_map_store_lookup [in ProofSystemFacts]
P
pointstos'_dontcare [in ProofSystemFacts]pointstos'_intuit [in ProofSystemFacts]
pointstos_intuit [in ProofSystemFacts]
pointstos_sep [in ProofSystemFacts]
ProofSystemFacts.asn_mono_asn_true [in ProofSystemFacts]
ProofSystemFacts.dummy_pointstos_dontcare [in ProofSystemFacts]
ProofSystemFacts.module0_dontcare [in ProofSystemFacts]
ProofSystemFacts.module_dontcare [in ProofSystemFacts]
S
Semantics.nsteps_assoc [in Language]sep_assoc_left [in ProofSystemFacts]
sep_assoc_right [in ProofSystemFacts]
sep_commut [in ProofSystemFacts]
sep_conj_pure_left [in ProofSystemFacts]
sep_exists_left [in ProofSystemFacts]
sep_mono [in ProofSystemFacts]
sep_pure_left [in ProofSystemFacts]
sep_pure_right_destruct [in ProofSystemFacts]
sep_stores [in ProofSystemFacts]
sep_stores_backward [in ProofSystemFacts]
SoundnessProof.asn_mono_Fn_mono [in Soundness]
SoundnessProof.asn_true_mono [in Soundness]
SoundnessProof.Fn_mono [in Soundness]
SoundnessProof.HCAssign [in Soundness]
SoundnessProof.HCCall [in Soundness]
SoundnessProof.HCCons [in Soundness]
SoundnessProof.HCConseq [in Soundness]
SoundnessProof.HCDispose [in Soundness]
SoundnessProof.HCExists [in Soundness]
SoundnessProof.HCFalse [in Soundness]
SoundnessProof.HCFrame [in Soundness]
SoundnessProof.HCIfEq [in Soundness]
SoundnessProof.HCLoad [in Soundness]
SoundnessProof.HCLookup [in Soundness]
SoundnessProof.HCMutate [in Soundness]
SoundnessProof.HCSeq [in Soundness]
SoundnessProof.HCUnload [in Soundness]
SoundnessProof.HPCombine [in Soundness]
SoundnessProof.HPFold [in Soundness]
SoundnessProof.HPFunType [in Soundness]
SoundnessProof.HPTrue [in Soundness]
SoundnessProof.HPUnfold [in Soundness]
SoundnessProof.Jdef_mono [in Soundness]
SoundnessProof.Jfix_fold [in Soundness]
SoundnessProof.Jfix_mono [in Soundness]
SoundnessProof.Jfix_unfold [in Soundness]
SoundnessProof.Pmods_all [in Soundness]
SoundnessProof.Pmods_mono [in Soundness]
SoundnessProof.Pmods_mono0 [in Soundness]
SoundnessProof.soundnessTheorem [in Soundness]
SoundnessProof.TheTarskiParams.le_trans [in Soundness]
SoundnessProof.TheTarskiParams.lub_is_lub [in Soundness]
store_lookup_store_update_diff [in ProofSystemFacts]
store_lookup_store_update_same [in ProofSystemFacts]
T
Tarski.tarski_left [in Tarski]Tarski.tarski_right [in Tarski]
V
vlambda_vnum [in ProofSystemFacts]vlambda_vnum_easy [in ProofSystemFacts]
Section Index
A
Assoc [in Assoc]T
Tarski.Tarski [in Tarski]Constructor Index
A
AddExpr [in Language]AndAsn [in ProofSystem]
ApplyAsn [in ProofSystem]
Assign [in Language]
B
BadSeed [in Language]C
Call [in Language]Closure [in ProofSystem]
Cons [in Language]
D
Dispose [in Language]Done [in Language]
E
EqAsn [in ProofSystem]ExistsAsn [in ProofSystem]
F
FunTypeAsn [in ProofSystem]FunTypeDef [in ProofSystem]
I
IfEq [in Language]L
LAdd [in ProofSystem]Lambda [in Language]
LambdaV [in Language]
LibAsn [in ProofSystem]
Lit [in Language]
LLambda [in ProofSystem]
LLit [in ProofSystem]
Load [in Language]
Lookup [in Language]
LVar [in ProofSystem]
M
ModuleAsn [in ProofSystem]ModuleNameV [in Language]
Module0Asn [in ProofSystem]
Mutate [in Language]
N
NewConfig [in Language]NumV [in Language]
P
PointsTo [in ProofSystem]ProofSystem.CAssign [in ProofSystem]
ProofSystem.CCall [in ProofSystem]
ProofSystem.CCons [in ProofSystem]
ProofSystem.CConseq [in ProofSystem]
ProofSystem.CDispose [in ProofSystem]
ProofSystem.CExists [in ProofSystem]
ProofSystem.CFalse [in ProofSystem]
ProofSystem.CFrame [in ProofSystem]
ProofSystem.CIfEq [in ProofSystem]
ProofSystem.CLoad [in ProofSystem]
ProofSystem.CLookup [in ProofSystem]
ProofSystem.CMutate [in ProofSystem]
ProofSystem.CSeq [in ProofSystem]
ProofSystem.CUnload [in ProofSystem]
ProofSystem.PCombine [in ProofSystem]
ProofSystem.PFold [in ProofSystem]
ProofSystem.PFunType [in ProofSystem]
ProofSystem.PTrue [in ProofSystem]
ProofSystem.PUnfold [in ProofSystem]
PVar [in ProofSystem]
R
Ret [in Language]S
Sep [in ProofSystem]Seq [in Language]
SeqC [in Language]
Stuck [in Language]
U
Unload [in Language]V
VarExpr [in Language]Inductive Index
A
asn [in ProofSystem]C
closure [in ProofSystem]cmd [in Language]
cont [in Language]
E
expr [in Language]F
funtypedef [in ProofSystem]L
lambda [in Language]lexpr [in ProofSystem]
P
ProofSystem.correct [in ProofSystem]ProofSystem.provable [in ProofSystem]
S
stepresult [in Language]V
value [in Language]Definition Index
A
alloc [in Language]asn_mono [in ProofSystem]
assigns [in ProofSystem]
assoc [in Assoc]
C
closure_interp [in ProofSystem]config [in Language]
D
dealloc [in Language]dontcare [in ProofSystem]
dummy_pointstos [in ProofSystem]
E
eval [in Language]F
funtype [in Language]funtype_interp [in ProofSystem]
H
heap [in Language]heap_contains [in Language]
heap_remove [in Language]
heap_try_lookup [in Language]
heap_update [in Language]
I
intuit [in ProofSystemFacts]is_split [in ProofSystem]
L
leval [in ProofSystem]lstore [in ProofSystem]
lvar [in ProofSystem]
M
mem_assoc [in Assoc]moduledef [in Language]
ModuleMap.modules_try_lookup [in Language]
modulename [in Language]
mymain [in ExampleProgram]
MyModuleMapValid.Qbody [in ExampleProof]
MyModuleMapValid.Qclosure [in ExampleProof]
MyModuleMap.disposeFunc [in ExampleProgram]
MyModuleMap.getIncrFunc [in ExampleProgram]
MyModuleMap.incrFunc [in ExampleProgram]
MyModuleMap.modules [in ExampleProgram]
MyModuleMap.modules_try_lookup [in ExampleProgram]
MyModuleMap2.modules [in ExampleProgram]
MyModuleMap2.modules_try_lookup [in ExampleProgram]
MySpec.funtypemap [in ExampleSpec]
P
pointstos [in ProofSystem]pointstos' [in ProofSystem]
ProofSystem.asn_true [in ProofSystem]
ProofSystem.command_valid [in ProofSystem]
ProofSystem.funtype_try_lookup [in ProofSystem]
ProofSystem.lib [in ProofSystem]
ProofSystem.module [in ProofSystem]
ProofSystem.module0 [in ProofSystem]
ProofSystem.module_valid [in ProofSystem]
pure [in ProofSystem]
R
remove [in Assoc]S
sasn [in ProofSystem]seed [in Language]
Semantics.nsteps [in Language]
Semantics.step [in Language]
sep [in ProofSystem]
SoundnessProof.c_ind [in Soundness]
SoundnessProof.Fn [in Soundness]
SoundnessProof.Jdef [in Soundness]
SoundnessProof.Jfix [in Soundness]
SoundnessProof.Pc [in Soundness]
SoundnessProof.Pmods [in Soundness]
SoundnessProof.Pp [in Soundness]
SoundnessProof.p_ind [in Soundness]
SoundnessProof.soundness [in Soundness]
SoundnessProof.stuck_n [in Soundness]
SoundnessProof.TheTarskiParams.is_lub [in Soundness]
SoundnessProof.TheTarskiParams.L [in Soundness]
SoundnessProof.TheTarskiParams.le [in Soundness]
SoundnessProof.TheTarskiParams.lub [in Soundness]
SoundnessProof.TheTarskiParams.ub [in Soundness]
store [in Language]
store_lookup [in Language]
store_update [in Language]
T
TarskiParams.is_lub [in Tarski]TarskiParams.ub [in Tarski]
Tarski.fp [in Tarski]
try_assoc [in Assoc]
U
update [in Assoc]V
var [in Language]vlambda [in Language]
vmodulename [in Language]
vnum [in Language]
Module Index
M
ModuleMap [in Language]ModuleMapValid [in Soundness]
MyModuleMap [in ExampleProgram]
MyModuleMapValid [in ExampleProof]
MyModuleMap2 [in ExampleProgram]
MySemantics [in ExampleProgram]
MySemantics [in ExampleProgram]
MySoundness [in ExampleProof]
MySpec [in ExampleSpec]
P
ProofSystem [in ProofSystem]ProofSystemFacts [in ProofSystemFacts]
S
Semantics [in Language]SoundnessProof [in Soundness]
Spec [in ProofSystem]
T
Tarski [in Tarski]TarskiParams [in Tarski]
Test [in ExampleProgram]
Test2 [in ExampleProgram]
TheProofSystem [in Soundness]
TheProofSystem [in Soundness]
TheProofSystem [in ProofSystemFacts]
TheProofSystem [in ExampleProof]
TheProofSystemFacts [in ExampleProof]
TheProofSystemFacts [in Soundness]
TheSemantics [in Soundness]
TheTarski [in Soundness]
TheTarskiParams [in Soundness]
Axiom Index
C
closure_of_num [in ProofSystem]closure_of_num_of_closure [in ProofSystem]
L
lambda_of_num [in Language]lambda_of_num_of_lambda [in Language]
M
ModuleMapValid.modules_valid [in Soundness]ModuleMap.modules [in Language]
N
num_of_closure [in ProofSystem]num_of_lambda [in Language]
num_of_lambda_of_num [in Language]
num_of_string [in Language]
num_of_string_of_num [in Language]
S
Spec.funtypemap [in ProofSystem]string_of_num [in Language]
string_of_num_of_string [in Language]
T
TarskiParams.L [in Tarski]TarskiParams.le [in Tarski]
TarskiParams.le_trans [in Tarski]
TarskiParams.lub [in Tarski]
TarskiParams.lub_is_lub [in Tarski]
Variable Index
A
Assoc.A [in Assoc]Assoc.B [in Assoc]
Assoc.eq [in Assoc]
T
Tarski.Tarski.f [in Tarski]Tarski.Tarski.mono [in Tarski]
Library Index
\
\Assoc\ExampleProgram
\ExampleProof
\ExampleSpec
\Language
\ProofSystem
\ProofSystemFacts
\Soundness
\Tarski
| 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 | \ | _ | (305 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 | _ | (92 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 | _ | (2 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 | _ | (59 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 | _ | (12 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 | _ | (80 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 | _ | (27 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 | _ | (19 entries) | |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | (5 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 | \ | _ | (9 entries) |
This page has been generated by coqdoc