| 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 |
_ |
(1098 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 |
_ |
(53 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 |
_ |
(408 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 |
_ |
(132 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 |
_ |
(59 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 |
_ |
(404 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 |
_ |
(14 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 |
_ |
(28 entries) |
Global Index
A
A [definition, in CTPC.Dict]
A [axiom, in CTPC.Dict]
A [axiom, in CTPC.Dict]
A [definition, in CTPC.Flat]
A [definition, in CTPC.Dict]
AACons [constructor, in CTPC.Alloc]
AANil [constructor, in CTPC.Alloc]
AApply [constructor, in CTPC.Alloc]
aargs [inductive, in CTPC.Alloc]
aargsDenote [definition, in CTPC.Alloc]
aargsDenote_len [lemma, in CTPC.Flatify]
aargsTy [definition, in CTPC.Alloc]
aBind [definition, in CTPC.AllocMonad]
ABind [constructor, in CTPC.Alloc]
ABindB [constructor, in CTPC.Allocify]
aBind_backward [lemma, in CTPC.AllocMonad]
aBind_forward [lemma, in CTPC.AllocMonad]
aBottom [definition, in CTPC.AllocMonad]
ACode [constructor, in CTPC.Alloc]
ACodeptr [constructor, in CTPC.Alloc]
AConst [constructor, in CTPC.Alloc]
adom [definition, in CTPC.Alloc]
AFBody [constructor, in CTPC.Alloc]
AFinal [constructor, in CTPC.Allocify]
AFLam [constructor, in CTPC.Alloc]
aformalsDenote [definition, in CTPC.Alloc]
aFrame [lemma, in CTPC.AllocMonad]
afunc [inductive, in CTPC.Alloc]
afuncBody [definition, in CTPC.Flatify]
afuncBody_sound [lemma, in CTPC.Flatify]
afuncDenote [definition, in CTPC.Alloc]
afuncTy [definition, in CTPC.Alloc]
alinear [inductive, in CTPC.Alloc]
alinearDenote [definition, in CTPC.Alloc]
alinearTy [definition, in CTPC.Alloc]
AllF [inductive, in LambdaTamer.ListT]
AllF_cons [constructor, in LambdaTamer.ListT]
AllF_nil [constructor, in LambdaTamer.ListT]
AllF_prover [lemma, in LambdaTamer.ListT]
Alloc [library]
allocArgs [definition, in CTPC.Allocify]
allocArgs_sound [lemma, in CTPC.Allocify]
allocCode [definition, in CTPC.Allocify]
allocCode_body_var [lemma, in CTPC.Allocify]
allocCode_body_var' [lemma, in CTPC.Allocify]
allocCode_bound [lemma, in CTPC.Allocify]
allocCode_nth [lemma, in CTPC.Allocify]
allocCode_nth_revAppN [lemma, in CTPC.Allocify]
allocCode_nth_revAppN' [lemma, in CTPC.Allocify]
allocCode_nth_ts [lemma, in CTPC.Allocify]
allocCode_nth_ts' [lemma, in CTPC.Allocify]
allocCode_push [lemma, in CTPC.Allocify]
allocCode_push' [lemma, in CTPC.Allocify]
allocCode_soundness [definition, in CTPC.Allocify]
allocCode_zero [lemma, in CTPC.Allocify]
allocCode_zero' [lemma, in CTPC.Allocify]
allocFunc [definition, in CTPC.Allocify]
allocFuncs [definition, in CTPC.Allocify]
allocFuncs_sound [lemma, in CTPC.Allocify]
allocFuncTys [definition, in CTPC.Allocify]
allocFunc_sound [lemma, in CTPC.Allocify]
Allocify [library]
allocLinear [definition, in CTPC.Allocify]
allocLinear_sound [lemma, in CTPC.Allocify]
allocM [definition, in CTPC.AllocMonad]
AllocMonad [library]
allocPrimop [definition, in CTPC.Allocify]
allocPrimop_sound [lemma, in CTPC.Allocify]
allocProg [definition, in CTPC.Allocify]
allocProg_body_sound [lemma, in CTPC.Allocify]
allocProg_funcs_soundness [lemma, in CTPC.Allocify]
allocProg_funcs_var [lemma, in CTPC.Allocify]
allocProg_funcs_var' [lemma, in CTPC.Allocify]
allocProg_sound [lemma, in CTPC.Allocify]
allocProj [definition, in CTPC.Allocify]
allocProj_sound [lemma, in CTPC.Allocify]
allocSpec [definition, in CTPC.AllocMonad]
allocTy [definition, in CTPC.Allocify]
allocTys [definition, in CTPC.Allocify]
allocVar [definition, in CTPC.Allocify]
allocVar' [definition, in CTPC.Allocify]
allocVar'_sound [lemma, in CTPC.Allocify]
allocVar_sound [lemma, in CTPC.Allocify]
allocVar_sound_lr [lemma, in CTPC.Allocify]
AllS2 [definition, in CTPC.Asm]
AllS2_len [lemma, in CTPC.Asmify]
all_elemT [definition, in LambdaTamer.AutoSyntax]
amakeTrace [definition, in CTPC.Alloc]
amakeTrace_unfold_external [lemma, in CTPC.Alloc]
amakeTrace_unfold_internal [lemma, in CTPC.Alloc]
ANat [constructor, in CTPC.Alloc]
ANew [constructor, in CTPC.Alloc]
aNew [definition, in CTPC.AllocMonad]
aNew_forward [lemma, in CTPC.AllocMonad]
appBinders_comm [lemma, in LambdaTamer.AutoSyntax]
appCfuncs [definition, in CTPC.CCify]
appF [definition, in LambdaTamer.ListT]
appSubst [definition, in LambdaTamer.Binding]
appSubstF [definition, in LambdaTamer.AutoSyntax]
appSubstF_liftSubst' [lemma, in LambdaTamer.AutoSyntax]
appSubstF_strengthen [lemma, in LambdaTamer.AutoSyntax]
appSubst_appSubstF [lemma, in LambdaTamer.AutoSyntax]
appSubst_assoc [lemma, in LambdaTamer.Binding]
appSubst_assoc' [lemma, in LambdaTamer.Binding]
appSubst_decomp [lemma, in LambdaTamer.Binding]
appSubst_liftSubst' [lemma, in LambdaTamer.Binding]
appSubst_nil [lemma, in LambdaTamer.Binding]
appSubst_nil' [lemma, in LambdaTamer.Binding]
appT [definition, in LambdaTamer.ListT]
appT [definition, in LambdaTamer.AutoSyntax]
app_length [lemma, in LambdaTamer.ListUtil]
app_middle [lemma, in LambdaTamer.ListUtil]
app_nil_middle [lemma, in LambdaTamer.ListUtil]
aprimop [inductive, in CTPC.Alloc]
aprimopB [inductive, in CTPC.Allocify]
aprimopBDenote [definition, in CTPC.Allocify]
aprimopDenote [definition, in CTPC.Alloc]
aprimopTy [definition, in CTPC.Alloc]
aprog [inductive, in CTPC.Alloc]
aprogDenote [definition, in CTPC.Alloc]
AProj [constructor, in CTPC.Alloc]
aRead [definition, in CTPC.AllocMonad]
aRead_forward [lemma, in CTPC.AllocMonad]
ARef [constructor, in CTPC.Alloc]
aReturn [definition, in CTPC.AllocMonad]
aReturn_forward [lemma, in CTPC.AllocMonad]
argsDenote [definition, in CTPC.Asm]
argsDenote_len [lemma, in CTPC.Asmify]
args_bound [definition, in CTPC.Flatify]
args_bound_early [lemma, in CTPC.Flatify]
args_early [definition, in CTPC.Flatify]
args_early_monotone [lemma, in CTPC.Flatify]
args_lr [definition, in CTPC.Asmify]
args_lr [definition, in CTPC.Allocify]
args_lr [definition, in CTPC.CCify]
args_lr [definition, in CTPC.Flatify]
args_lr_vals_lr [lemma, in CTPC.Allocify]
args_max [definition, in CTPC.Flatify]
args_max_early [lemma, in CTPC.Flatify]
Asm [library]
asmArgs [definition, in CTPC.Asmify]
asmArgs_sound [lemma, in CTPC.Asmify]
Asmify [library]
asmLinear [definition, in CTPC.Asmify]
asmLinear_sound [lemma, in CTPC.Asmify]
asmPrimop [definition, in CTPC.Asmify]
asmPrimop_sound [lemma, in CTPC.Asmify]
asmProg [definition, in CTPC.Asmify]
asmProg_sound [lemma, in CTPC.Asmify]
asmTrace_sound [lemma, in CTPC.Asmify]
asmTrace_sound' [lemma, in CTPC.Asmify]
Assign [constructor, in CTPC.Asm]
aty [inductive, in CTPC.Alloc]
atyDenote [definition, in CTPC.Alloc]
atys [definition, in CTPC.Alloc]
atys_eq_dec [definition, in CTPC.Alloc]
aty_eq_dec [definition, in CTPC.Alloc]
augmentSubst [definition, in CTPC.Flatify]
AutoSyntax [library]
AVar [constructor, in CTPC.Alloc]
A_eq_dec [axiom, in CTPC.Dict]
A_eq_dec [definition, in CTPC.Flat]
B
Bind [constructor, in LambdaTamer.Computation]
bindCfunc [definition, in CTPC.CCify]
bindCfunc_sound [lemma, in CTPC.CCify]
Binding [library]
buildEnv [definition, in CTPC.CCify]
buildEnv' [definition, in CTPC.CCify]
buildEnv'_sound [lemma, in CTPC.CCify]
buildEnv_apply [lemma, in CTPC.CCify]
C
CACons [constructor, in CTPC.CC]
Call [constructor, in CTPC.Trace]
CallShape [constructor, in CTPC.Trace]
call_precondition [lemma, in CTPC.Flatify]
CANil [constructor, in CTPC.CC]
CApply [constructor, in CTPC.CC]
cargs [inductive, in CTPC.CC]
cargsDenote [definition, in CTPC.CC]
cargsDenote_app_nil [lemma, in CTPC.CCify]
cast_app [lemma, in LambdaTamer.Binding]
cast_CFCons [lemma, in CTPC.CCify]
cast_cons [lemma, in LambdaTamer.Binding]
cast_SCons_head [lemma, in LambdaTamer.Binding]
cast_SCons_tail [lemma, in LambdaTamer.Binding]
CBind [constructor, in CTPC.CC]
CBool [constructor, in examples.CPS]
CC [library]
CCall [constructor, in examples.CPS]
ccArgs [definition, in CTPC.CCify]
CCify [library]
ccLinear_sound [lemma, in CTPC.CCify]
CClosure [constructor, in CTPC.CC]
CCode [constructor, in CTPC.CC]
CConst [constructor, in CTPC.CC]
CConst [constructor, in examples.CPS]
CCont [constructor, in CTPC.CC]
CCont [constructor, in examples.CPS]
ccPrimop [definition, in CTPC.CCify]
ccTy [definition, in CTPC.CCify]
ccTys [definition, in CTPC.CCify]
ccTySmall [lemma, in CTPC.CCify]
ccTysSmall [lemma, in CTPC.CCify]
ccTysViSmall [lemma, in CTPC.CCify]
cc_lr [lemma, in CTPC.Compile]
cexp [inductive, in examples.CPS]
cexpDenote [definition, in examples.CPS]
CFBody [constructor, in CTPC.CC]
CFCons [constructor, in CTPC.CC]
cfhead [definition, in CTPC.CCify]
CFLam [constructor, in CTPC.CC]
CFNil [constructor, in CTPC.CC]
cfprog [definition, in CTPC.CCify]
cfprogDenote [definition, in CTPC.CCify]
CFst [constructor, in examples.CPS]
cfunc [inductive, in CTPC.CC]
cfuncDenote [definition, in CTPC.CC]
cfuncs [inductive, in CTPC.CC]
cfuncsDenote [definition, in CTPC.CC]
cfuncs_larges [lemma, in CTPC.Allocify]
cfuncTyDenote [definition, in CTPC.CC]
checkTag [definition, in CTPC.Alloc]
CLam [constructor, in examples.CPS]
CLet [constructor, in examples.CPS]
clinear [inductive, in CTPC.CC]
clinearDenote [definition, in CTPC.CC]
close [definition, in CTPC.CCify]
close' [definition, in CTPC.CCify]
close'' [definition, in CTPC.CCify]
close''_sound [lemma, in CTPC.CCify]
close'_sound [lemma, in CTPC.CCify]
close_sound [lemma, in CTPC.CCify]
closureVar_sound [lemma, in CTPC.CCify]
CNat [constructor, in CTPC.CC]
Compile [library]
compile_correct [lemma, in CTPC.Compile]
compile_slots_lr [lemma, in CTPC.Compile]
compile_term [definition, in CTPC.Compile]
compile_term' [definition, in CTPC.Compile]
compose [definition, in CTPC.CPSify]
compose_sound [lemma, in CTPC.CPSify]
computation [inductive, in LambdaTamer.Computation]
Computation [library]
con [inductive, in LambdaTamer.AutoSyntax]
cons [definition, in LambdaTamer.AutoSyntax]
cons [axiom, in LambdaTamer.AutoSyntax]
cons [definition, in LambdaTamer.AutoSyntax]
cons [axiom, in LambdaTamer.AutoSyntax]
consF [constructor, in LambdaTamer.ListT]
consI [definition, in LambdaTamer.ListUtil]
conSig [definition, in LambdaTamer.AutoSyntax]
consS [definition, in LambdaTamer.ListT]
Const [constructor, in CTPC.Asm]
consT [constructor, in LambdaTamer.ListT]
Construct [constructor, in LambdaTamer.AutoSyntax]
Cont [library]
Contify [library]
contifyLinear [definition, in CTPC.Contify]
contifyLinear_sound [lemma, in CTPC.Contify]
contifyPrimop [definition, in CTPC.Contify]
contifyTy [definition, in CTPC.Contify]
Continuation [library]
contTy [definition, in examples.CPS]
cont_lr [definition, in CTPC.CCify]
cont_lr [lemma, in CTPC.Compile]
con_builder [definition, in LambdaTamer.AutoSyntax]
con_ih [definition, in LambdaTamer.AutoSyntax]
copy [definition, in CTPC.Flatify]
copySlots [definition, in CTPC.Flatify]
copySlots_late [lemma, in CTPC.Flatify]
copySlots_sound [lemma, in CTPC.Flatify]
copyType [definition, in CTPC.Flatify]
copyType_late [lemma, in CTPC.Flatify]
copyType_sound [lemma, in CTPC.Flatify]
copy_bound [definition, in CTPC.Safety]
copy_bounded [lemma, in CTPC.Safety]
copy_bound_has [lemma, in CTPC.Safety]
copy_bound_mono [lemma, in CTPC.Safety]
copy_soundness [lemma, in CTPC.Flatify]
CPair [constructor, in examples.CPS]
CPFst [constructor, in CTPC.CC]
cpprog [definition, in CTPC.CCify]
cpprogDenote [definition, in CTPC.CCify]
cprimexp [inductive, in examples.CPS]
cprimexpDenote [definition, in examples.CPS]
cprimop [inductive, in CTPC.CC]
cprimopDenote [definition, in CTPC.CC]
CProd [constructor, in examples.CPS]
CProd [constructor, in CTPC.CC]
cprog [definition, in CTPC.CC]
cprogDenote [definition, in CTPC.CC]
CProj [constructor, in CTPC.CC]
cproj [inductive, in CTPC.CC]
cprojDenote [definition, in CTPC.CC]
cprojTy [inductive, in CTPC.CC]
cprojTyDenote [definition, in CTPC.CC]
cps [definition, in CTPC.CPSify]
CPS [library]
CPS [library]
CPSify [library]
CPSnd [constructor, in CTPC.CC]
cpsTerm [definition, in examples.CPS]
cpsTerm_sound [lemma, in examples.CPS]
cpsTerm_sound_bool [lemma, in examples.CPS]
cpsTy [definition, in examples.CPS]
cps_sound [lemma, in CTPC.CPSify]
Crash [constructor, in CTPC.Trace]
CrashShape [constructor, in CTPC.Trace]
cresultDenote [definition, in CTPC.CC]
CSnd [constructor, in examples.CPS]
cty [inductive, in examples.CPS]
cty [inductive, in CTPC.CC]
ctyDenote [definition, in examples.CPS]
ctyDenote [definition, in CTPC.CC]
ctys [definition, in CTPC.CC]
ctysDenote [definition, in CTPC.CC]
ctysDenote_tail [definition, in CTPC.CCify]
ctysDenote_tail' [definition, in CTPC.CCify]
ctysDenote_tail'' [definition, in CTPC.CCify]
ctysSubst [definition, in CTPC.CC]
cty_ind' [definition, in CTPC.Allocify]
CVar [constructor, in CTPC.CC]
CVar [constructor, in examples.CPS]
cwithProg [inductive, in CTPC.CC]
cwithProgDenote [definition, in CTPC.CC]
D
default [definition, in CTPC.Dict]
default [axiom, in CTPC.Dict]
Denote [module, in LambdaTamer.AutoSyntax]
Denote [module, in LambdaTamer.AutoSyntax]
DENOTE_PARAM [module, in LambdaTamer.AutoSyntax]
DENOTE_PARAM [module, in LambdaTamer.AutoSyntax]
DENOTE_RESULT [module, in LambdaTamer.AutoSyntax]
DENOTE_RESULT [module, in LambdaTamer.AutoSyntax]
DICT [module, in CTPC.Dict]
dict [axiom, in CTPC.Dict]
dict [definition, in CTPC.Dict]
Dict [module, in CTPC.Dict]
Dict [library]
DICT_DOMAIN [module, in CTPC.Dict]
dict_eq_dec [axiom, in CTPC.Dict]
dict_eq_dec [definition, in CTPC.Dict]
drop [definition, in LambdaTamer.ListUtil]
dty [definition, in LambdaTamer.AutoSyntax]
dty [definition, in LambdaTamer.AutoSyntax]
dtyDenote [axiom, in LambdaTamer.AutoSyntax]
dtyDenote [axiom, in LambdaTamer.AutoSyntax]
dtyDenote [definition, in LambdaTamer.AutoSyntax]
dtyDenote [axiom, in LambdaTamer.AutoSyntax]
dtyDenote [definition, in LambdaTamer.AutoSyntax]
dtyDenote [definition, in LambdaTamer.AutoSyntax]
dtyDenote [axiom, in LambdaTamer.AutoSyntax]
E
early_bump [lemma, in CTPC.Flatify]
elemify [definition, in LambdaTamer.AutoSyntax]
elemT [inductive, in LambdaTamer.ListT]
elemT_absurd [definition, in LambdaTamer.ListT]
elemT_invert [lemma, in LambdaTamer.ListT]
elemT_invert' [lemma, in LambdaTamer.ListT]
elemT_split [lemma, in LambdaTamer.ListT]
embed [definition, in LambdaTamer.Binding]
embed' [definition, in LambdaTamer.Binding]
embed'_sound [lemma, in LambdaTamer.Binding]
embed_sound [lemma, in LambdaTamer.Binding]
empty [definition, in CTPC.Dict]
empty [axiom, in CTPC.Dict]
empty_inj [axiom, in CTPC.Dict]
empty_inj [lemma, in CTPC.Dict]
enT [definition, in LambdaTamer.AutoSyntax]
equations [axiom, in LambdaTamer.AutoSyntax]
equations [axiom, in LambdaTamer.AutoSyntax]
equations_type [definition, in LambdaTamer.AutoSyntax]
eq_app [definition, in LambdaTamer.Binding]
eq_cons [definition, in LambdaTamer.Binding]
eq_rect_ident [lemma, in LambdaTamer.ListT]
eq_rect_reverse [lemma, in LambdaTamer.ListT]
eq_rect_r_ident [lemma, in LambdaTamer.ListT]
eq_rec_r_ident [lemma, in LambdaTamer.ListT]
erase [inductive, in LambdaTamer.Computation]
EraseBind [constructor, in LambdaTamer.Computation]
EraseDrop [constructor, in LambdaTamer.Computation]
EraseReturn [constructor, in LambdaTamer.Computation]
etaF [definition, in LambdaTamer.AutoSyntax]
etaF_eq [lemma, in LambdaTamer.AutoSyntax]
etaT [lemma, in LambdaTamer.AutoSyntax]
exp_lr [definition, in CTPC.CPSify]
Ext [library]
extendSubst [definition, in LambdaTamer.AutoSyntax]
extend_app [lemma, in LambdaTamer.AutoSyntax]
ext_eq [lemma, in LambdaTamer.Ext]
ext_eqT [lemma, in LambdaTamer.Ext]
ext_eq_dep [lemma, in LambdaTamer.Ext]
ext_eq_Type [axiom, in LambdaTamer.Ext]
F
FACons [constructor, in CTPC.Flat]
FANil [constructor, in CTPC.Flat]
fargs [inductive, in CTPC.Flat]
fargsDenote [definition, in CTPC.Flat]
fargsDenote_len [lemma, in CTPC.Flatify]
fargs_bounded [definition, in CTPC.Safety]
fargs_bounded_mono [lemma, in CTPC.Safety]
fargs_bounded_mono' [lemma, in CTPC.Safety]
fargs_safe [lemma, in CTPC.Safety]
fields_backup [lemma, in CTPC.Asmify]
First [constructor, in LambdaTamer.Binding]
firstT [constructor, in LambdaTamer.ListT]
FJump [constructor, in CTPC.Flat]
Flat [library]
flatArgs [definition, in CTPC.Flatify]
flatArgs_bounded [lemma, in CTPC.Safety]
flatArgs_sound [lemma, in CTPC.Flatify]
flatCall [definition, in CTPC.Flatify]
flatCall_lemma [lemma, in CTPC.Flatify]
flatCall_sel [lemma, in CTPC.Flatify]
flatContext [definition, in CTPC.Flat]
flatContext' [definition, in CTPC.Flat]
flatContext_inj [lemma, in CTPC.Safety]
flatContext_late [lemma, in CTPC.Asmify]
flatContext_revApp_inj [lemma, in CTPC.Safety]
flatContext_sel [lemma, in CTPC.Safety]
flatContext_sel' [lemma, in CTPC.Safety]
flatContext_sel'' [lemma, in CTPC.Safety]
flatContext_sel_direct [lemma, in CTPC.Asmify]
flatFunc [definition, in CTPC.Flatify]
flatFunc_bounded [lemma, in CTPC.Safety]
Flatify [library]
flatLinear [definition, in CTPC.Flatify]
flatLinear_bounded [lemma, in CTPC.Safety]
flatLinear_sound [lemma, in CTPC.Flatify]
flatPrimop [definition, in CTPC.Flatify]
flatPrimop_bounded [lemma, in CTPC.Safety]
flatPrimop_sound [lemma, in CTPC.Flatify]
flatProg [definition, in CTPC.Flatify]
flatProg_body_bounded [lemma, in CTPC.Safety]
flatProg_funcs_bounded [lemma, in CTPC.Safety]
flatProg_sound [lemma, in CTPC.Flatify]
flatProg_sound' [lemma, in CTPC.Flatify]
flatVar [definition, in CTPC.Flatify]
flatVar_bound [lemma, in CTPC.Flatify]
flatVar_bounded [lemma, in CTPC.Safety]
flatVar_sel [lemma, in CTPC.Flatify]
flinear [inductive, in CTPC.Flat]
flinearDenote [definition, in CTPC.Flat]
flinear_bounded [definition, in CTPC.Safety]
flinear_safe [lemma, in CTPC.Safety]
flinear_safe_alt [lemma, in CTPC.Asmify]
fmakeTrace [definition, in CTPC.Flat]
fmakeTrace_unfold_external [lemma, in CTPC.Flat]
fmakeTrace_unfold_internal [lemma, in CTPC.Flat]
followPath [definition, in CTPC.Safety]
followPath_monotone [lemma, in CTPC.Safety]
followPath_refl [lemma, in CTPC.Asmify]
followPath_trans [lemma, in CTPC.Asmify]
fprecondition [definition, in CTPC.Flat]
fprimop [inductive, in CTPC.Flat]
fprimopDenote [definition, in CTPC.Flat]
fprimop_bounded [definition, in CTPC.Safety]
fprimop_safe [lemma, in CTPC.Safety]
fprog [inductive, in CTPC.Flat]
fprogDenote [definition, in CTPC.Flat]
fprog_safe [lemma, in CTPC.Safety]
freeVars [definition, in LambdaTamer.AutoSyntax]
freeVars [definition, in LambdaTamer.AutoSyntax]
freeVars [definition, in LambdaTamer.AutoSyntax]
frob_args [definition, in CTPC.Flatify]
frob_args_bounded [lemma, in CTPC.Safety]
frob_args_early [lemma, in CTPC.Flatify]
frob_args_sound [lemma, in CTPC.Flatify]
fromConsF [lemma, in LambdaTamer.ListT]
fromConsF' [lemma, in LambdaTamer.ListT]
fromNilF [lemma, in LambdaTamer.ListT]
fromNilF' [lemma, in LambdaTamer.ListT]
front [definition, in LambdaTamer.Binding]
frontVar [definition, in LambdaTamer.Binding]
frontVar' [definition, in LambdaTamer.Binding]
front' [definition, in LambdaTamer.Binding]
front'_sound [lemma, in LambdaTamer.Binding]
front_sound [lemma, in LambdaTamer.Binding]
FSlot [constructor, in CTPC.Flat]
ftrace_safe [lemma, in CTPC.Safety]
ftrace_safe' [lemma, in CTPC.Safety]
ftrace_safe_alt [lemma, in CTPC.Asmify]
ftyping [definition, in CTPC.Flat]
Fun [constructor, in LambdaTamer.AutoSyntax]
funcs_lr [definition, in CTPC.Allocify]
func_lr [definition, in CTPC.Allocify]
G
genop [inductive, in CTPC.Asm]
genopDenote [definition, in CTPC.Asm]
getElemT_listF_prover [lemma, in LambdaTamer.ListT]
getElemT_listF_prover' [lemma, in LambdaTamer.ListT]
getLarge [definition, in CTPC.Allocify]
getTerm [definition, in LambdaTamer.AutoSyntax]
getVar [definition, in LambdaTamer.AutoSyntax]
get_AllF [definition, in LambdaTamer.ListT]
get_AllF' [lemma, in LambdaTamer.ListT]
get_AllF'_AllF_prover [lemma, in LambdaTamer.ListT]
get_AllF_listF_prover' [lemma, in LambdaTamer.ListT]
get_AllF_listF_prover'' [lemma, in LambdaTamer.ListT]
get_AllF_prover [lemma, in LambdaTamer.ListT]
get_AllF_prover' [lemma, in LambdaTamer.ListT]
get_elemT [definition, in LambdaTamer.ListT]
get_elemT_listF_prover'' [lemma, in LambdaTamer.ListT]
get_elemT_map [lemma, in LambdaTamer.ListT]
get_mapF [lemma, in LambdaTamer.ListT]
get_traceShape [definition, in CTPC.Trace]
grabCproj [definition, in CTPC.CCify]
grabCproj' [definition, in CTPC.CCify]
grabCproj'' [definition, in CTPC.CCify]
grabCproj''_sound [lemma, in CTPC.CCify]
grabCproj'_sound [lemma, in CTPC.CCify]
grabCproj_sound [lemma, in CTPC.CCify]
grabVar [definition, in LambdaTamer.Binding]
grabVar_sound [lemma, in LambdaTamer.Binding]
H
head [definition, in LambdaTamer.Binding]
headF [definition, in LambdaTamer.ListT]
headF' [definition, in LambdaTamer.ListT]
headI [definition, in LambdaTamer.ListUtil]
headS [definition, in LambdaTamer.ListT]
headS' [definition, in LambdaTamer.ListT]
head_AllF [lemma, in LambdaTamer.ListT]
head_AllF' [lemma, in LambdaTamer.ListT]
I
ifVar [definition, in CTPC.Contify]
ifVar_sound [lemma, in CTPC.Contify]
initRoots [definition, in CTPC.Asmify]
initRoots_In [lemma, in CTPC.Asmify]
initRoots_incl [lemma, in CTPC.Asmify]
initRoots_In' [lemma, in CTPC.Asmify]
initRoots_NotIn [lemma, in CTPC.Asmify]
initRoots_NotIn' [lemma, in CTPC.Asmify]
init_bound [definition, in CTPC.Safety]
init_bound_incl [lemma, in CTPC.Safety]
insert [definition, in examples.CPS]
insert [definition, in CTPC.Allocify]
insert [definition, in CTPC.CPSify]
insert2 [definition, in examples.CPS]
insert2_sound [definition, in examples.CPS]
insert_sound [definition, in examples.CPS]
insert_sound [lemma, in CTPC.Allocify]
insert_sound [lemma, in CTPC.CPSify]
instrs [inductive, in CTPC.Asm]
instrsDenote [definition, in CTPC.Asm]
InT [definition, in LambdaTamer.ListT]
internal_nthI [lemma, in CTPC.Allocify]
inversion_Subst_cons [lemma, in LambdaTamer.Binding]
inversion_Subst_nil [lemma, in LambdaTamer.Binding]
invert_cfuncs_cons [lemma, in CTPC.CCify]
invert_cfuncs_cons' [lemma, in CTPC.CCify]
invert_cfuncs_nil [lemma, in CTPC.CCify]
invert_cfuncs_nil' [lemma, in CTPC.CCify]
invert_listF_cons [lemma, in LambdaTamer.ListT]
invert_listF_nil [lemma, in LambdaTamer.ListT]
In_init_bound [lemma, in CTPC.Asmify]
In_init_bound [lemma, in CTPC.Safety]
isLarges [definition, in CTPC.Allocify]
isLarges' [definition, in CTPC.Allocify]
isomorphic_args [definition, in CTPC.Safety]
isomorphic_new [lemma, in CTPC.Safety]
isomorphic_pointers [definition, in CTPC.Safety]
isomorphic_pointers_monotone [lemma, in CTPC.Safety]
isomorphic_pointers_refl [lemma, in CTPC.Asmify]
isomorphic_pointers_trans [lemma, in CTPC.Asmify]
isomorphic_slots [definition, in CTPC.Safety]
isomorphic_slots_call [lemma, in CTPC.Asmify]
isomorphic_slots_mono [lemma, in CTPC.Safety]
isomorphic_slots_monotone [lemma, in CTPC.Safety]
isomorphic_slots_refl [lemma, in CTPC.Asmify]
isomorphic_slots_set [lemma, in CTPC.Asmify]
isomorphic_slots_trans [lemma, in CTPC.Asmify]
isomorphic_values [definition, in CTPC.Safety]
isomorphic_values_lr [lemma, in CTPC.Asmify]
isomorphic_values_monotone [lemma, in CTPC.Safety]
isomorphic_values_trans [lemma, in CTPC.Asmify]
isSmall [definition, in CTPC.CC]
isSmalls [definition, in CTPC.CC]
isSmalls' [definition, in CTPC.CC]
isSmalls_nil [lemma, in CTPC.Allocify]
isSmalls_obvious [lemma, in CTPC.Allocify]
isSmall' [definition, in CTPC.CC]
isSmall'_obvious [lemma, in CTPC.Allocify]
isSmall_obvious [lemma, in CTPC.Allocify]
J
Jump [constructor, in CTPC.Asm]
K
keys [definition, in CTPC.Dict]
keys [axiom, in CTPC.Dict]
keys_empty [axiom, in CTPC.Dict]
keys_empty [lemma, in CTPC.Dict]
keys_init [lemma, in CTPC.Asmify]
keys_ok [axiom, in CTPC.Dict]
keys_ok [lemma, in CTPC.Dict]
keys_ok' [lemma, in CTPC.Dict]
keys_upd [lemma, in CTPC.Dict]
keys_upd [axiom, in CTPC.Dict]
L
LambdaTamer [library]
lastVar [definition, in LambdaTamer.Binding]
lastVar' [definition, in LambdaTamer.Binding]
lastVar'_sound [lemma, in LambdaTamer.Binding]
lastVar_sound [lemma, in LambdaTamer.Binding]
lengthF [definition, in LambdaTamer.ListT]
lengthT [definition, in LambdaTamer.ListT]
length_allocTys [lemma, in CTPC.Allocify]
length_app_cons [lemma, in LambdaTamer.ListUtil]
length_args [lemma, in CTPC.Allocify]
length_revApp_nil [lemma, in CTPC.Asmify]
lift [definition, in LambdaTamer.AutoSyntax]
lift [definition, in LambdaTamer.AutoSyntax]
lift [definition, in LambdaTamer.AutoSyntax]
liftEnd [definition, in LambdaTamer.Binding]
liftEnd' [definition, in LambdaTamer.Binding]
liftEnd'_sound [lemma, in LambdaTamer.Binding]
liftEnd_sound [lemma, in LambdaTamer.Binding]
liftMiddle [definition, in LambdaTamer.Binding]
liftMiddle_cons_sound [lemma, in LambdaTamer.Binding]
liftMiddle_sound [lemma, in LambdaTamer.Binding]
liftSubst' [definition, in LambdaTamer.Binding]
liftSubst'_sound [lemma, in LambdaTamer.Binding]
liftVar [definition, in LambdaTamer.Binding]
liftVarEnd [definition, in LambdaTamer.Binding]
liftVar' [definition, in LambdaTamer.Binding]
lift' [definition, in LambdaTamer.AutoSyntax]
lift' [definition, in LambdaTamer.AutoSyntax]
lift' [definition, in LambdaTamer.AutoSyntax]
lift'' [definition, in LambdaTamer.AutoSyntax]
lift'' [definition, in LambdaTamer.AutoSyntax]
lift'' [definition, in LambdaTamer.AutoSyntax]
lift''_sound [definition, in LambdaTamer.AutoSyntax]
lift''_sound [lemma, in LambdaTamer.AutoSyntax]
lift''_sound [axiom, in LambdaTamer.AutoSyntax]
lift''_sound [axiom, in LambdaTamer.AutoSyntax]
lift'_sound [definition, in LambdaTamer.AutoSyntax]
lift'_sound [lemma, in LambdaTamer.AutoSyntax]
lift'_sound [axiom, in LambdaTamer.AutoSyntax]
lift'_sound [axiom, in LambdaTamer.AutoSyntax]
lift_sound [axiom, in LambdaTamer.AutoSyntax]
lift_sound [lemma, in LambdaTamer.AutoSyntax]
lift_sound [definition, in LambdaTamer.AutoSyntax]
lift_sound [axiom, in LambdaTamer.AutoSyntax]
linear_lr [definition, in CTPC.Flatify]
linear_lr [definition, in CTPC.CCify]
linear_lr [definition, in CTPC.Contify]
listF [inductive, in LambdaTamer.ListT]
listF_AllF [lemma, in LambdaTamer.ListT]
listF_prover [lemma, in LambdaTamer.ListT]
listF_prover' [lemma, in LambdaTamer.ListT]
listF_prover'' [lemma, in LambdaTamer.ListT]
listI [definition, in LambdaTamer.ListUtil]
listS [definition, in LambdaTamer.ListT]
listT [inductive, in LambdaTamer.ListT]
ListT [library]
ListUtil [library]
M
Make [module, in LambdaTamer.AutoSyntax]
makeActuals [definition, in CTPC.Alloc]
makeTm [definition, in LambdaTamer.AutoSyntax]
makeTrace [definition, in CTPC.Asm]
mapCompose [lemma, in LambdaTamer.ListT]
mapElemT [definition, in LambdaTamer.ListT]
mapF [definition, in LambdaTamer.ListT]
mapF' [definition, in LambdaTamer.ListT]
mapF'_compose [lemma, in LambdaTamer.ListT]
mapF'_In [lemma, in LambdaTamer.ListT]
mapI [definition, in LambdaTamer.ListUtil]
mapIdempotent [lemma, in LambdaTamer.ListT]
mapI_list [definition, in CTPC.Asmify]
mapT [definition, in LambdaTamer.ListT]
mapT_appT [lemma, in LambdaTamer.AutoSyntax]
mapT_InT [lemma, in LambdaTamer.ListT]
map_AllF [lemma, in LambdaTamer.ListT]
map_AllF_prover [lemma, in LambdaTamer.ListT]
map_app [lemma, in LambdaTamer.ListUtil]
map_id [lemma, in LambdaTamer.ListUtil]
map_length [lemma, in CTPC.Asmify]
meaning [inductive, in LambdaTamer.AutoSyntax]
meaningDenote [definition, in LambdaTamer.AutoSyntax]
meaningDenote_change [lemma, in LambdaTamer.AutoSyntax]
mem [definition, in CTPC.AllocMonad]
mem0 [definition, in CTPC.Compile]
mem_nil_end [lemma, in CTPC.Allocify]
multiSwap [definition, in LambdaTamer.Binding]
multiSwap_sound [lemma, in LambdaTamer.Binding]
N
NatDict [module, in CTPC.Flat]
NatKey [module, in CTPC.Flat]
negb_prop [lemma, in CTPC.Allocify]
negb_true_intro [lemma, in CTPC.Allocify]
New [constructor, in CTPC.Asm]
Next [constructor, in LambdaTamer.Binding]
nextT [constructor, in LambdaTamer.ListT]
nilF [constructor, in LambdaTamer.ListT]
nilI [definition, in LambdaTamer.ListUtil]
nilS [definition, in LambdaTamer.ListT]
nilT [constructor, in LambdaTamer.ListT]
NoneT [constructor, in LambdaTamer.ListT]
NotIn_init_bound [lemma, in CTPC.Asmify]
nthFuncs [definition, in CTPC.Allocify]
nthFuncs_contra [lemma, in CTPC.Allocify]
nthFuncs_larges [lemma, in CTPC.Allocify]
nthI [definition, in LambdaTamer.ListUtil]
nthI_mapI [lemma, in LambdaTamer.ListUtil]
nthI_mapI' [lemma, in CTPC.Safety]
nthT [definition, in LambdaTamer.ListT]
nth_error_bound [lemma, in LambdaTamer.ListUtil]
nth_error_grab [lemma, in LambdaTamer.ListUtil]
nth_error_grab' [lemma, in LambdaTamer.ListUtil]
nth_error_grab_last [lemma, in LambdaTamer.ListUtil]
nth_error_monotone [lemma, in LambdaTamer.ListUtil]
nth_error_total [lemma, in CTPC.Safety]
nth_mapI_list [lemma, in CTPC.Asmify]
O
OACons [constructor, in CTPC.Cont]
OANil [constructor, in CTPC.Cont]
OApply [constructor, in CTPC.Cont]
oargs [inductive, in CTPC.Cont]
oargsDenote [definition, in CTPC.Cont]
OBind [constructor, in CTPC.Cont]
OCCons [constructor, in CTPC.Cont]
OCNil [constructor, in CTPC.Cont]
OConst [constructor, in CTPC.Cont]
OCont [constructor, in CTPC.Cont]
ocont [inductive, in CTPC.Cont]
ocontDenote [definition, in CTPC.Cont]
ocontTy [definition, in CTPC.Cont]
OLam [constructor, in CTPC.Cont]
olinear [inductive, in CTPC.Cont]
olinearDenote [definition, in CTPC.Cont]
ONat [constructor, in CTPC.Cont]
oprimop [inductive, in CTPC.Cont]
oprimopDenote [definition, in CTPC.Cont]
oprimop_lift_sound [lemma, in CTPC.Contify]
optionT [inductive, in LambdaTamer.ListT]
option_inj [lemma, in LambdaTamer.ListT]
oresultDenote [definition, in CTPC.Cont]
oty [inductive, in CTPC.Cont]
otyDenote [definition, in CTPC.Cont]
otys [definition, in CTPC.Cont]
otysDenote [definition, in CTPC.Cont]
Output [constructor, in CTPC.Trace]
OutputShape [constructor, in CTPC.Trace]
OVar [constructor, in CTPC.Cont]
P
PApply [constructor, in CTPC.CPS]
PARAM [module, in LambdaTamer.AutoSyntax]
PBind [constructor, in CTPC.CPS]
PConst [constructor, in CTPC.CPS]
permute [definition, in LambdaTamer.AutoSyntax]
permute [definition, in LambdaTamer.AutoSyntax]
permute [definition, in LambdaTamer.AutoSyntax]
permuteVar [definition, in LambdaTamer.Binding]
permuteVar_sound [lemma, in LambdaTamer.Binding]
permute' [definition, in LambdaTamer.AutoSyntax]
permute'_sound [lemma, in LambdaTamer.AutoSyntax]
permute_sound [axiom, in LambdaTamer.AutoSyntax]
permute_sound [axiom, in LambdaTamer.AutoSyntax]
permute_sound [definition, in LambdaTamer.AutoSyntax]
permute_sound [lemma, in LambdaTamer.AutoSyntax]
pexpDenote [definition, in CTPC.CPS]
PLam [constructor, in CTPC.CPS]
plinear [inductive, in CTPC.CPS]
plinearDenote [definition, in CTPC.CPS]
pprimop [inductive, in CTPC.CPS]
pprimopDenote [definition, in CTPC.CPS]
precondition_safe [lemma, in CTPC.Safety]
primop_lr [definition, in CTPC.CCify]
primop_lr [definition, in CTPC.Allocify]
primop_lr [definition, in CTPC.Contify]
primop_lr [definition, in CTPC.Flatify]
program [inductive, in CTPC.Asm]
programDenote [definition, in CTPC.Asm]
prog_lr [definition, in CTPC.Flatify]
prog_lr [definition, in CTPC.Allocify]
Proj [constructor, in CTPC.Asm]
prover_AllF [lemma, in LambdaTamer.ListT]
PThrow [constructor, in CTPC.CPS]
ptyDenote [definition, in CTPC.CPS]
PVar [constructor, in CTPC.CPS]
R
read_ctys [definition, in CTPC.CCify]
read_ctys' [definition, in CTPC.CCify]
read_ctys'' [definition, in CTPC.CCify]
remover [definition, in CTPC.Asmify]
remover_eq [lemma, in CTPC.Asmify]
remover_mono [lemma, in CTPC.Asmify]
remover_neq1 [lemma, in CTPC.Asmify]
remover_neq2 [lemma, in CTPC.Asmify]
remover_neq2_cp [lemma, in CTPC.Asmify]
result [definition, in CTPC.Continuation]
RESULT [module, in LambdaTamer.AutoSyntax]
result [definition, in CTPC.Cont]
Return [constructor, in LambdaTamer.Computation]
retype_elemT [definition, in LambdaTamer.ListT]
retype_elemT_ident [lemma, in LambdaTamer.ListT]
retype_listF [definition, in LambdaTamer.ListT]
retype_listF_ident [lemma, in LambdaTamer.ListT]
retype_Subst [definition, in LambdaTamer.AutoSyntax]
retype_Subst_cons [lemma, in LambdaTamer.AutoSyntax]
retype_Subst_ident [lemma, in LambdaTamer.AutoSyntax]
retype_term [definition, in LambdaTamer.AutoSyntax]
retype_term_ident [lemma, in LambdaTamer.AutoSyntax]
retype_Var [definition, in LambdaTamer.Binding]
retype_Var_ident [lemma, in LambdaTamer.Binding]
revApp [definition, in LambdaTamer.ListUtil]
revAppN [definition, in LambdaTamer.ListUtil]
revAppN_app [lemma, in LambdaTamer.ListUtil]
revAppN_length [lemma, in LambdaTamer.ListUtil]
revAppN_split [lemma, in LambdaTamer.ListUtil]
revAppN_Subst [definition, in LambdaTamer.Binding]
revAppN_Subst_app [lemma, in LambdaTamer.Binding]
revApp_app [lemma, in LambdaTamer.ListUtil]
revApp_ass [lemma, in CTPC.CCify]
revApp_inj [lemma, in CTPC.Safety]
revApp_nil [lemma, in LambdaTamer.ListUtil]
rev_length [lemma, in LambdaTamer.ListUtil]
rootsIn [definition, in CTPC.Asm]
rootsIn_In [lemma, in CTPC.Asmify]
rootsIn_notIn [lemma, in CTPC.Asmify]
roots_backup [lemma, in CTPC.Asmify]
roots_grabber [definition, in CTPC.Asmify]
rty [definition, in LambdaTamer.AutoSyntax]
rty [definition, in LambdaTamer.AutoSyntax]
rtyDenote [axiom, in LambdaTamer.AutoSyntax]
rtyDenote [definition, in LambdaTamer.AutoSyntax]
rtyDenote [definition, in LambdaTamer.AutoSyntax]
rtyDenote [axiom, in LambdaTamer.AutoSyntax]
rtyDenote [definition, in LambdaTamer.AutoSyntax]
rtyDenote [axiom, in LambdaTamer.AutoSyntax]
rtyDenote [axiom, in LambdaTamer.AutoSyntax]
run [inductive, in LambdaTamer.Computation]
Run [constructor, in LambdaTamer.Computation]
RunCall [constructor, in CTPC.Trace]
RunCall' [constructor, in CTPC.Trace]
RunOutput [constructor, in CTPC.Trace]
RunOutput' [constructor, in CTPC.Trace]
runsTo [inductive, in CTPC.Trace]
runsTo' [inductive, in CTPC.Trace]
runsTo_Call [lemma, in CTPC.Trace]
runsTo_runTrace_trans [lemma, in CTPC.Trace]
runsTo_Self [lemma, in CTPC.Trace]
runsTo_shape [lemma, in CTPC.Trace]
runsTo_trans [lemma, in CTPC.Trace]
runtime [inductive, in CTPC.Asm]
RunTo_Call [constructor, in CTPC.Trace]
RunTo_Call' [constructor, in CTPC.Trace]
RunTo_Self [constructor, in CTPC.Trace]
RunTo_Self' [constructor, in CTPC.Trace]
runTrace [inductive, in CTPC.Trace]
runTrace' [inductive, in CTPC.Trace]
runTrace_shape [lemma, in CTPC.Trace]
runTrace_shape_inv [lemma, in CTPC.Trace]
S
Safety [library]
SApp [constructor, in examples.CPS]
SApp [constructor, in CTPC.Source]
SArrow [constructor, in CTPC.Source]
SArrow [constructor, in examples.CPS]
SBool [constructor, in examples.CPS]
SCons [constructor, in LambdaTamer.Binding]
SConst [constructor, in examples.CPS]
SConst [constructor, in CTPC.Source]
sel [axiom, in CTPC.Dict]
sel [definition, in CTPC.Dict]
self_revAppN [lemma, in LambdaTamer.ListUtil]
sel' [definition, in CTPC.Dict]
sel_empty [axiom, in CTPC.Dict]
sel_empty [lemma, in CTPC.Dict]
sel_upd_eq [axiom, in CTPC.Dict]
sel_upd_eq [lemma, in CTPC.Dict]
sel_upd_ne [lemma, in CTPC.Dict]
sel_upd_ne [axiom, in CTPC.Dict]
set [definition, in LambdaTamer.ListT]
SFst [constructor, in examples.CPS]
SLam [constructor, in examples.CPS]
SLam [constructor, in CTPC.Source]
Slot [constructor, in CTPC.Asm]
slots [definition, in CTPC.Flat]
slots_actuals [definition, in CTPC.Flatify]
slots_args [definition, in CTPC.Flatify]
slots_args' [definition, in CTPC.Flatify]
slots_args_app [lemma, in CTPC.Flatify]
slots_args_app1 [lemma, in CTPC.Flatify]
slots_lr [definition, in CTPC.Asmify]
slots_lr_call [lemma, in CTPC.Asmify]
slots_lr_valid [lemma, in CTPC.Asmify]
slots_Subst [definition, in CTPC.Flatify]
slots_Subst' [definition, in CTPC.Flatify]
slots_Subst_func [lemma, in CTPC.Flatify]
slots_Subst_sound [lemma, in CTPC.Flatify]
slots_Subst_upd [lemma, in CTPC.Flatify]
SlrU_Cons [constructor, in LambdaTamer.Binding]
SlrU_Nil [constructor, in LambdaTamer.Binding]
Slr_Cons [constructor, in LambdaTamer.Binding]
Slr_Nil [constructor, in LambdaTamer.Binding]
smallCty [definition, in CTPC.CC]
smallCtys [definition, in CTPC.CC]
SNat [constructor, in CTPC.Source]
SNil [constructor, in LambdaTamer.Binding]
SomeT [constructor, in LambdaTamer.ListT]
Source [library]
SPair [constructor, in examples.CPS]
splice [definition, in CTPC.Allocify]
splice_sound [lemma, in CTPC.Allocify]
splitCtysSubst [lemma, in CTPC.CCify]
SProd [constructor, in examples.CPS]
SSnd [constructor, in examples.CPS]
stash [definition, in CTPC.Flatify]
stashSlots [definition, in CTPC.Flatify]
stashSlots_early [lemma, in CTPC.Flatify]
stashSlots_late [lemma, in CTPC.Flatify]
stashSlots_sound [lemma, in CTPC.Flatify]
stashType [definition, in CTPC.Flatify]
stashType_early [lemma, in CTPC.Flatify]
stashType_early' [lemma, in CTPC.Flatify]
stashType_late [lemma, in CTPC.Flatify]
stashType_sound [lemma, in CTPC.Flatify]
stash_bound [definition, in CTPC.Safety]
stash_bounded [lemma, in CTPC.Safety]
stash_bound_has [lemma, in CTPC.Safety]
stash_bound_mono [lemma, in CTPC.Safety]
stash_soundness [lemma, in CTPC.Flatify]
sterm [inductive, in CTPC.Source]
sterm [inductive, in examples.CPS]
stermDenote [definition, in CTPC.Source]
stermDenote [definition, in examples.CPS]
store [definition, in CTPC.Asm]
strengthen [definition, in LambdaTamer.AutoSyntax]
strengthen [definition, in LambdaTamer.AutoSyntax]
strengthen [definition, in LambdaTamer.AutoSyntax]
strengthen' [definition, in LambdaTamer.AutoSyntax]
strengthen'_sound [lemma, in LambdaTamer.AutoSyntax]
strengthen_app [definition, in LambdaTamer.AutoSyntax]
strengthen_app [definition, in LambdaTamer.AutoSyntax]
strengthen_app [definition, in LambdaTamer.AutoSyntax]
strengthen_app_sound [lemma, in LambdaTamer.AutoSyntax]
strengthen_app_sound [axiom, in LambdaTamer.AutoSyntax]
strengthen_app_sound [lemma, in CTPC.CCify]
strengthen_app_sound [definition, in LambdaTamer.AutoSyntax]
strengthen_app_sound [axiom, in LambdaTamer.AutoSyntax]
strengthen_First [lemma, in LambdaTamer.Binding]
strengthen_Next_false [lemma, in LambdaTamer.Binding]
strengthen_Next_true [lemma, in LambdaTamer.Binding]
strengthen_SCons_false [lemma, in LambdaTamer.Binding]
strengthen_SCons_true [lemma, in LambdaTamer.Binding]
strengthen_sound [axiom, in LambdaTamer.AutoSyntax]
strengthen_sound [definition, in LambdaTamer.AutoSyntax]
strengthen_sound [axiom, in LambdaTamer.AutoSyntax]
strengthen_sound [lemma, in LambdaTamer.AutoSyntax]
sty [inductive, in examples.CPS]
sty [inductive, in CTPC.Source]
styDenote [definition, in CTPC.Source]
styDenote [definition, in examples.CPS]
Subst [inductive, in LambdaTamer.Binding]
SubstU_lr [inductive, in LambdaTamer.Binding]
SubstU_lr_Var [lemma, in LambdaTamer.Binding]
substVar [definition, in LambdaTamer.Binding]
substVar' [definition, in LambdaTamer.Binding]
subst_comm [lemma, in LambdaTamer.AutoSyntax]
Subst_decomp [lemma, in LambdaTamer.Binding]
Subst_drop [definition, in LambdaTamer.Binding]
Subst_invert_cons [lemma, in LambdaTamer.Binding]
Subst_invert_cons' [lemma, in LambdaTamer.Binding]
Subst_invert_nil [lemma, in LambdaTamer.Binding]
Subst_invert_nil' [lemma, in LambdaTamer.Binding]
Subst_lr [definition, in CTPC.Contify]
Subst_lr [definition, in CTPC.CPSify]
Subst_lr [definition, in CTPC.Allocify]
Subst_lr [definition, in CTPC.CCify]
Subst_lr [inductive, in LambdaTamer.Binding]
Subst_lr [definition, in examples.CPS]
Subst_lr_fold [lemma, in CTPC.Allocify]
Subst_lr_monotone [lemma, in CTPC.Allocify]
Subst_lr_Var [lemma, in LambdaTamer.Binding]
Subst_lr_Var [lemma, in CTPC.CPSify]
Subst_revAppN_split [lemma, in LambdaTamer.Binding]
Subst_revAppN_split' [lemma, in LambdaTamer.Binding]
Subst_strengthen [definition, in LambdaTamer.Binding]
Subst_strengthen_all [lemma, in LambdaTamer.Binding]
Subterm [constructor, in LambdaTamer.AutoSyntax]
Subvar [constructor, in LambdaTamer.AutoSyntax]
SVar [constructor, in examples.CPS]
SVar [constructor, in CTPC.Source]
swap [definition, in CTPC.Contify]
swap_sound [lemma, in CTPC.Contify]
T
Tactics [library]
tag [inductive, in CTPC.Alloc]
tagof [definition, in CTPC.Alloc]
tag_eq_dec [definition, in CTPC.Alloc]
tail [definition, in LambdaTamer.Binding]
tailF [definition, in LambdaTamer.ListT]
tailF' [definition, in LambdaTamer.ListT]
tailI [definition, in LambdaTamer.ListUtil]
tailS [definition, in LambdaTamer.ListT]
tailS' [definition, in LambdaTamer.ListT]
tail''_tail [lemma, in CTPC.CCify]
tail'_split [lemma, in CTPC.CCify]
tail'_tail [lemma, in CTPC.CCify]
tail'_tail_pf [lemma, in CTPC.CCify]
tail_AllF [lemma, in LambdaTamer.ListT]
tail_AllF' [lemma, in LambdaTamer.ListT]
tail_split [lemma, in CTPC.CCify]
tail_split_pf [lemma, in CTPC.CCify]
term [definition, in LambdaTamer.AutoSyntax]
term [axiom, in LambdaTamer.AutoSyntax]
term [definition, in LambdaTamer.AutoSyntax]
term [axiom, in LambdaTamer.AutoSyntax]
termDenote [axiom, in LambdaTamer.AutoSyntax]
termDenote [definition, in LambdaTamer.AutoSyntax]
termDenote [axiom, in LambdaTamer.AutoSyntax]
termDenote [axiom, in LambdaTamer.AutoSyntax]
termDenote [definition, in LambdaTamer.AutoSyntax]
termDenote [axiom, in LambdaTamer.AutoSyntax]
termDenote [definition, in LambdaTamer.AutoSyntax]
termDenote_ass [lemma, in LambdaTamer.Binding]
termDenote_cons_ass [lemma, in LambdaTamer.Binding]
termNil [definition, in LambdaTamer.Binding]
term_incl [lemma, in LambdaTamer.AutoSyntax]
term_lr [definition, in examples.CPS]
term_rect [definition, in LambdaTamer.AutoSyntax]
term_rect [definition, in LambdaTamer.AutoSyntax]
term_rect [axiom, in LambdaTamer.AutoSyntax]
term_rect [axiom, in LambdaTamer.AutoSyntax]
term_rect_cons [axiom, in LambdaTamer.AutoSyntax]
term_rect_cons [axiom, in LambdaTamer.AutoSyntax]
term_rect_cons [definition, in LambdaTamer.AutoSyntax]
trace [inductive, in CTPC.Trace]
Trace [library]
Traced [constructor, in CTPC.Alloc]
traceShape [inductive, in CTPC.Trace]
traceShape_eq [lemma, in CTPC.Trace]
trace_eq [lemma, in CTPC.Trace]
trace_precondition [lemma, in CTPC.Asmify]
U
unfold_computation [lemma, in LambdaTamer.Computation]
unT [definition, in LambdaTamer.AutoSyntax]
Untraced [constructor, in CTPC.Alloc]
unT_appT [lemma, in LambdaTamer.AutoSyntax]
unT_cons [definition, in LambdaTamer.AutoSyntax]
unT_enT [lemma, in LambdaTamer.AutoSyntax]
unT_enT_app [lemma, in LambdaTamer.AutoSyntax]
unvalify [definition, in LambdaTamer.AutoSyntax]
upd [axiom, in CTPC.Dict]
upd [definition, in CTPC.Dict]
updateRoots [definition, in CTPC.Asmify]
upd_early [lemma, in CTPC.Flatify]
upd_inj [axiom, in CTPC.Dict]
upd_inj [lemma, in CTPC.Dict]
V
valComp [definition, in CTPC.Asm]
validPath [definition, in CTPC.Safety]
validPath_monotone [lemma, in CTPC.Safety]
vals_lr [definition, in CTPC.CCify]
vals_lr [definition, in CTPC.Allocify]
vals_lr_monotone [lemma, in CTPC.Allocify]
val_lr [definition, in CTPC.Contify]
val_lr [definition, in CTPC.Flatify]
val_lr [definition, in CTPC.CPSify]
val_lr [definition, in examples.CPS]
val_lr [definition, in CTPC.Asmify]
val_lr [definition, in CTPC.CCify]
val_lr [definition, in CTPC.Allocify]
val_lr_monotone [lemma, in CTPC.Allocify]
Var [inductive, in LambdaTamer.Binding]
VarConvert [definition, in LambdaTamer.Binding]
VarDenote [definition, in LambdaTamer.Binding]
varInfo [definition, in LambdaTamer.Binding]
varInfo_all [definition, in LambdaTamer.Binding]
varInfo_all_incl [lemma, in LambdaTamer.Binding]
varInfo_app [definition, in LambdaTamer.Binding]
varInfo_apply [definition, in LambdaTamer.Binding]
varInfo_apply_all [lemma, in LambdaTamer.Binding]
varInfo_apply_drop [lemma, in LambdaTamer.Binding]
varInfo_apply_pad [lemma, in LambdaTamer.Binding]
varInfo_apply_take [lemma, in LambdaTamer.Binding]
varInfo_apply_take_drop [lemma, in LambdaTamer.Binding]
varInfo_double_join_incl [lemma, in LambdaTamer.Binding]
varInfo_drop [definition, in LambdaTamer.Binding]
varInfo_drop_app [lemma, in LambdaTamer.Binding]
varInfo_fold_incl_acc [lemma, in LambdaTamer.Binding]
varInfo_fold_incl_acc' [lemma, in LambdaTamer.Binding]
varInfo_fold_incl_acc'' [lemma, in LambdaTamer.Binding]
varInfo_fold_incl_ls [lemma, in LambdaTamer.Binding]
varInfo_incl [definition, in LambdaTamer.Binding]
varInfo_incl_drop [lemma, in LambdaTamer.Binding]
varInfo_incl_refl [lemma, in LambdaTamer.Binding]
varInfo_incl_split [lemma, in LambdaTamer.Binding]
varInfo_incl_take [lemma, in LambdaTamer.Binding]
varInfo_incl_take_drop [lemma, in LambdaTamer.Binding]
varInfo_incl_trans [lemma, in LambdaTamer.Binding]
varInfo_join [definition, in LambdaTamer.Binding]
varInfo_join_incl [lemma, in LambdaTamer.Binding]
varInfo_join_incl1 [lemma, in LambdaTamer.Binding]
varInfo_join_incl2 [lemma, in LambdaTamer.Binding]
varInfo_keep [definition, in LambdaTamer.Binding]
varInfo_keep_incl [lemma, in LambdaTamer.Binding]
varInfo_none [definition, in LambdaTamer.Binding]
varInfo_pad [definition, in LambdaTamer.Binding]
varInfo_take [definition, in LambdaTamer.Binding]
varInfo_take_app [lemma, in LambdaTamer.Binding]
VarNil [definition, in LambdaTamer.Binding]
VarNil_sound [lemma, in LambdaTamer.Binding]
Var_app_split [lemma, in CTPC.Allocify]
Var_freeVars [definition, in LambdaTamer.Binding]
var_incl [lemma, in LambdaTamer.AutoSyntax]
Var_invert [lemma, in LambdaTamer.Binding]
Var_invert' [lemma, in LambdaTamer.Binding]
Var_revAppN_split [lemma, in CTPC.Allocify]
Var_split [lemma, in LambdaTamer.Binding]
Var_strengthen [definition, in LambdaTamer.Binding]
Var_strengthen_sound [lemma, in LambdaTamer.Binding]
W
withCont [definition, in CTPC.Continuation]
withCont_bind [definition, in examples.CPS]
withCont_bind [definition, in CTPC.Continuation]
withCont_compose [definition, in CTPC.Continuation]
withCont_const [definition, in CTPC.Continuation]
Axiom Index
A
A [in CTPC.Dict]
A [in CTPC.Dict]
A_eq_dec [in CTPC.Dict]
C
cons [in LambdaTamer.AutoSyntax]
cons [in LambdaTamer.AutoSyntax]
D
default [in CTPC.Dict]
dict [in CTPC.Dict]
dict_eq_dec [in CTPC.Dict]
dtyDenote [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
E
empty [in CTPC.Dict]
empty_inj [in CTPC.Dict]
equations [in LambdaTamer.AutoSyntax]
equations [in LambdaTamer.AutoSyntax]
ext_eq_Type [in LambdaTamer.Ext]
K
keys [in CTPC.Dict]
keys_empty [in CTPC.Dict]
keys_ok [in CTPC.Dict]
keys_upd [in CTPC.Dict]
L
lift''_sound [in LambdaTamer.AutoSyntax]
lift''_sound [in LambdaTamer.AutoSyntax]
lift'_sound [in LambdaTamer.AutoSyntax]
lift'_sound [in LambdaTamer.AutoSyntax]
lift_sound [in LambdaTamer.AutoSyntax]
lift_sound [in LambdaTamer.AutoSyntax]
P
permute_sound [in LambdaTamer.AutoSyntax]
permute_sound [in LambdaTamer.AutoSyntax]
R
rtyDenote [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
S
sel [in CTPC.Dict]
sel_empty [in CTPC.Dict]
sel_upd_eq [in CTPC.Dict]
sel_upd_ne [in CTPC.Dict]
strengthen_app_sound [in LambdaTamer.AutoSyntax]
strengthen_app_sound [in LambdaTamer.AutoSyntax]
strengthen_sound [in LambdaTamer.AutoSyntax]
strengthen_sound [in LambdaTamer.AutoSyntax]
T
term [in LambdaTamer.AutoSyntax]
term [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
term_rect [in LambdaTamer.AutoSyntax]
term_rect [in LambdaTamer.AutoSyntax]
term_rect_cons [in LambdaTamer.AutoSyntax]
term_rect_cons [in LambdaTamer.AutoSyntax]
U
upd [in CTPC.Dict]
upd_inj [in CTPC.Dict]
Lemma Index
A
aargsDenote_len [in CTPC.Flatify]
aBind_backward [in CTPC.AllocMonad]
aBind_forward [in CTPC.AllocMonad]
aFrame [in CTPC.AllocMonad]
afuncBody_sound [in CTPC.Flatify]
AllF_prover [in LambdaTamer.ListT]
allocArgs_sound [in CTPC.Allocify]
allocCode_body_var [in CTPC.Allocify]
allocCode_body_var' [in CTPC.Allocify]
allocCode_bound [in CTPC.Allocify]
allocCode_nth [in CTPC.Allocify]
allocCode_nth_revAppN [in CTPC.Allocify]
allocCode_nth_revAppN' [in CTPC.Allocify]
allocCode_nth_ts [in CTPC.Allocify]
allocCode_nth_ts' [in CTPC.Allocify]
allocCode_push [in CTPC.Allocify]
allocCode_push' [in CTPC.Allocify]
allocCode_zero [in CTPC.Allocify]
allocCode_zero' [in CTPC.Allocify]
allocFuncs_sound [in CTPC.Allocify]
allocFunc_sound [in CTPC.Allocify]
allocLinear_sound [in CTPC.Allocify]
allocPrimop_sound [in CTPC.Allocify]
allocProg_body_sound [in CTPC.Allocify]
allocProg_funcs_soundness [in CTPC.Allocify]
allocProg_funcs_var [in CTPC.Allocify]
allocProg_funcs_var' [in CTPC.Allocify]
allocProg_sound [in CTPC.Allocify]
allocProj_sound [in CTPC.Allocify]
allocVar'_sound [in CTPC.Allocify]
allocVar_sound [in CTPC.Allocify]
allocVar_sound_lr [in CTPC.Allocify]
AllS2_len [in CTPC.Asmify]
amakeTrace_unfold_external [in CTPC.Alloc]
amakeTrace_unfold_internal [in CTPC.Alloc]
aNew_forward [in CTPC.AllocMonad]
appBinders_comm [in LambdaTamer.AutoSyntax]
appSubstF_liftSubst' [in LambdaTamer.AutoSyntax]
appSubstF_strengthen [in LambdaTamer.AutoSyntax]
appSubst_appSubstF [in LambdaTamer.AutoSyntax]
appSubst_assoc [in LambdaTamer.Binding]
appSubst_assoc' [in LambdaTamer.Binding]
appSubst_decomp [in LambdaTamer.Binding]
appSubst_liftSubst' [in LambdaTamer.Binding]
appSubst_nil [in LambdaTamer.Binding]
appSubst_nil' [in LambdaTamer.Binding]
app_length [in LambdaTamer.ListUtil]
app_middle [in LambdaTamer.ListUtil]
app_nil_middle [in LambdaTamer.ListUtil]
aRead_forward [in CTPC.AllocMonad]
aReturn_forward [in CTPC.AllocMonad]
argsDenote_len [in CTPC.Asmify]
args_bound_early [in CTPC.Flatify]
args_early_monotone [in CTPC.Flatify]
args_lr_vals_lr [in CTPC.Allocify]
args_max_early [in CTPC.Flatify]
asmArgs_sound [in CTPC.Asmify]
asmLinear_sound [in CTPC.Asmify]
asmPrimop_sound [in CTPC.Asmify]
asmProg_sound [in CTPC.Asmify]
asmTrace_sound [in CTPC.Asmify]
asmTrace_sound' [in CTPC.Asmify]
B
bindCfunc_sound [in CTPC.CCify]
buildEnv'_sound [in CTPC.CCify]
buildEnv_apply [in CTPC.CCify]
C
call_precondition [in CTPC.Flatify]
cargsDenote_app_nil [in CTPC.CCify]
cast_app [in LambdaTamer.Binding]
cast_CFCons [in CTPC.CCify]
cast_cons [in LambdaTamer.Binding]
cast_SCons_head [in LambdaTamer.Binding]
cast_SCons_tail [in LambdaTamer.Binding]
ccLinear_sound [in CTPC.CCify]
ccTySmall [in CTPC.CCify]
ccTysSmall [in CTPC.CCify]
ccTysViSmall [in CTPC.CCify]
cc_lr [in CTPC.Compile]
cfuncs_larges [in CTPC.Allocify]
close''_sound [in CTPC.CCify]
close'_sound [in CTPC.CCify]
close_sound [in CTPC.CCify]
closureVar_sound [in CTPC.CCify]
compile_correct [in CTPC.Compile]
compile_slots_lr [in CTPC.Compile]
compose_sound [in CTPC.CPSify]
contifyLinear_sound [in CTPC.Contify]
cont_lr [in CTPC.Compile]
copySlots_late [in CTPC.Flatify]
copySlots_sound [in CTPC.Flatify]
copyType_late [in CTPC.Flatify]
copyType_sound [in CTPC.Flatify]
copy_bounded [in CTPC.Safety]
copy_bound_has [in CTPC.Safety]
copy_bound_mono [in CTPC.Safety]
copy_soundness [in CTPC.Flatify]
cpsTerm_sound [in examples.CPS]
cpsTerm_sound_bool [in examples.CPS]
cps_sound [in CTPC.CPSify]
E
early_bump [in CTPC.Flatify]
elemT_invert [in LambdaTamer.ListT]
elemT_invert' [in LambdaTamer.ListT]
elemT_split [in LambdaTamer.ListT]
embed'_sound [in LambdaTamer.Binding]
embed_sound [in LambdaTamer.Binding]
empty_inj [in CTPC.Dict]
eq_rect_ident [in LambdaTamer.ListT]
eq_rect_reverse [in LambdaTamer.ListT]
eq_rect_r_ident [in LambdaTamer.ListT]
eq_rec_r_ident [in LambdaTamer.ListT]
etaF_eq [in LambdaTamer.AutoSyntax]
etaT [in LambdaTamer.AutoSyntax]
extend_app [in LambdaTamer.AutoSyntax]
ext_eq [in LambdaTamer.Ext]
ext_eqT [in LambdaTamer.Ext]
ext_eq_dep [in LambdaTamer.Ext]
F
fargsDenote_len [in CTPC.Flatify]
fargs_bounded_mono [in CTPC.Safety]
fargs_bounded_mono' [in CTPC.Safety]
fargs_safe [in CTPC.Safety]
fields_backup [in CTPC.Asmify]
flatArgs_bounded [in CTPC.Safety]
flatArgs_sound [in CTPC.Flatify]
flatCall_lemma [in CTPC.Flatify]
flatCall_sel [in CTPC.Flatify]
flatContext_inj [in CTPC.Safety]
flatContext_late [in CTPC.Asmify]
flatContext_revApp_inj [in CTPC.Safety]
flatContext_sel [in CTPC.Safety]
flatContext_sel' [in CTPC.Safety]
flatContext_sel'' [in CTPC.Safety]
flatContext_sel_direct [in CTPC.Asmify]
flatFunc_bounded [in CTPC.Safety]
flatLinear_bounded [in CTPC.Safety]
flatLinear_sound [in CTPC.Flatify]
flatPrimop_bounded [in CTPC.Safety]
flatPrimop_sound [in CTPC.Flatify]
flatProg_body_bounded [in CTPC.Safety]
flatProg_funcs_bounded [in CTPC.Safety]
flatProg_sound [in CTPC.Flatify]
flatProg_sound' [in CTPC.Flatify]
flatVar_bound [in CTPC.Flatify]
flatVar_bounded [in CTPC.Safety]
flatVar_sel [in CTPC.Flatify]
flinear_safe [in CTPC.Safety]
flinear_safe_alt [in CTPC.Asmify]
fmakeTrace_unfold_external [in CTPC.Flat]
fmakeTrace_unfold_internal [in CTPC.Flat]
followPath_monotone [in CTPC.Safety]
followPath_refl [in CTPC.Asmify]
followPath_trans [in CTPC.Asmify]
fprimop_safe [in CTPC.Safety]
fprog_safe [in CTPC.Safety]
frob_args_bounded [in CTPC.Safety]
frob_args_early [in CTPC.Flatify]
frob_args_sound [in CTPC.Flatify]
fromConsF [in LambdaTamer.ListT]
fromConsF' [in LambdaTamer.ListT]
fromNilF [in LambdaTamer.ListT]
fromNilF' [in LambdaTamer.ListT]
front'_sound [in LambdaTamer.Binding]
front_sound [in LambdaTamer.Binding]
ftrace_safe [in CTPC.Safety]
ftrace_safe' [in CTPC.Safety]
ftrace_safe_alt [in CTPC.Asmify]
G
getElemT_listF_prover [in LambdaTamer.ListT]
getElemT_listF_prover' [in LambdaTamer.ListT]
get_AllF' [in LambdaTamer.ListT]
get_AllF'_AllF_prover [in LambdaTamer.ListT]
get_AllF_listF_prover' [in LambdaTamer.ListT]
get_AllF_listF_prover'' [in LambdaTamer.ListT]
get_AllF_prover [in LambdaTamer.ListT]
get_AllF_prover' [in LambdaTamer.ListT]
get_elemT_listF_prover'' [in LambdaTamer.ListT]
get_elemT_map [in LambdaTamer.ListT]
get_mapF [in LambdaTamer.ListT]
grabCproj''_sound [in CTPC.CCify]
grabCproj'_sound [in CTPC.CCify]
grabCproj_sound [in CTPC.CCify]
grabVar_sound [in LambdaTamer.Binding]
H
head_AllF [in LambdaTamer.ListT]
head_AllF' [in LambdaTamer.ListT]
I
ifVar_sound [in CTPC.Contify]
initRoots_In [in CTPC.Asmify]
initRoots_incl [in CTPC.Asmify]
initRoots_In' [in CTPC.Asmify]
initRoots_NotIn [in CTPC.Asmify]
initRoots_NotIn' [in CTPC.Asmify]
init_bound_incl [in CTPC.Safety]
insert_sound [in CTPC.Allocify]
insert_sound [in CTPC.CPSify]
internal_nthI [in CTPC.Allocify]
inversion_Subst_cons [in LambdaTamer.Binding]
inversion_Subst_nil [in LambdaTamer.Binding]
invert_cfuncs_cons [in CTPC.CCify]
invert_cfuncs_cons' [in CTPC.CCify]
invert_cfuncs_nil [in CTPC.CCify]
invert_cfuncs_nil' [in CTPC.CCify]
invert_listF_cons [in LambdaTamer.ListT]
invert_listF_nil [in LambdaTamer.ListT]
In_init_bound [in CTPC.Asmify]
In_init_bound [in CTPC.Safety]
isomorphic_new [in CTPC.Safety]
isomorphic_pointers_monotone [in CTPC.Safety]
isomorphic_pointers_refl [in CTPC.Asmify]
isomorphic_pointers_trans [in CTPC.Asmify]
isomorphic_slots_call [in CTPC.Asmify]
isomorphic_slots_mono [in CTPC.Safety]
isomorphic_slots_monotone [in CTPC.Safety]
isomorphic_slots_refl [in CTPC.Asmify]
isomorphic_slots_set [in CTPC.Asmify]
isomorphic_slots_trans [in CTPC.Asmify]
isomorphic_values_lr [in CTPC.Asmify]
isomorphic_values_monotone [in CTPC.Safety]
isomorphic_values_trans [in CTPC.Asmify]
isSmalls_nil [in CTPC.Allocify]
isSmalls_obvious [in CTPC.Allocify]
isSmall'_obvious [in CTPC.Allocify]
isSmall_obvious [in CTPC.Allocify]
K
keys_empty [in CTPC.Dict]
keys_init [in CTPC.Asmify]
keys_ok [in CTPC.Dict]
keys_ok' [in CTPC.Dict]
keys_upd [in CTPC.Dict]
L
lastVar'_sound [in LambdaTamer.Binding]
lastVar_sound [in LambdaTamer.Binding]
length_allocTys [in CTPC.Allocify]
length_app_cons [in LambdaTamer.ListUtil]
length_args [in CTPC.Allocify]
length_revApp_nil [in CTPC.Asmify]
liftEnd'_sound [in LambdaTamer.Binding]
liftEnd_sound [in LambdaTamer.Binding]
liftMiddle_cons_sound [in LambdaTamer.Binding]
liftMiddle_sound [in LambdaTamer.Binding]
liftSubst'_sound [in LambdaTamer.Binding]
lift''_sound [in LambdaTamer.AutoSyntax]
lift'_sound [in LambdaTamer.AutoSyntax]
lift_sound [in LambdaTamer.AutoSyntax]
listF_AllF [in LambdaTamer.ListT]
listF_prover [in LambdaTamer.ListT]
listF_prover' [in LambdaTamer.ListT]
listF_prover'' [in LambdaTamer.ListT]
M
mapCompose [in LambdaTamer.ListT]
mapF'_compose [in LambdaTamer.ListT]
mapF'_In [in LambdaTamer.ListT]
mapIdempotent [in LambdaTamer.ListT]
mapT_appT [in LambdaTamer.AutoSyntax]
mapT_InT [in LambdaTamer.ListT]
map_AllF [in LambdaTamer.ListT]
map_AllF_prover [in LambdaTamer.ListT]
map_app [in LambdaTamer.ListUtil]
map_id [in LambdaTamer.ListUtil]
map_length [in CTPC.Asmify]
meaningDenote_change [in LambdaTamer.AutoSyntax]
mem_nil_end [in CTPC.Allocify]
multiSwap_sound [in LambdaTamer.Binding]
N
negb_prop [in CTPC.Allocify]
negb_true_intro [in CTPC.Allocify]
NotIn_init_bound [in CTPC.Asmify]
nthFuncs_contra [in CTPC.Allocify]
nthFuncs_larges [in CTPC.Allocify]
nthI_mapI [in LambdaTamer.ListUtil]
nthI_mapI' [in CTPC.Safety]
nth_error_bound [in LambdaTamer.ListUtil]
nth_error_grab [in LambdaTamer.ListUtil]
nth_error_grab' [in LambdaTamer.ListUtil]
nth_error_grab_last [in LambdaTamer.ListUtil]
nth_error_monotone [in LambdaTamer.ListUtil]
nth_error_total [in CTPC.Safety]
nth_mapI_list [in CTPC.Asmify]
O
oprimop_lift_sound [in CTPC.Contify]
option_inj [in LambdaTamer.ListT]
P
permuteVar_sound [in LambdaTamer.Binding]
permute'_sound [in LambdaTamer.AutoSyntax]
permute_sound [in LambdaTamer.AutoSyntax]
precondition_safe [in CTPC.Safety]
prover_AllF [in LambdaTamer.ListT]
R
remover_eq [in CTPC.Asmify]
remover_mono [in CTPC.Asmify]
remover_neq1 [in CTPC.Asmify]
remover_neq2 [in CTPC.Asmify]
remover_neq2_cp [in CTPC.Asmify]
retype_elemT_ident [in LambdaTamer.ListT]
retype_listF_ident [in LambdaTamer.ListT]
retype_Subst_cons [in LambdaTamer.AutoSyntax]
retype_Subst_ident [in LambdaTamer.AutoSyntax]
retype_term_ident [in LambdaTamer.AutoSyntax]
retype_Var_ident [in LambdaTamer.Binding]
revAppN_app [in LambdaTamer.ListUtil]
revAppN_length [in LambdaTamer.ListUtil]
revAppN_split [in LambdaTamer.ListUtil]
revAppN_Subst_app [in LambdaTamer.Binding]
revApp_app [in LambdaTamer.ListUtil]
revApp_ass [in CTPC.CCify]
revApp_inj [in CTPC.Safety]
revApp_nil [in LambdaTamer.ListUtil]
rev_length [in LambdaTamer.ListUtil]
rootsIn_In [in CTPC.Asmify]
rootsIn_notIn [in CTPC.Asmify]
roots_backup [in CTPC.Asmify]
runsTo_Call [in CTPC.Trace]
runsTo_runTrace_trans [in CTPC.Trace]
runsTo_Self [in CTPC.Trace]
runsTo_shape [in CTPC.Trace]
runsTo_trans [in CTPC.Trace]
runTrace_shape [in CTPC.Trace]
runTrace_shape_inv [in CTPC.Trace]
S
self_revAppN [in LambdaTamer.ListUtil]
sel_empty [in CTPC.Dict]
sel_upd_eq [in CTPC.Dict]
sel_upd_ne [in CTPC.Dict]
slots_args_app [in CTPC.Flatify]
slots_args_app1 [in CTPC.Flatify]
slots_lr_call [in CTPC.Asmify]
slots_lr_valid [in CTPC.Asmify]
slots_Subst_func [in CTPC.Flatify]
slots_Subst_sound [in CTPC.Flatify]
slots_Subst_upd [in CTPC.Flatify]
splice_sound [in CTPC.Allocify]
splitCtysSubst [in CTPC.CCify]
stashSlots_early [in CTPC.Flatify]
stashSlots_late [in CTPC.Flatify]
stashSlots_sound [in CTPC.Flatify]
stashType_early [in CTPC.Flatify]
stashType_early' [in CTPC.Flatify]
stashType_late [in CTPC.Flatify]
stashType_sound [in CTPC.Flatify]
stash_bounded [in CTPC.Safety]
stash_bound_has [in CTPC.Safety]
stash_bound_mono [in CTPC.Safety]
stash_soundness [in CTPC.Flatify]
strengthen'_sound [in LambdaTamer.AutoSyntax]
strengthen_app_sound [in LambdaTamer.AutoSyntax]
strengthen_app_sound [in CTPC.CCify]
strengthen_First [in LambdaTamer.Binding]
strengthen_Next_false [in LambdaTamer.Binding]
strengthen_Next_true [in LambdaTamer.Binding]
strengthen_SCons_false [in LambdaTamer.Binding]
strengthen_SCons_true [in LambdaTamer.Binding]
strengthen_sound [in LambdaTamer.AutoSyntax]
SubstU_lr_Var [in LambdaTamer.Binding]
subst_comm [in LambdaTamer.AutoSyntax]
Subst_decomp [in LambdaTamer.Binding]
Subst_invert_cons [in LambdaTamer.Binding]
Subst_invert_cons' [in LambdaTamer.Binding]
Subst_invert_nil [in LambdaTamer.Binding]
Subst_invert_nil' [in LambdaTamer.Binding]
Subst_lr_fold [in CTPC.Allocify]
Subst_lr_monotone [in CTPC.Allocify]
Subst_lr_Var [in LambdaTamer.Binding]
Subst_lr_Var [in CTPC.CPSify]
Subst_revAppN_split [in LambdaTamer.Binding]
Subst_revAppN_split' [in LambdaTamer.Binding]
Subst_strengthen_all [in LambdaTamer.Binding]
swap_sound [in CTPC.Contify]
T
tail''_tail [in CTPC.CCify]
tail'_split [in CTPC.CCify]
tail'_tail [in CTPC.CCify]
tail'_tail_pf [in CTPC.CCify]
tail_AllF [in LambdaTamer.ListT]
tail_AllF' [in LambdaTamer.ListT]
tail_split [in CTPC.CCify]
tail_split_pf [in CTPC.CCify]
termDenote_ass [in LambdaTamer.Binding]
termDenote_cons_ass [in LambdaTamer.Binding]
term_incl [in LambdaTamer.AutoSyntax]
traceShape_eq [in CTPC.Trace]
trace_eq [in CTPC.Trace]
trace_precondition [in CTPC.Asmify]
U
unfold_computation [in LambdaTamer.Computation]
unT_appT [in LambdaTamer.AutoSyntax]
unT_enT [in LambdaTamer.AutoSyntax]
unT_enT_app [in LambdaTamer.AutoSyntax]
upd_early [in CTPC.Flatify]
upd_inj [in CTPC.Dict]
V
validPath_monotone [in CTPC.Safety]
vals_lr_monotone [in CTPC.Allocify]
val_lr_monotone [in CTPC.Allocify]
varInfo_all_incl [in LambdaTamer.Binding]
varInfo_apply_all [in LambdaTamer.Binding]
varInfo_apply_drop [in LambdaTamer.Binding]
varInfo_apply_pad [in LambdaTamer.Binding]
varInfo_apply_take [in LambdaTamer.Binding]
varInfo_apply_take_drop [in LambdaTamer.Binding]
varInfo_double_join_incl [in LambdaTamer.Binding]
varInfo_drop_app [in LambdaTamer.Binding]
varInfo_fold_incl_acc [in LambdaTamer.Binding]
varInfo_fold_incl_acc' [in LambdaTamer.Binding]
varInfo_fold_incl_acc'' [in LambdaTamer.Binding]
varInfo_fold_incl_ls [in LambdaTamer.Binding]
varInfo_incl_drop [in LambdaTamer.Binding]
varInfo_incl_refl [in LambdaTamer.Binding]
varInfo_incl_split [in LambdaTamer.Binding]
varInfo_incl_take [in LambdaTamer.Binding]
varInfo_incl_take_drop [in LambdaTamer.Binding]
varInfo_incl_trans [in LambdaTamer.Binding]
varInfo_join_incl [in LambdaTamer.Binding]
varInfo_join_incl1 [in LambdaTamer.Binding]
varInfo_join_incl2 [in LambdaTamer.Binding]
varInfo_keep_incl [in LambdaTamer.Binding]
varInfo_take_app [in LambdaTamer.Binding]
VarNil_sound [in LambdaTamer.Binding]
Var_app_split [in CTPC.Allocify]
var_incl [in LambdaTamer.AutoSyntax]
Var_invert [in LambdaTamer.Binding]
Var_invert' [in LambdaTamer.Binding]
Var_revAppN_split [in CTPC.Allocify]
Var_split [in LambdaTamer.Binding]
Var_strengthen_sound [in LambdaTamer.Binding]
Constructor Index
A
AACons [in CTPC.Alloc]
AANil [in CTPC.Alloc]
AApply [in CTPC.Alloc]
ABind [in CTPC.Alloc]
ABindB [in CTPC.Allocify]
ACode [in CTPC.Alloc]
ACodeptr [in CTPC.Alloc]
AConst [in CTPC.Alloc]
AFBody [in CTPC.Alloc]
AFinal [in CTPC.Allocify]
AFLam [in CTPC.Alloc]
AllF_cons [in LambdaTamer.ListT]
AllF_nil [in LambdaTamer.ListT]
ANat [in CTPC.Alloc]
ANew [in CTPC.Alloc]
AProj [in CTPC.Alloc]
ARef [in CTPC.Alloc]
Assign [in CTPC.Asm]
AVar [in CTPC.Alloc]
B
Bind [in LambdaTamer.Computation]
C
CACons [in CTPC.CC]
Call [in CTPC.Trace]
CallShape [in CTPC.Trace]
CANil [in CTPC.CC]
CApply [in CTPC.CC]
CBind [in CTPC.CC]
CBool [in examples.CPS]
CCall [in examples.CPS]
CClosure [in CTPC.CC]
CCode [in CTPC.CC]
CConst [in CTPC.CC]
CConst [in examples.CPS]
CCont [in CTPC.CC]
CCont [in examples.CPS]
CFBody [in CTPC.CC]
CFCons [in CTPC.CC]
CFLam [in CTPC.CC]
CFNil [in CTPC.CC]
CFst [in examples.CPS]
CLam [in examples.CPS]
CLet [in examples.CPS]
CNat [in CTPC.CC]
consF [in LambdaTamer.ListT]
Const [in CTPC.Asm]
consT [in LambdaTamer.ListT]
Construct [in LambdaTamer.AutoSyntax]
CPair [in examples.CPS]
CPFst [in CTPC.CC]
CProd [in examples.CPS]
CProd [in CTPC.CC]
CProj [in CTPC.CC]
CPSnd [in CTPC.CC]
Crash [in CTPC.Trace]
CrashShape [in CTPC.Trace]
CSnd [in examples.CPS]
CVar [in CTPC.CC]
CVar [in examples.CPS]
E
EraseBind [in LambdaTamer.Computation]
EraseDrop [in LambdaTamer.Computation]
EraseReturn [in LambdaTamer.Computation]
F
FACons [in CTPC.Flat]
FANil [in CTPC.Flat]
First [in LambdaTamer.Binding]
firstT [in LambdaTamer.ListT]
FJump [in CTPC.Flat]
FSlot [in CTPC.Flat]
Fun [in LambdaTamer.AutoSyntax]
J
Jump [in CTPC.Asm]
N
New [in CTPC.Asm]
Next [in LambdaTamer.Binding]
nextT [in LambdaTamer.ListT]
nilF [in LambdaTamer.ListT]
nilT [in LambdaTamer.ListT]
NoneT [in LambdaTamer.ListT]
O
OACons [in CTPC.Cont]
OANil [in CTPC.Cont]
OApply [in CTPC.Cont]
OBind [in CTPC.Cont]
OCCons [in CTPC.Cont]
OCNil [in CTPC.Cont]
OConst [in CTPC.Cont]
OCont [in CTPC.Cont]
OLam [in CTPC.Cont]
ONat [in CTPC.Cont]
Output [in CTPC.Trace]
OutputShape [in CTPC.Trace]
OVar [in CTPC.Cont]
P
PApply [in CTPC.CPS]
PBind [in CTPC.CPS]
PConst [in CTPC.CPS]
PLam [in CTPC.CPS]
Proj [in CTPC.Asm]
PThrow [in CTPC.CPS]
PVar [in CTPC.CPS]
R
Return [in LambdaTamer.Computation]
Run [in LambdaTamer.Computation]
RunCall [in CTPC.Trace]
RunCall' [in CTPC.Trace]
RunOutput [in CTPC.Trace]
RunOutput' [in CTPC.Trace]
RunTo_Call [in CTPC.Trace]
RunTo_Call' [in CTPC.Trace]
RunTo_Self [in CTPC.Trace]
RunTo_Self' [in CTPC.Trace]
S
SApp [in examples.CPS]
SApp [in CTPC.Source]
SArrow [in CTPC.Source]
SArrow [in examples.CPS]
SBool [in examples.CPS]
SCons [in LambdaTamer.Binding]
SConst [in examples.CPS]
SConst [in CTPC.Source]
SFst [in examples.CPS]
SLam [in examples.CPS]
SLam [in CTPC.Source]
Slot [in CTPC.Asm]
SlrU_Cons [in LambdaTamer.Binding]
SlrU_Nil [in LambdaTamer.Binding]
Slr_Cons [in LambdaTamer.Binding]
Slr_Nil [in LambdaTamer.Binding]
SNat [in CTPC.Source]
SNil [in LambdaTamer.Binding]
SomeT [in LambdaTamer.ListT]
SPair [in examples.CPS]
SProd [in examples.CPS]
SSnd [in examples.CPS]
Subterm [in LambdaTamer.AutoSyntax]
Subvar [in LambdaTamer.AutoSyntax]
SVar [in examples.CPS]
SVar [in CTPC.Source]
T
Traced [in CTPC.Alloc]
U
Untraced [in CTPC.Alloc]
Inductive Index
A
aargs [in CTPC.Alloc]
afunc [in CTPC.Alloc]
alinear [in CTPC.Alloc]
AllF [in LambdaTamer.ListT]
aprimop [in CTPC.Alloc]
aprimopB [in CTPC.Allocify]
aprog [in CTPC.Alloc]
aty [in CTPC.Alloc]
C
cargs [in CTPC.CC]
cexp [in examples.CPS]
cfunc [in CTPC.CC]
cfuncs [in CTPC.CC]
clinear [in CTPC.CC]
computation [in LambdaTamer.Computation]
con [in LambdaTamer.AutoSyntax]
cprimexp [in examples.CPS]
cprimop [in CTPC.CC]
cproj [in CTPC.CC]
cprojTy [in CTPC.CC]
cty [in examples.CPS]
cty [in CTPC.CC]
cwithProg [in CTPC.CC]
E
elemT [in LambdaTamer.ListT]
erase [in LambdaTamer.Computation]
F
fargs [in CTPC.Flat]
flinear [in CTPC.Flat]
fprimop [in CTPC.Flat]
fprog [in CTPC.Flat]
G
genop [in CTPC.Asm]
I
instrs [in CTPC.Asm]
L
listF [in LambdaTamer.ListT]
listT [in LambdaTamer.ListT]
M
meaning [in LambdaTamer.AutoSyntax]
O
oargs [in CTPC.Cont]
ocont [in CTPC.Cont]
olinear [in CTPC.Cont]
oprimop [in CTPC.Cont]
optionT [in LambdaTamer.ListT]
oty [in CTPC.Cont]
P
plinear [in CTPC.CPS]
pprimop [in CTPC.CPS]
program [in CTPC.Asm]
R
run [in LambdaTamer.Computation]
runsTo [in CTPC.Trace]
runsTo' [in CTPC.Trace]
runtime [in CTPC.Asm]
runTrace [in CTPC.Trace]
runTrace' [in CTPC.Trace]
S
sterm [in CTPC.Source]
sterm [in examples.CPS]
sty [in examples.CPS]
sty [in CTPC.Source]
Subst [in LambdaTamer.Binding]
SubstU_lr [in LambdaTamer.Binding]
Subst_lr [in LambdaTamer.Binding]
T
tag [in CTPC.Alloc]
trace [in CTPC.Trace]
traceShape [in CTPC.Trace]
V
Var [in LambdaTamer.Binding]
Definition Index
A
A [in CTPC.Dict]
A [in CTPC.Flat]
A [in CTPC.Dict]
aargsDenote [in CTPC.Alloc]
aargsTy [in CTPC.Alloc]
aBind [in CTPC.AllocMonad]
aBottom [in CTPC.AllocMonad]
adom [in CTPC.Alloc]
aformalsDenote [in CTPC.Alloc]
afuncBody [in CTPC.Flatify]
afuncDenote [in CTPC.Alloc]
afuncTy [in CTPC.Alloc]
alinearDenote [in CTPC.Alloc]
alinearTy [in CTPC.Alloc]
allocArgs [in CTPC.Allocify]
allocCode [in CTPC.Allocify]
allocCode_soundness [in CTPC.Allocify]
allocFunc [in CTPC.Allocify]
allocFuncs [in CTPC.Allocify]
allocFuncTys [in CTPC.Allocify]
allocLinear [in CTPC.Allocify]
allocM [in CTPC.AllocMonad]
allocPrimop [in CTPC.Allocify]
allocProg [in CTPC.Allocify]
allocProj [in CTPC.Allocify]
allocSpec [in CTPC.AllocMonad]
allocTy [in CTPC.Allocify]
allocTys [in CTPC.Allocify]
allocVar [in CTPC.Allocify]
allocVar' [in CTPC.Allocify]
AllS2 [in CTPC.Asm]
all_elemT [in LambdaTamer.AutoSyntax]
amakeTrace [in CTPC.Alloc]
aNew [in CTPC.AllocMonad]
appCfuncs [in CTPC.CCify]
appF [in LambdaTamer.ListT]
appSubst [in LambdaTamer.Binding]
appSubstF [in LambdaTamer.AutoSyntax]
appT [in LambdaTamer.ListT]
appT [in LambdaTamer.AutoSyntax]
aprimopBDenote [in CTPC.Allocify]
aprimopDenote [in CTPC.Alloc]
aprimopTy [in CTPC.Alloc]
aprogDenote [in CTPC.Alloc]
aRead [in CTPC.AllocMonad]
aReturn [in CTPC.AllocMonad]
argsDenote [in CTPC.Asm]
args_bound [in CTPC.Flatify]
args_early [in CTPC.Flatify]
args_lr [in CTPC.Asmify]
args_lr [in CTPC.Allocify]
args_lr [in CTPC.CCify]
args_lr [in CTPC.Flatify]
args_max [in CTPC.Flatify]
asmArgs [in CTPC.Asmify]
asmLinear [in CTPC.Asmify]
asmPrimop [in CTPC.Asmify]
asmProg [in CTPC.Asmify]
atyDenote [in CTPC.Alloc]
atys [in CTPC.Alloc]
atys_eq_dec [in CTPC.Alloc]
aty_eq_dec [in CTPC.Alloc]
augmentSubst [in CTPC.Flatify]
A_eq_dec [in CTPC.Flat]
B
bindCfunc [in CTPC.CCify]
buildEnv [in CTPC.CCify]
buildEnv' [in CTPC.CCify]
C
cargsDenote [in CTPC.CC]
ccArgs [in CTPC.CCify]
ccPrimop [in CTPC.CCify]
ccTy [in CTPC.CCify]
ccTys [in CTPC.CCify]
cexpDenote [in examples.CPS]
cfhead [in CTPC.CCify]
cfprog [in CTPC.CCify]
cfprogDenote [in CTPC.CCify]
cfuncDenote [in CTPC.CC]
cfuncsDenote [in CTPC.CC]
cfuncTyDenote [in CTPC.CC]
checkTag [in CTPC.Alloc]
clinearDenote [in CTPC.CC]
close [in CTPC.CCify]
close' [in CTPC.CCify]
close'' [in CTPC.CCify]
compile_term [in CTPC.Compile]
compile_term' [in CTPC.Compile]
compose [in CTPC.CPSify]
cons [in LambdaTamer.AutoSyntax]
cons [in LambdaTamer.AutoSyntax]
consI [in LambdaTamer.ListUtil]
conSig [in LambdaTamer.AutoSyntax]
consS [in LambdaTamer.ListT]
contifyLinear [in CTPC.Contify]
contifyPrimop [in CTPC.Contify]
contifyTy [in CTPC.Contify]
contTy [in examples.CPS]
cont_lr [in CTPC.CCify]
con_builder [in LambdaTamer.AutoSyntax]
con_ih [in LambdaTamer.AutoSyntax]
copy [in CTPC.Flatify]
copySlots [in CTPC.Flatify]
copyType [in CTPC.Flatify]
copy_bound [in CTPC.Safety]
cpprog [in CTPC.CCify]
cpprogDenote [in CTPC.CCify]
cprimexpDenote [in examples.CPS]
cprimopDenote [in CTPC.CC]
cprog [in CTPC.CC]
cprogDenote [in CTPC.CC]
cprojDenote [in CTPC.CC]
cprojTyDenote [in CTPC.CC]
cps [in CTPC.CPSify]
cpsTerm [in examples.CPS]
cpsTy [in examples.CPS]
cresultDenote [in CTPC.CC]
ctyDenote [in examples.CPS]
ctyDenote [in CTPC.CC]
ctys [in CTPC.CC]
ctysDenote [in CTPC.CC]
ctysDenote_tail [in CTPC.CCify]
ctysDenote_tail' [in CTPC.CCify]
ctysDenote_tail'' [in CTPC.CCify]
ctysSubst [in CTPC.CC]
cty_ind' [in CTPC.Allocify]
cwithProgDenote [in CTPC.CC]
D
default [in CTPC.Dict]
dict [in CTPC.Dict]
dict_eq_dec [in CTPC.Dict]
drop [in LambdaTamer.ListUtil]
dty [in LambdaTamer.AutoSyntax]
dty [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
dtyDenote [in LambdaTamer.AutoSyntax]
E
elemify [in LambdaTamer.AutoSyntax]
elemT_absurd [in LambdaTamer.ListT]
embed [in LambdaTamer.Binding]
embed' [in LambdaTamer.Binding]
empty [in CTPC.Dict]
enT [in LambdaTamer.AutoSyntax]
equations_type [in LambdaTamer.AutoSyntax]
eq_app [in LambdaTamer.Binding]
eq_cons [in LambdaTamer.Binding]
etaF [in LambdaTamer.AutoSyntax]
exp_lr [in CTPC.CPSify]
extendSubst [in LambdaTamer.AutoSyntax]
F
fargsDenote [in CTPC.Flat]
fargs_bounded [in CTPC.Safety]
flatArgs [in CTPC.Flatify]
flatCall [in CTPC.Flatify]
flatContext [in CTPC.Flat]
flatContext' [in CTPC.Flat]
flatFunc [in CTPC.Flatify]
flatLinear [in CTPC.Flatify]
flatPrimop [in CTPC.Flatify]
flatProg [in CTPC.Flatify]
flatVar [in CTPC.Flatify]
flinearDenote [in CTPC.Flat]
flinear_bounded [in CTPC.Safety]
fmakeTrace [in CTPC.Flat]
followPath [in CTPC.Safety]
fprecondition [in CTPC.Flat]
fprimopDenote [in CTPC.Flat]
fprimop_bounded [in CTPC.Safety]
fprogDenote [in CTPC.Flat]
freeVars [in LambdaTamer.AutoSyntax]
freeVars [in LambdaTamer.AutoSyntax]
freeVars [in LambdaTamer.AutoSyntax]
frob_args [in CTPC.Flatify]
front [in LambdaTamer.Binding]
frontVar [in LambdaTamer.Binding]
frontVar' [in LambdaTamer.Binding]
front' [in LambdaTamer.Binding]
ftyping [in CTPC.Flat]
funcs_lr [in CTPC.Allocify]
func_lr [in CTPC.Allocify]
G
genopDenote [in CTPC.Asm]
getLarge [in CTPC.Allocify]
getTerm [in LambdaTamer.AutoSyntax]
getVar [in LambdaTamer.AutoSyntax]
get_AllF [in LambdaTamer.ListT]
get_elemT [in LambdaTamer.ListT]
get_traceShape [in CTPC.Trace]
grabCproj [in CTPC.CCify]
grabCproj' [in CTPC.CCify]
grabCproj'' [in CTPC.CCify]
grabVar [in LambdaTamer.Binding]
H
head [in LambdaTamer.Binding]
headF [in LambdaTamer.ListT]
headF' [in LambdaTamer.ListT]
headI [in LambdaTamer.ListUtil]
headS [in LambdaTamer.ListT]
headS' [in LambdaTamer.ListT]
I
ifVar [in CTPC.Contify]
initRoots [in CTPC.Asmify]
init_bound [in CTPC.Safety]
insert [in examples.CPS]
insert [in CTPC.Allocify]
insert [in CTPC.CPSify]
insert2 [in examples.CPS]
insert2_sound [in examples.CPS]
insert_sound [in examples.CPS]
instrsDenote [in CTPC.Asm]
InT [in LambdaTamer.ListT]
isLarges [in CTPC.Allocify]
isLarges' [in CTPC.Allocify]
isomorphic_args [in CTPC.Safety]
isomorphic_pointers [in CTPC.Safety]
isomorphic_slots [in CTPC.Safety]
isomorphic_values [in CTPC.Safety]
isSmall [in CTPC.CC]
isSmalls [in CTPC.CC]
isSmalls' [in CTPC.CC]
isSmall' [in CTPC.CC]
K
keys [in CTPC.Dict]
L
lastVar [in LambdaTamer.Binding]
lastVar' [in LambdaTamer.Binding]
lengthF [in LambdaTamer.ListT]
lengthT [in LambdaTamer.ListT]
lift [in LambdaTamer.AutoSyntax]
lift [in LambdaTamer.AutoSyntax]
lift [in LambdaTamer.AutoSyntax]
liftEnd [in LambdaTamer.Binding]
liftEnd' [in LambdaTamer.Binding]
liftMiddle [in LambdaTamer.Binding]
liftSubst' [in LambdaTamer.Binding]
liftVar [in LambdaTamer.Binding]
liftVarEnd [in LambdaTamer.Binding]
liftVar' [in LambdaTamer.Binding]
lift' [in LambdaTamer.AutoSyntax]
lift' [in LambdaTamer.AutoSyntax]
lift' [in LambdaTamer.AutoSyntax]
lift'' [in LambdaTamer.AutoSyntax]
lift'' [in LambdaTamer.AutoSyntax]
lift'' [in LambdaTamer.AutoSyntax]
lift''_sound [in LambdaTamer.AutoSyntax]
lift'_sound [in LambdaTamer.AutoSyntax]
lift_sound [in LambdaTamer.AutoSyntax]
linear_lr [in CTPC.Flatify]
linear_lr [in CTPC.CCify]
linear_lr [in CTPC.Contify]
listI [in LambdaTamer.ListUtil]
listS [in LambdaTamer.ListT]
M
makeActuals [in CTPC.Alloc]
makeTm [in LambdaTamer.AutoSyntax]
makeTrace [in CTPC.Asm]
mapElemT [in LambdaTamer.ListT]
mapF [in LambdaTamer.ListT]
mapF' [in LambdaTamer.ListT]
mapI [in LambdaTamer.ListUtil]
mapI_list [in CTPC.Asmify]
mapT [in LambdaTamer.ListT]
meaningDenote [in LambdaTamer.AutoSyntax]
mem [in CTPC.AllocMonad]
mem0 [in CTPC.Compile]
multiSwap [in LambdaTamer.Binding]
N
nilI [in LambdaTamer.ListUtil]
nilS [in LambdaTamer.ListT]
nthFuncs [in CTPC.Allocify]
nthI [in LambdaTamer.ListUtil]
nthT [in LambdaTamer.ListT]
O
oargsDenote [in CTPC.Cont]
ocontDenote [in CTPC.Cont]
ocontTy [in CTPC.Cont]
olinearDenote [in CTPC.Cont]
oprimopDenote [in CTPC.Cont]
oresultDenote [in CTPC.Cont]
otyDenote [in CTPC.Cont]
otys [in CTPC.Cont]
otysDenote [in CTPC.Cont]
P
permute [in LambdaTamer.AutoSyntax]
permute [in LambdaTamer.AutoSyntax]
permute [in LambdaTamer.AutoSyntax]
permuteVar [in LambdaTamer.Binding]
permute' [in LambdaTamer.AutoSyntax]
permute_sound [in LambdaTamer.AutoSyntax]
pexpDenote [in CTPC.CPS]
plinearDenote [in CTPC.CPS]
pprimopDenote [in CTPC.CPS]
primop_lr [in CTPC.CCify]
primop_lr [in CTPC.Allocify]
primop_lr [in CTPC.Contify]
primop_lr [in CTPC.Flatify]
programDenote [in CTPC.Asm]
prog_lr [in CTPC.Flatify]
prog_lr [in CTPC.Allocify]
ptyDenote [in CTPC.CPS]
R
read_ctys [in CTPC.CCify]
read_ctys' [in CTPC.CCify]
read_ctys'' [in CTPC.CCify]
remover [in CTPC.Asmify]
result [in CTPC.Continuation]
result [in CTPC.Cont]
retype_elemT [in LambdaTamer.ListT]
retype_listF [in LambdaTamer.ListT]
retype_Subst [in LambdaTamer.AutoSyntax]
retype_term [in LambdaTamer.AutoSyntax]
retype_Var [in LambdaTamer.Binding]
revApp [in LambdaTamer.ListUtil]
revAppN [in LambdaTamer.ListUtil]
revAppN_Subst [in LambdaTamer.Binding]
rootsIn [in CTPC.Asm]
roots_grabber [in CTPC.Asmify]
rty [in LambdaTamer.AutoSyntax]
rty [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
rtyDenote [in LambdaTamer.AutoSyntax]
S
sel [in CTPC.Dict]
sel' [in CTPC.Dict]
set [in LambdaTamer.ListT]
slots [in CTPC.Flat]
slots_actuals [in CTPC.Flatify]
slots_args [in CTPC.Flatify]
slots_args' [in CTPC.Flatify]
slots_lr [in CTPC.Asmify]
slots_Subst [in CTPC.Flatify]
slots_Subst' [in CTPC.Flatify]
smallCty [in CTPC.CC]
smallCtys [in CTPC.CC]
splice [in CTPC.Allocify]
stash [in CTPC.Flatify]
stashSlots [in CTPC.Flatify]
stashType [in CTPC.Flatify]
stash_bound [in CTPC.Safety]
stermDenote [in CTPC.Source]
stermDenote [in examples.CPS]
store [in CTPC.Asm]
strengthen [in LambdaTamer.AutoSyntax]
strengthen [in LambdaTamer.AutoSyntax]
strengthen [in LambdaTamer.AutoSyntax]
strengthen' [in LambdaTamer.AutoSyntax]
strengthen_app [in LambdaTamer.AutoSyntax]
strengthen_app [in LambdaTamer.AutoSyntax]
strengthen_app [in LambdaTamer.AutoSyntax]
strengthen_app_sound [in LambdaTamer.AutoSyntax]
strengthen_sound [in LambdaTamer.AutoSyntax]
styDenote [in CTPC.Source]
styDenote [in examples.CPS]
substVar [in LambdaTamer.Binding]
substVar' [in LambdaTamer.Binding]
Subst_drop [in LambdaTamer.Binding]
Subst_lr [in CTPC.Contify]
Subst_lr [in CTPC.CPSify]
Subst_lr [in CTPC.Allocify]
Subst_lr [in CTPC.CCify]
Subst_lr [in examples.CPS]
Subst_strengthen [in LambdaTamer.Binding]
swap [in CTPC.Contify]
T
tagof [in CTPC.Alloc]
tag_eq_dec [in CTPC.Alloc]
tail [in LambdaTamer.Binding]
tailF [in LambdaTamer.ListT]
tailF' [in LambdaTamer.ListT]
tailI [in LambdaTamer.ListUtil]
tailS [in LambdaTamer.ListT]
tailS' [in LambdaTamer.ListT]
term [in LambdaTamer.AutoSyntax]
term [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termDenote [in LambdaTamer.AutoSyntax]
termNil [in LambdaTamer.Binding]
term_lr [in examples.CPS]
term_rect [in LambdaTamer.AutoSyntax]
term_rect [in LambdaTamer.AutoSyntax]
term_rect_cons [in LambdaTamer.AutoSyntax]
U
unT [in LambdaTamer.AutoSyntax]
unT_cons [in LambdaTamer.AutoSyntax]
unvalify [in LambdaTamer.AutoSyntax]
upd [in CTPC.Dict]
updateRoots [in CTPC.Asmify]
V
valComp [in CTPC.Asm]
validPath [in CTPC.Safety]
vals_lr [in CTPC.CCify]
vals_lr [in CTPC.Allocify]
val_lr [in CTPC.Contify]
val_lr [in CTPC.Flatify]
val_lr [in CTPC.CPSify]
val_lr [in examples.CPS]
val_lr [in CTPC.Asmify]
val_lr [in CTPC.CCify]
val_lr [in CTPC.Allocify]
VarConvert [in LambdaTamer.Binding]
VarDenote [in LambdaTamer.Binding]
varInfo [in LambdaTamer.Binding]
varInfo_all [in LambdaTamer.Binding]
varInfo_app [in LambdaTamer.Binding]
varInfo_apply [in LambdaTamer.Binding]
varInfo_drop [in LambdaTamer.Binding]
varInfo_incl [in LambdaTamer.Binding]
varInfo_join [in LambdaTamer.Binding]
varInfo_keep [in LambdaTamer.Binding]
varInfo_none [in LambdaTamer.Binding]
varInfo_pad [in LambdaTamer.Binding]
varInfo_take [in LambdaTamer.Binding]
VarNil [in LambdaTamer.Binding]
Var_freeVars [in LambdaTamer.Binding]
Var_strengthen [in LambdaTamer.Binding]
W
withCont [in CTPC.Continuation]
withCont_bind [in examples.CPS]
withCont_bind [in CTPC.Continuation]
withCont_compose [in CTPC.Continuation]
withCont_const [in CTPC.Continuation]
Module Index
D
Denote [in LambdaTamer.AutoSyntax]
Denote [in LambdaTamer.AutoSyntax]
DENOTE_PARAM [in LambdaTamer.AutoSyntax]
DENOTE_PARAM [in LambdaTamer.AutoSyntax]
DENOTE_RESULT [in LambdaTamer.AutoSyntax]
DENOTE_RESULT [in LambdaTamer.AutoSyntax]
DICT [in CTPC.Dict]
Dict [in CTPC.Dict]
DICT_DOMAIN [in CTPC.Dict]
M
Make [in LambdaTamer.AutoSyntax]
N
NatDict [in CTPC.Flat]
NatKey [in CTPC.Flat]
P
PARAM [in LambdaTamer.AutoSyntax]
R
RESULT [in LambdaTamer.AutoSyntax]
Library Index
A
Alloc
Allocify
AllocMonad
Asm
Asmify
AutoSyntax
B
Binding
C
CC
CCify
Compile
Computation
Cont
Contify
Continuation
CPS
CPS
CPSify
D
Dict
E
Ext
F
Flat
Flatify
L
LambdaTamer
ListT
ListUtil
S
Safety
Source
T
Tactics
Trace
| 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 |
_ |
(1098 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 |
_ |
(53 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 |
_ |
(408 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 |
_ |
(132 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 |
_ |
(59 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 |
_ |
(404 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 |
_ |
(14 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 |
_ |
(28 entries) |
This page has been generated by coqdoc