| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1309 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (503 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (487 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (64 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (205 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
Global Index
A
Absurd [constructor, in Llanguage]Absurd [constructor, in Flanguage]
acheck [constructor, in typechecker]
Acheck [constructor, in typechecker]
AC2 [constructor, in typechecker]
aenv [abbreviation, in typesystem]
AG [constructor, in typechecker]
agree [inductive, in typechecker]
AH [constructor, in typechecker]
AK [constructor, in typechecker]
and_extensionality [lemma, in ext]
AP [constructor, in typechecker]
App [constructor, in Llanguage]
App [constructor, in Flanguage]
approx [definition, in Fsemantics]
approx_eq [lemma, in Fsemantics]
approx_inc [lemma, in Fsemantics]
approx_swap [lemma, in Fsemantics]
approx_min [lemma, in Fsemantics]
approx_approx [lemma, in Fsemantics]
approx_fold [lemma, in Fsemantics]
approx_unfold [lemma, in Fsemantics]
approx0 [lemma, in Fsemantics]
approx0_eq [lemma, in Fsemantics]
app_insn2 [lemma, in Lnormalization]
app_deln2 [lemma, in Lnormalization]
app_deln_length [lemma, in Lnormalization]
app_insn2 [lemma, in Fsoundness]
app_deln2 [lemma, in Fsoundness]
app_deln_length [lemma, in Fsoundness]
arrow_extensionality [lemma, in ext]
asig [inductive, in typechecker]
Asig [inductive, in typechecker]
AT [constructor, in typechecker]
atc [definition, in typechecker]
Atc [definition, in typechecker]
atcj [definition, in typechecker]
Awf [constructor, in typechecker]
B
BadSyntax [constructor, in typechecker]binary_fuel_unary [lemma, in Flanguage]
binary_fuel_lift [lemma, in Flanguage]
binary_fuel_refl [lemma, in Flanguage]
binary_fuel_trans [lemma, in Flanguage]
binary_fuel_map_trivial [lemma, in Flanguage]
binary_fuel_map [lemma, in Flanguage]
binary_fuel [definition, in Flanguage]
bind [definition, in typechecker]
C
C [record, in Lsemantics]C [record, in Fsemantics]
CAEnv [constructor, in typesystem]
ccljudg1 [definition, in typesystemextra]
Cdec [projection, in Fsemantics]
cdrop [definition, in Llanguage]
CE [record, in Lsemantics]
CE [record, in Fsemantics]
CEdec [projection, in Fsemantics]
CEexp [projection, in Lsemantics]
CEexp [projection, in Fsemantics]
CEok [projection, in Fsemantics]
CEred [projection, in Lsemantics]
CEred [projection, in Fsemantics]
CEsn [projection, in Lsemantics]
CE_EBot [lemma, in Lsemantics]
CE_ETop [lemma, in Lsemantics]
CE_EExi [lemma, in Lsemantics]
CE_EPi [lemma, in Lsemantics]
CE_EFor [lemma, in Lsemantics]
CE_ESum [lemma, in Lsemantics]
CE_EVoid [lemma, in Lsemantics]
CE_EProd [lemma, in Lsemantics]
CE_EOne [lemma, in Lsemantics]
CE_EArr [lemma, in Lsemantics]
CE_Cl [lemma, in Lsemantics]
CE_SN [lemma, in Lsemantics]
CE_CPexp [lemma, in Lsemantics]
CE_ [constructor, in Lsemantics]
CE_EMu [lemma, in Fsemantics]
CE_EBot [lemma, in Fsemantics]
CE_ETop [lemma, in Fsemantics]
CE_EExi [lemma, in Fsemantics]
CE_EPi [lemma, in Fsemantics]
CE_EFor [lemma, in Fsemantics]
CE_ESum [lemma, in Fsemantics]
CE_EVoid [lemma, in Fsemantics]
CE_EProd [lemma, in Fsemantics]
CE_EOne [lemma, in Fsemantics]
CE_EArr [lemma, in Fsemantics]
CE_Cl [lemma, in Fsemantics]
CE_CPexp [lemma, in Fsemantics]
CE_ [constructor, in Fsemantics]
CF [definition, in Fsemantics]
CF_iter_F [lemma, in Fsemantics]
CGCons [constructor, in typesystem]
CGNil [constructor, in typesystem]
CHCons [constructor, in typesystem]
CHNil [constructor, in typesystem]
CKind [constructor, in typesystem]
CKOne [constructor, in typesystem]
CKProd [constructor, in typesystem]
CKRes [constructor, in typesystem]
CKStar [constructor, in typesystem]
Cl [inductive, in Lsemantics]
Cl [definition, in Fsemantics]
class [inductive, in typesystem]
classjudg [definition, in typesystemextra]
class_dec [definition, in typesystemdec]
ClExp [constructor, in Lsemantics]
ClR [constructor, in Lsemantics]
Cl_For [lemma, in Lsemantics]
Cl_def [lemma, in Lsemantics]
Cl_approx_For [lemma, in Fsemantics]
Cl_approx_eq [lemma, in Fsemantics]
Cl_approx [lemma, in Fsemantics]
Cl_CE [lemma, in Fsemantics]
Cl_monotone [lemma, in Fsemantics]
Cl_def [lemma, in Fsemantics]
Cmp [definition, in set]
CN [definition, in Llanguage]
CN [definition, in Flanguage]
CNprevalue_is_absurd [lemma, in Llanguage]
CN_drop [lemma, in Llanguage]
CN_red [lemma, in Llanguage]
CN_N [lemma, in Llanguage]
CN_le_term [lemma, in Flanguage]
CN_red [lemma, in Flanguage]
CN_subst [lemma, in Flanguage]
CN_N [lemma, in Flanguage]
cobj [inductive, in typesystem]
cobj_unsubst [lemma, in typesystemextra]
cobj_eq [lemma, in typesystemextra]
cobj_subst [lemma, in typesystemextra]
cobj_unlift [lemma, in typesystemextra]
cobj_lift [lemma, in typesystemextra]
cobj_sound [lemma, in Lnormalization]
cobj_dec_cobj [lemma, in typesystemdec]
cobj_dec [definition, in typesystemdec]
cobj_sound [lemma, in Fsoundness]
Cok [projection, in Fsemantics]
CPAnd [constructor, in typesystem]
CPCoer [constructor, in typesystem]
CPEnv [constructor, in typesystem]
CPExi [constructor, in typesystem]
CPFor [constructor, in typesystem]
CProp [constructor, in typesystem]
CPTrue [constructor, in typesystem]
Cred [projection, in Lsemantics]
Cred [projection, in Fsemantics]
Csn [projection, in Lsemantics]
CST [definition, in Fsemantics]
CST_WF [lemma, in Fsemantics]
CTArr [constructor, in typesystem]
CTBot [constructor, in typesystem]
CTEnv [constructor, in typesystem]
CTFor [constructor, in typesystem]
CTFst [constructor, in typesystem]
CTMu [constructor, in typesystem]
CTOne [constructor, in typesystem]
CTPair [constructor, in typesystem]
CTPi [constructor, in typesystem]
CTProd [constructor, in typesystem]
CTSnd [constructor, in typesystem]
CTSum [constructor, in typesystem]
CTTop [constructor, in typesystem]
CTUnit [constructor, in typesystem]
CTVar [constructor, in typesystem]
CTVoid [constructor, in typesystem]
Ctx [inductive, in Llanguage]
Ctx [inductive, in Flanguage]
CtxAbsurd [constructor, in Llanguage]
CtxAbsurd [constructor, in Flanguage]
CtxApp1 [constructor, in Llanguage]
CtxApp1 [constructor, in Flanguage]
CtxApp2 [constructor, in Llanguage]
CtxApp2 [constructor, in Flanguage]
CtxFst [constructor, in Llanguage]
CtxFst [constructor, in Flanguage]
CtxInl [constructor, in Llanguage]
CtxInl [constructor, in Flanguage]
CtxInr [constructor, in Llanguage]
CtxInr [constructor, in Flanguage]
CtxInst [constructor, in Llanguage]
CtxInst [constructor, in Flanguage]
CtxLam [constructor, in Llanguage]
CtxLam [constructor, in Flanguage]
CtxMatch1 [constructor, in Llanguage]
CtxMatch1 [constructor, in Flanguage]
CtxMatch2 [constructor, in Llanguage]
CtxMatch2 [constructor, in Flanguage]
CtxMatch3 [constructor, in Llanguage]
CtxMatch3 [constructor, in Flanguage]
CtxPair1 [constructor, in Llanguage]
CtxPair1 [constructor, in Flanguage]
CtxPair2 [constructor, in Llanguage]
CtxPair2 [constructor, in Flanguage]
CtxSnd [constructor, in Llanguage]
CtxSnd [constructor, in Flanguage]
CType [constructor, in typesystem]
cut_length [lemma, in list]
Cv [lemma, in Fsemantics]
CYCons [constructor, in typesystem]
CYNil [constructor, in typesystem]
C_EJudg [lemma, in Lsemantics]
C_EBot [lemma, in Lsemantics]
C_ETop [lemma, in Lsemantics]
C_PExi [lemma, in Lsemantics]
C_PPi [lemma, in Lsemantics]
C_EFor [lemma, in Lsemantics]
C_PSum [lemma, in Lsemantics]
C_PVoid [lemma, in Lsemantics]
C_PProd [lemma, in Lsemantics]
C_POne [lemma, in Lsemantics]
C_PArr [lemma, in Lsemantics]
C_Cl [lemma, in Lsemantics]
C_SN [lemma, in Lsemantics]
C_CE [lemma, in Lsemantics]
C_ [constructor, in Lsemantics]
C_EJudg [lemma, in Fsemantics]
C_approx [lemma, in Fsemantics]
C_EBot [lemma, in Fsemantics]
C_ETop [lemma, in Fsemantics]
C_PExi [lemma, in Fsemantics]
C_PPi [lemma, in Fsemantics]
C_EFor [lemma, in Fsemantics]
C_PSum [lemma, in Fsemantics]
C_PVoid [lemma, in Fsemantics]
C_PProd [lemma, in Fsemantics]
C_POne [lemma, in Fsemantics]
C_PArr [lemma, in Fsemantics]
C_Cl [lemma, in Fsemantics]
C_OK [lemma, in Fsemantics]
C_CE [lemma, in Fsemantics]
C_ [constructor, in Fsemantics]
D
Dec [definition, in Fsemantics]DecCN [lemma, in Fsemantics]
DecN [lemma, in Fsemantics]
DecNV [lemma, in Fsemantics]
DecV [definition, in Fsemantics]
deln [definition, in Lnormalization]
deln [definition, in Fsoundness]
der [definition, in Fnormalization]
destruct_Cl_CN [lemma, in Lsemantics]
destruct_Cl_CN [lemma, in Fsemantics]
do_cobj [definition, in typechecker]
drop [definition, in Llanguage]
drop_red_exists [lemma, in Llanguage]
drop_fill [lemma, in Llanguage]
drop_kfill [lemma, in Llanguage]
drop_subst [lemma, in Llanguage]
drop_lift [lemma, in Llanguage]
drop_lower [lemma, in Llanguage]
E
EAbsurd_sem [lemma, in Lsemantics]EAbsurd_sem [lemma, in Fsemantics]
eApp [constructor, in typechecker]
EApp_sem [lemma, in Lsemantics]
EApp_sem [lemma, in Fsemantics]
EArr [definition, in Lsemantics]
EArr [definition, in Fsemantics]
EBot [definition, in Lsemantics]
EBot [definition, in Fsemantics]
eCoer [constructor, in typechecker]
ECoer_sem [lemma, in Lsemantics]
ECoer_sem [lemma, in Fsemantics]
EC1 [constructor, in typechecker]
EC2 [constructor, in typechecker]
Edistrib [lemma, in Lsemantics]
Edistrib [lemma, in Fsemantics]
EExi [definition, in Lsemantics]
EExi [definition, in Fsemantics]
EExi_preserve [definition, in Lsemantics]
EExi_preserve [definition, in Fsemantics]
EFor [definition, in Lsemantics]
EFor [definition, in Fsemantics]
EFor_preserve [definition, in Lsemantics]
EFor_preserve [definition, in Fsemantics]
eFst [constructor, in typechecker]
EFst_sem [lemma, in Lsemantics]
EFst_sem [lemma, in Fsemantics]
EG [constructor, in typechecker]
eGen [constructor, in typechecker]
EGen_sem [lemma, in Lsemantics]
EGen_sem [lemma, in Fsemantics]
EH [constructor, in typechecker]
eInl [constructor, in typechecker]
EInl_sem [lemma, in Lsemantics]
EInl_sem [lemma, in Fsemantics]
eInr [constructor, in typechecker]
EInr_sem [lemma, in Lsemantics]
EInr_sem [lemma, in Fsemantics]
eInst [constructor, in typechecker]
EInst_sem [lemma, in Lsemantics]
EInst_sem [lemma, in Fsemantics]
EJudg [definition, in Lsemantics]
EJudg [definition, in Fsemantics]
EJudg_Var [lemma, in Lsemantics]
EJudg_Var [lemma, in Fsemantics]
EK [constructor, in typechecker]
eLam [constructor, in typechecker]
ELam_sem [lemma, in Lsemantics]
ELam_sem [lemma, in Fsemantics]
eMatch [constructor, in typechecker]
EMatch_sem [lemma, in Lsemantics]
EMatch_sem [lemma, in Fsemantics]
Empty [constructor, in typechecker]
EMu [definition, in Fsemantics]
eobj [inductive, in typechecker]
EOne [definition, in Lsemantics]
EOne [definition, in Fsemantics]
EP [constructor, in typechecker]
ePair [constructor, in typechecker]
EPair_sem [lemma, in Lsemantics]
EPair_sem [lemma, in Fsemantics]
EPi [definition, in Lsemantics]
EPi [definition, in Fsemantics]
EProd [definition, in Lsemantics]
EProd [definition, in Fsemantics]
Eq [definition, in set]
EQcongrGCons [constructor, in typesystem]
EQcongrHCons [constructor, in typesystem]
EQcongrKProd [constructor, in typesystem]
EQcongrKRes [constructor, in typesystem]
EQcongrPAnd [constructor, in typesystem]
EQcongrPCoer [constructor, in typesystem]
EQcongrPExi [constructor, in typesystem]
EQcongrPFor [constructor, in typesystem]
EQcongrTArr [constructor, in typesystem]
EQcongrTFor [constructor, in typesystem]
EQcongrTFst [constructor, in typesystem]
EQcongrTMu [constructor, in typesystem]
EQcongrTPair [constructor, in typesystem]
EQcongrTPi [constructor, in typesystem]
EQcongrTProd [constructor, in typesystem]
EQcongrTSnd [constructor, in typesystem]
EQcongrTSum [constructor, in typesystem]
EQcongrYCons [constructor, in typesystem]
EQrefl [constructor, in typesystem]
EQsym [constructor, in typesystem]
EQTFstPair [constructor, in typesystem]
EQtrans [constructor, in typesystem]
EQTSndPair [constructor, in typesystem]
Err [inductive, in Llanguage]
Err [inductive, in Flanguage]
Err [constructor, in typechecker]
ErrAbsurd [constructor, in Llanguage]
ErrAbsurd [constructor, in Flanguage]
ErrApp [constructor, in Llanguage]
ErrApp [constructor, in Flanguage]
ErrCtx [constructor, in Llanguage]
ErrCtx [constructor, in Flanguage]
ErrFst [constructor, in Llanguage]
ErrFst [constructor, in Flanguage]
ErrInst [constructor, in Llanguage]
ErrInst [constructor, in Flanguage]
ErrMatch [constructor, in Llanguage]
ErrMatch [constructor, in Flanguage]
ErrSnd [constructor, in Llanguage]
ErrSnd [constructor, in Flanguage]
Err_drop [lemma, in Llanguage]
eSnd [constructor, in typechecker]
ESnd_sem [lemma, in Lsemantics]
ESnd_sem [lemma, in Fsemantics]
ESum [definition, in Lsemantics]
ESum [definition, in Fsemantics]
ET [constructor, in typechecker]
eterm [inductive, in typechecker]
ETop [definition, in Lsemantics]
ETop [definition, in Fsemantics]
EUnit_sem [lemma, in Lsemantics]
EUnit_sem [lemma, in Fsemantics]
eVar [constructor, in typechecker]
EVar_sem [lemma, in Lsemantics]
EVar_sem [lemma, in Fsemantics]
EVoid [definition, in Lsemantics]
EVoid [definition, in Fsemantics]
EVoid_EBot [lemma, in Fsemantics]
Ewf [constructor, in typechecker]
exists_extensionality [lemma, in ext]
exn [inductive, in typechecker]
Exp [definition, in Lsemantics]
Exp [definition, in Fsemantics]
ExpectedGotClass [constructor, in typechecker]
ExpectedGotJudg [constructor, in typechecker]
ExpectedGotJwf [constructor, in typechecker]
ExpectedGotObj [constructor, in typechecker]
ExpectedJEnv [constructor, in typechecker]
ExpFix [definition, in Fsemantics]
ExpSN [lemma, in Llanguage]
ext [library]
extEq [lemma, in set]
extrajudg [definition, in typesystemextra]
ext_v [inductive, in ext]
F
F [module, in Llanguage]fill [definition, in Llanguage]
fill [definition, in Flanguage]
Fix [definition, in Fnormalization]
Flanguage [library]
Flanguage_v [inductive, in Flanguage]
Fnormalization [library]
Fnormalization_v [inductive, in Fnormalization]
fold_Cl [lemma, in Lsemantics]
fold_Cl [lemma, in Fsemantics]
fold_OK [lemma, in Fsemantics]
For [definition, in Lsemantics]
For [definition, in Fsemantics]
forall_extensionality [lemma, in ext]
Forall_map_impl [lemma, in list]
Forall_map [lemma, in list]
Forall_app [lemma, in list]
Forall_nth [lemma, in list]
Fsemantics [library]
Fsemantics_v [inductive, in Fsemantics]
Fsoundness [library]
Fsoundness_v [inductive, in Fsoundness]
Fst [constructor, in Llanguage]
Fst [constructor, in Flanguage]
Ftypesystem [library]
Ftypesystem_v [inductive, in Ftypesystem]
G
gArr [constructor, in typechecker]gBot [constructor, in typechecker]
GCons [constructor, in typesystem]
Gen [constructor, in Llanguage]
Gen [constructor, in Flanguage]
getb [definition, in typechecker]
getstar [definition, in Lnormalization]
getstar [definition, in Fsoundness]
get_jrec [definition, in typesystemdec]
get_Gnth [definition, in typesystemdec]
get_Hnth [definition, in typesystemdec]
get_cobj [definition, in typesystemdec]
gFold [constructor, in typechecker]
gGen [constructor, in typechecker]
gInst [constructor, in typechecker]
GNil [constructor, in typesystem]
Gnth [inductive, in typesystem]
Gnth_extra [lemma, in typesystemextra]
Gnth_type [lemma, in Lnormalization]
Gnth_dec_Gnth [lemma, in typesystemdec]
Gnth_dec [definition, in typesystemdec]
Gnth_type [lemma, in Fsoundness]
Gnth0 [constructor, in typesystem]
Gnth1 [constructor, in typesystem]
Gnth2 [constructor, in typesystem]
GotTermType [constructor, in typechecker]
gPi [constructor, in typechecker]
gProd [constructor, in typechecker]
gProp [constructor, in typechecker]
gRefl [constructor, in typechecker]
gSum [constructor, in typechecker]
gTop [constructor, in typechecker]
gTrans [constructor, in typechecker]
gUnfold [constructor, in typechecker]
gWeak [constructor, in typechecker]
H
Happ [inductive, in typesystem]Happ_jobj [lemma, in typesystemextra]
Happ_Jwf_0 [lemma, in typesystemextra]
Happ_Jwf [lemma, in typesystemextra]
Happ_Hlength_lt [lemma, in typesystemextra]
Happ_Hlength_eq [lemma, in typesystemextra]
Happ_assoc_left [lemma, in typesystemextra]
Happ_assoc_right [lemma, in typesystemextra]
Happ_exists [lemma, in typesystemextra]
Happ_subst [lemma, in typesystemextra]
Happ_lift [lemma, in typesystemextra]
Happ_HCons_move [lemma, in typesystemextra]
Happ_HNil_eq [lemma, in typesystemextra]
Happ_HNil [lemma, in typesystemextra]
Happ_cobj_rev [lemma, in typesystemextra]
Happ_cobj [lemma, in typesystemextra]
Happ_fH_rev [lemma, in Lnormalization]
Happ_fH_nil [lemma, in Lnormalization]
Happ_fH [lemma, in Lnormalization]
Happ_semobj_rev2 [lemma, in Lnormalization]
Happ_semobj [lemma, in Lnormalization]
Happ_HNil [lemma, in Lnormalization]
Happ_fH_rev [lemma, in Fsoundness]
Happ_fH_nil [lemma, in Fsoundness]
Happ_fH [lemma, in Fsoundness]
Happ_semobj_rev2 [lemma, in Fsoundness]
Happ_semobj [lemma, in Fsoundness]
Happ_eq [lemma, in typesystem]
Happ0 [constructor, in typesystem]
Happ1 [constructor, in typesystem]
Hcheck [constructor, in typechecker]
HCons [constructor, in typesystem]
hCons [constructor, in typechecker]
Hlength [definition, in typesystem]
Hlength_Happ [lemma, in typesystemextra]
Hlength_subst [lemma, in typesystem]
Hlength_lift [lemma, in typesystem]
HNil [constructor, in typesystem]
hNil [constructor, in typechecker]
Hnth [inductive, in typesystem]
Hnth_extra [lemma, in typesystemextra]
Hnth_HCons_Hlength [lemma, in typesystemextra]
Hnth_Happ_subst [lemma, in typesystemextra]
Hnth_Happ_lift [lemma, in typesystemextra]
Hnth_lift [lemma, in typesystemextra]
Hnth_Hlength_exact [lemma, in typesystemextra]
Hnth_Hlength_KOne [lemma, in typesystemextra]
Hnth_cobj [lemma, in typesystemextra]
Hnth_mem [lemma, in Lnormalization]
Hnth_dec_Hnth [lemma, in typesystemdec]
Hnth_dec [definition, in typesystemdec]
Hnth_mem [lemma, in Fsoundness]
Hnth_eq [lemma, in typesystem]
Hnth0 [constructor, in typesystem]
Hnth1 [constructor, in typesystem]
Hnth2 [constructor, in typesystem]
hypjudg1 [definition, in typesystemextra]
hypjudg2 [definition, in typesystemextra]
I
Impossible [constructor, in typechecker]Inc [definition, in set]
Inc_approx [lemma, in Fsemantics]
Index [library]
Index_v [inductive, in Index]
ind_red [lemma, in Fnormalization]
Inl [constructor, in Llanguage]
Inl [constructor, in Flanguage]
Inr [constructor, in Llanguage]
Inr [constructor, in Flanguage]
insn [definition, in Lnormalization]
insn [definition, in Fsoundness]
Inst [constructor, in Llanguage]
Inst [constructor, in Flanguage]
Inter [definition, in set]
irred [definition, in Llanguage]
irred_value [lemma, in Llanguage]
is_free_sound [lemma, in typesystemdec]
is_free [definition, in typesystemdec]
iter [definition, in Fsemantics]
iter_le [lemma, in Fsemantics]
iter_dec [lemma, in Fsemantics]
J
JAbsurd [constructor, in Ftypesystem]JAbsurd [constructor, in Ltypesystem]
JApp [constructor, in Ftypesystem]
JApp [constructor, in Ltypesystem]
JC [constructor, in typesystem]
JCArr [constructor, in typesystem]
JCBot [constructor, in typesystem]
JCFold [constructor, in typesystem]
JCGen [constructor, in typesystem]
JCInst [constructor, in typesystem]
JCoer [constructor, in Ftypesystem]
JCoer [constructor, in Ltypesystem]
JCoer_aux [lemma, in typechecker]
JCPi [constructor, in typesystem]
JCProd [constructor, in typesystem]
JCProp [constructor, in typesystem]
JCProp_aux [lemma, in typechecker]
JCRefl [constructor, in typesystem]
JCSum [constructor, in typesystem]
JCTop [constructor, in typesystem]
JCTrans [constructor, in typesystem]
JCUnfold [constructor, in typesystem]
JCWeak [constructor, in typesystem]
jenv [inductive, in typechecker]
jeq [inductive, in typesystem]
jeq_KRes_rev [lemma, in typesystemextra]
jeq_KRes_rev_aux [lemma, in typesystemextra]
jeq_agree_KRes [definition, in typesystemextra]
jeq_KProd_rev [lemma, in typesystemextra]
jeq_KProd_rev_aux [lemma, in typesystemextra]
jeq_agree_KProd [definition, in typesystemextra]
jeq_KOne_rev [lemma, in typesystemextra]
jeq_KOne_rev_aux [lemma, in typesystemextra]
jeq_KStar_rev [lemma, in typesystemextra]
jeq_KStar_rev_aux [lemma, in typesystemextra]
jeq_class [lemma, in typesystemextra]
jeq_subst [lemma, in typesystemextra]
jeq_lift [lemma, in typesystemextra]
jeq_Hlength [lemma, in typesystemextra]
jeq_sound [lemma, in Lnormalization]
jeq_sound [lemma, in Fsoundness]
JFst [constructor, in Ftypesystem]
JFst [constructor, in Ltypesystem]
JG [constructor, in typesystem]
JGCons [constructor, in typesystem]
JGen [constructor, in Ftypesystem]
JGen [constructor, in Ltypesystem]
JGNil [constructor, in typesystem]
JH [constructor, in typesystem]
JHCons [constructor, in typesystem]
JHNil [constructor, in typesystem]
JH_extra [lemma, in typesystemextra]
JInl [constructor, in Ftypesystem]
JInl [constructor, in Ltypesystem]
JInr [constructor, in Ftypesystem]
JInr [constructor, in Ltypesystem]
JInst [constructor, in Ftypesystem]
JInst [constructor, in Ltypesystem]
JK [constructor, in typesystem]
JKexi [constructor, in typesystem]
JLam [constructor, in Ftypesystem]
JLam [constructor, in Ltypesystem]
jlift [definition, in typesystem]
jlift_subst2_0 [lemma, in typesystem]
jlift_subst2 [lemma, in typesystem]
jlift_fusion [lemma, in typesystem]
jlift_lift_0 [lemma, in typesystem]
jlift_lift [lemma, in typesystem]
jlift_0 [lemma, in typesystem]
JMatch [constructor, in Ftypesystem]
JMatch [constructor, in Ltypesystem]
jobj [inductive, in typesystem]
jobj_PF [lemma, in typesystemextra]
jobj_FP [lemma, in typesystemextra]
jobj_FS [lemma, in typesystemextra]
jobj_extra [lemma, in typesystemextra]
jobj_TPi_inversion [lemma, in typesystemextra]
jobj_TPi_inversion_ctx [lemma, in typesystemextra]
jobj_TMu_inversion [lemma, in typesystemextra]
jobj_TMu_inversion_ctx [lemma, in typesystemextra]
jobj_TFor_inversion [lemma, in typesystemextra]
jobj_TFor_inversion_ctx [lemma, in typesystemextra]
jobj_TSum_inversion [lemma, in typesystemextra]
jobj_TSum_inversion_ctx [lemma, in typesystemextra]
jobj_TProd_inversion [lemma, in typesystemextra]
jobj_TProd_inversion_ctx [lemma, in typesystemextra]
jobj_TArr_inversion [lemma, in typesystemextra]
jobj_TArr_inversion_ctx [lemma, in typesystemextra]
jobj_subst_0 [lemma, in typesystemextra]
jobj_subst [lemma, in typesystemextra]
jobj_subst_aux1 [lemma, in typesystemextra]
jobj_shift_0 [lemma, in typesystemextra]
jobj_lift_0 [lemma, in typesystemextra]
jobj_lift [lemma, in typesystemextra]
jobj_class [lemma, in typesystemextra]
jobj_sound [lemma, in Lnormalization]
jobj_sound [lemma, in Fsoundness]
JP [constructor, in typesystem]
JPair [constructor, in Ftypesystem]
JPair [constructor, in Ltypesystem]
JPAndFst [constructor, in typesystem]
JPAndPair [constructor, in typesystem]
JPAndSnd [constructor, in typesystem]
JPCoer [constructor, in typesystem]
JPCoer_aux [lemma, in typechecker]
JPeq [constructor, in typesystem]
JPExi [constructor, in typesystem]
JPFix [constructor, in typesystem]
JPForElim [constructor, in typesystem]
JPForIntro [constructor, in typesystem]
JPRes [constructor, in typesystem]
JPTrue [constructor, in typesystem]
JPVar [constructor, in typesystem]
jrec [inductive, in typesystem]
jrec_subst_0 [lemma, in typesystemextra]
jrec_subst [lemma, in typesystemextra]
jrec_lift_0 [lemma, in typesystemextra]
jrec_lift [lemma, in typesystemextra]
jrec_dec_jrec [lemma, in typesystemdec]
jrec_dec [definition, in typesystemdec]
jrec_sound [lemma, in Fsoundness]
JSnd [constructor, in Ftypesystem]
JSnd [constructor, in Ltypesystem]
jsubst [definition, in typesystem]
JT [constructor, in typesystem]
JTArr [constructor, in typesystem]
JTBot [constructor, in typesystem]
JTeq [constructor, in typesystem]
jterm [inductive, in Ftypesystem]
jterm [inductive, in Ltypesystem]
jterm_PF [lemma, in typesystemextra]
jterm_FP [lemma, in typesystemextra]
jterm_FS [lemma, in typesystemextra]
jterm_extra [lemma, in typesystemextra]
jterm_sound [lemma, in Lnormalization]
jterm_sound [lemma, in Fsoundness]
jterm_aux_rev [lemma, in Lsoundness]
jterm_aux [lemma, in Lsoundness]
JTFor [constructor, in typesystem]
JTFst [constructor, in typesystem]
JTMu [constructor, in typesystem]
JTOne [constructor, in typesystem]
JTPack [constructor, in typesystem]
JTPair [constructor, in typesystem]
JTPi [constructor, in typesystem]
JTProd [constructor, in typesystem]
JTSnd [constructor, in typesystem]
JTSum [constructor, in typesystem]
JTTop [constructor, in typesystem]
JTUnit [constructor, in typesystem]
JTUnpack [constructor, in typesystem]
JTVar [constructor, in typesystem]
JTVoid [constructor, in typesystem]
judg [inductive, in typesystem]
JUnit [constructor, in Ftypesystem]
JUnit [constructor, in Ltypesystem]
JVar [constructor, in Ftypesystem]
JVar [constructor, in Ltypesystem]
Jwf [constructor, in typesystem]
K
kexi [constructor, in typechecker]kfill [definition, in Llanguage]
kind [abbreviation, in typesystem]
KOne [constructor, in typesystem]
KProd [constructor, in typesystem]
KRes [constructor, in typesystem]
KRes_ctx_jeq [lemma, in typesystemextra]
KRes_ctx [inductive, in typesystemextra]
KRes0 [constructor, in typesystemextra]
KRes1 [constructor, in typesystemextra]
KStar [constructor, in typesystem]
L
Lam [constructor, in Llanguage]Lam [constructor, in Flanguage]
le_term_lt [lemma, in Flanguage]
le_term_le [lemma, in Flanguage]
le_term_red [lemma, in Flanguage]
le_term_subst [lemma, in Flanguage]
le_term_lower_trivial [lemma, in Flanguage]
le_term_lower [lemma, in Flanguage]
le_term [definition, in Flanguage]
le_max_l' [lemma, in minmax]
le_max_r' [lemma, in minmax]
le_min_l' [lemma, in minmax]
le_min_r' [lemma, in minmax]
lift [definition, in Llanguage]
lift [definition, in typesystem]
lift [definition, in Flanguage]
lift_subst [lemma, in Llanguage]
lift_lift [lemma, in Llanguage]
lift_0 [lemma, in Llanguage]
lift_idx [definition, in Llanguage]
lift_subst2_0 [lemma, in typesystem]
lift_subst2 [lemma, in typesystem]
lift_subst1_0 [lemma, in typesystem]
lift_subst1 [lemma, in typesystem]
lift_shift_0 [lemma, in typesystem]
lift_lift_0 [lemma, in typesystem]
lift_lift [lemma, in typesystem]
lift_fusion [lemma, in typesystem]
lift_0 [lemma, in typesystem]
lift_idx [definition, in typesystem]
lift_subst [lemma, in Flanguage]
lift_lift [lemma, in Flanguage]
lift_0 [lemma, in Flanguage]
lift_idx [definition, in Flanguage]
list [library]
list_v [inductive, in list]
Llanguage [library]
Llanguage_v [inductive, in Llanguage]
Lnormalization [library]
Lnormalization_v [inductive, in Lnormalization]
lower [definition, in Flanguage]
lower_subst [lemma, in Flanguage]
lower_lower [lemma, in Flanguage]
lower_lift [lemma, in Flanguage]
Lsemantics [library]
Lsemantics_v [inductive, in Lsemantics]
Lsoundness [library]
Lsoundness_v [inductive, in Lsoundness]
Ltypesystem [library]
Ltypesystem_v [inductive, in Ltypesystem]
lt_term_le [lemma, in Flanguage]
lt2 [definition, in Lnormalization]
lt2 [definition, in Fsoundness]
M
mapb0 [definition, in typechecker]mapb1 [definition, in typechecker]
mapb2 [definition, in typechecker]
mapb3 [definition, in typechecker]
mapb4 [definition, in typechecker]
map_fuel_lift [lemma, in Flanguage]
map_fuel [definition, in Flanguage]
Match [constructor, in Llanguage]
Match [constructor, in Flanguage]
mE [definition, in mxx]
measure [definition, in Fnormalization]
measure_lower [lemma, in Fnormalization]
message [inductive, in typechecker]
minmax [library]
minmax_v [inductive, in minmax]
Mode [definition, in mxx]
mR [definition, in mxx]
mS [definition, in mxx]
Mu [definition, in Fsemantics]
Mu_Mu' [lemma, in Fsemantics]
Mu_fold [lemma, in Fsemantics]
Mu_unfold [lemma, in Fsemantics]
Mu_approx_iter [lemma, in Fsemantics]
Mu' [definition, in Fsemantics]
mxx [library]
mxx_v [inductive, in mxx]
N
N [definition, in Llanguage]N [definition, in Flanguage]
NE [constructor, in typesystem]
NE [definition, in Fsemantics]
NE_id [lemma, in Fsemantics]
Nob [constructor, in typechecker]
NoRecTypes [constructor, in typechecker]
normalization [lemma, in Lnormalization]
normalization_aux [lemma, in Lnormalization]
NotArr [definition, in Llanguage]
NotArr [definition, in Flanguage]
NotArr_drop [lemma, in Llanguage]
NotArr_le_term [lemma, in Flanguage]
NotArr_subst [lemma, in Flanguage]
NotPi [definition, in Llanguage]
NotPi [definition, in Flanguage]
NotPi_drop [lemma, in Llanguage]
NotPi_le_term [lemma, in Flanguage]
NotPi_subst [lemma, in Flanguage]
NotProd [definition, in Llanguage]
NotProd [definition, in Flanguage]
NotProd_drop [lemma, in Llanguage]
NotProd_le_term [lemma, in Flanguage]
NotProd_subst [lemma, in Flanguage]
NotSum [definition, in Llanguage]
NotSum [definition, in Flanguage]
NotSum_drop [lemma, in Llanguage]
NotSum_le_term [lemma, in Flanguage]
NotSum_subst [lemma, in Flanguage]
NotWellFounded [constructor, in typechecker]
nth_insn2_minus [lemma, in Lnormalization]
nth_insn2 [lemma, in Lnormalization]
nth_insn2_nil [lemma, in Lnormalization]
nth_insneq [lemma, in Lnormalization]
nth_insn1 [lemma, in Lnormalization]
nth_deln1 [lemma, in Lnormalization]
nth_deln2 [lemma, in Lnormalization]
nth_insn2_minus [lemma, in Fsoundness]
nth_insn2 [lemma, in Fsoundness]
nth_insn2_nil [lemma, in Fsoundness]
nth_insneq [lemma, in Fsoundness]
nth_insn1 [lemma, in Fsoundness]
nth_deln1 [lemma, in Fsoundness]
nth_deln2 [lemma, in Fsoundness]
NV [definition, in Flanguage]
Nvalue_is_prevalue [lemma, in Llanguage]
NV_Var [lemma, in Flanguage]
N_drop [lemma, in Llanguage]
N_dec [lemma, in Llanguage]
N_dec [lemma, in Flanguage]
O
obj [inductive, in typesystem]Obj [constructor, in typechecker]
obj_dec [definition, in typesystemdec]
ocheck [constructor, in typechecker]
OK [definition, in Fsemantics]
OK [inductive, in Lsoundness]
OK [constructor, in typechecker]
OKOKstep [lemma, in Lsoundness]
OKstep [definition, in Lsoundness]
OKstepOK [lemma, in Lsoundness]
OKV [lemma, in Fsemantics]
OK_Gen [lemma, in Fsemantics]
OK_subst_Var [lemma, in Fsemantics]
OK_Inr [lemma, in Fsemantics]
OK_Inl [lemma, in Fsemantics]
OK_Pair [lemma, in Fsemantics]
OK_Lam [lemma, in Fsemantics]
OK_Unit [lemma, in Fsemantics]
OK_Var [lemma, in Fsemantics]
OK_def [lemma, in Fsemantics]
OK_ [constructor, in Lsoundness]
optb [inductive, in typechecker]
osig [inductive, in typechecker]
otc [definition, in typechecker]
otcj [definition, in typechecker]
P
Pair [constructor, in Llanguage]Pair [constructor, in Flanguage]
PAnd [constructor, in typesystem]
pApp [constructor, in typechecker]
PArr [definition, in Lsemantics]
PArr [definition, in Fsemantics]
PCoer [constructor, in typesystem]
pCoer [constructor, in typechecker]
Pdec [definition, in Fsemantics]
Pdec_EJudg [lemma, in Fsemantics]
Pdec_OK [lemma, in Fsemantics]
penv [abbreviation, in typesystem]
peq [constructor, in typechecker]
PExi [definition, in Lsemantics]
PExi [constructor, in typesystem]
PExi [definition, in Fsemantics]
pExi [constructor, in typechecker]
PExi_preserve [definition, in Lsemantics]
PExi_preserve [definition, in Fsemantics]
Pexp [definition, in Lsemantics]
Pexp [definition, in Fsemantics]
Pexp_EExi [lemma, in Lsemantics]
Pexp_EFor [lemma, in Lsemantics]
Pexp_Cl [lemma, in Lsemantics]
Pexp_SN [lemma, in Lsemantics]
Pexp_EExi [lemma, in Fsemantics]
Pexp_EFor [lemma, in Fsemantics]
Pexp_Cl [lemma, in Fsemantics]
Pexp_OK [lemma, in Fsemantics]
pFix [constructor, in typechecker]
PFor [constructor, in typesystem]
pFst [constructor, in typechecker]
pLam [constructor, in typechecker]
Pok [definition, in Fsemantics]
Pok_EJudg [lemma, in Fsemantics]
POne [definition, in Lsemantics]
POne [definition, in Fsemantics]
pPair [constructor, in typechecker]
PPi [definition, in Lsemantics]
PPi [definition, in Fsemantics]
PProd [definition, in Lsemantics]
PProd [definition, in Fsemantics]
Pred [definition, in Lsemantics]
Pred [definition, in Fsemantics]
Pred_EJudg [lemma, in Lsemantics]
Pred_SN [lemma, in Lsemantics]
Pred_EJudg [lemma, in Fsemantics]
Pred_OK [lemma, in Fsemantics]
pRes [constructor, in typechecker]
prevalue_is_value [lemma, in Llanguage]
progre [lemma, in Llanguage]
prop [abbreviation, in typesystem]
propositional_extensionality [axiom, in ext]
Psn [definition, in Lsemantics]
pSnd [constructor, in typechecker]
Psn_EJudg [lemma, in Lsemantics]
PSum [definition, in Lsemantics]
PSum [definition, in Fsemantics]
PTrue [constructor, in typesystem]
pTrue [constructor, in typechecker]
Push_right_Arr [lemma, in Fsemantics]
pVar [constructor, in typechecker]
PVoid [definition, in Lsemantics]
PVoid [definition, in Fsemantics]
R
RECArr [constructor, in typesystem]RECFor [constructor, in typesystem]
RECMu [constructor, in typesystem]
RECne [constructor, in typesystem]
RECPi [constructor, in typesystem]
RECProd [constructor, in typesystem]
recsort [inductive, in typesystem]
RECSum [constructor, in typesystem]
RECVar [constructor, in typesystem]
RECwf [constructor, in typesystem]
Red [definition, in Lsemantics]
red [inductive, in Llanguage]
Red [definition, in Fsemantics]
red [inductive, in Flanguage]
RedApp [constructor, in Llanguage]
RedApp [constructor, in Flanguage]
RedCN [lemma, in Lsemantics]
RedCN [lemma, in Fsemantics]
RedCtx [constructor, in Llanguage]
RedCtx [constructor, in Flanguage]
RedFst [constructor, in Llanguage]
RedFst [constructor, in Flanguage]
RedInl [constructor, in Llanguage]
RedInl [constructor, in Flanguage]
RedInr [constructor, in Llanguage]
RedInr [constructor, in Flanguage]
RedInst [constructor, in Llanguage]
RedInst [constructor, in Flanguage]
RedSnd [constructor, in Llanguage]
RedSnd [constructor, in Flanguage]
red_subst [lemma, in Llanguage]
red_drop [lemma, in Llanguage]
red_measure [lemma, in Fnormalization]
red_lower [lemma, in Flanguage]
red_subst [lemma, in Flanguage]
red_0 [lemma, in Flanguage]
replicate [lemma, in list]
R_Var [lemma, in Lsemantics]
R_lower [lemma, in Fsemantics]
R_Var [lemma, in Fsemantics]
S
SAEnv [constructor, in Lnormalization]SAEnv [constructor, in Fsoundness]
sem [inductive, in Lnormalization]
sem [inductive, in Fsoundness]
semclass [definition, in Lnormalization]
semclass [definition, in Fsoundness]
semenv [definition, in Lnormalization]
semenv [definition, in Fsoundness]
semGCons [constructor, in Lnormalization]
semGCons [constructor, in Fsoundness]
semGNil [constructor, in Lnormalization]
semGNil [constructor, in Fsoundness]
semHCons [constructor, in Lnormalization]
semHCons [constructor, in Fsoundness]
semHNil [constructor, in Lnormalization]
semHNil [constructor, in Fsoundness]
semjudg [definition, in Lnormalization]
semjudg [definition, in Fsoundness]
semKOne [constructor, in Lnormalization]
semKOne [constructor, in Fsoundness]
semKProd [constructor, in Lnormalization]
semKProd [constructor, in Fsoundness]
semKRes [constructor, in Lnormalization]
semKRes [constructor, in Fsoundness]
semKStar [constructor, in Lnormalization]
semKStar [constructor, in Fsoundness]
semobj [inductive, in Lnormalization]
semobj [inductive, in Fsoundness]
semobj_subst_rev [lemma, in Lnormalization]
semobj_subst [lemma, in Lnormalization]
semobj_lift_rev [lemma, in Lnormalization]
semobj_lift [lemma, in Lnormalization]
semobj_eq [lemma, in Lnormalization]
semobj_subst_rev [lemma, in Fsoundness]
semobj_subst [lemma, in Fsoundness]
semobj_lift_rev [lemma, in Fsoundness]
semobj_lift [lemma, in Fsoundness]
semobj_eq [lemma, in Fsoundness]
semPAnd [constructor, in Lnormalization]
semPAnd [constructor, in Fsoundness]
semPCoer [constructor, in Lnormalization]
semPCoer [constructor, in Fsoundness]
semPExi [constructor, in Lnormalization]
semPExi [constructor, in Fsoundness]
semPFor [constructor, in Lnormalization]
semPFor [constructor, in Fsoundness]
semPTrue [constructor, in Lnormalization]
semPTrue [constructor, in Fsoundness]
semTArr [constructor, in Lnormalization]
semTArr [constructor, in Fsoundness]
semTBot [constructor, in Lnormalization]
semTBot [constructor, in Fsoundness]
semTFor [constructor, in Lnormalization]
semTFor [constructor, in Fsoundness]
semTFst [constructor, in Lnormalization]
semTFst [constructor, in Fsoundness]
semTMu [constructor, in Lnormalization]
semTMu [constructor, in Fsoundness]
semTOne [constructor, in Lnormalization]
semTOne [constructor, in Fsoundness]
semTPair [constructor, in Lnormalization]
semTPair [constructor, in Fsoundness]
semTPi [constructor, in Lnormalization]
semTPi [constructor, in Fsoundness]
semTProd [constructor, in Lnormalization]
semTProd [constructor, in Fsoundness]
semTSnd [constructor, in Lnormalization]
semTSnd [constructor, in Fsoundness]
semTSum [constructor, in Lnormalization]
semTSum [constructor, in Fsoundness]
semTTop [constructor, in Lnormalization]
semTTop [constructor, in Fsoundness]
semTUnit [constructor, in Lnormalization]
semTUnit [constructor, in Fsoundness]
semTVar [constructor, in Lnormalization]
semTVar [constructor, in Fsoundness]
semTVoid [constructor, in Lnormalization]
semTVoid [constructor, in Fsoundness]
semYCons [constructor, in Lnormalization]
semYCons [constructor, in Fsoundness]
semYNil [constructor, in Lnormalization]
semYNil [constructor, in Fsoundness]
seq [definition, in Lnormalization]
seq [definition, in Fsoundness]
set [definition, in Llanguage]
set [definition, in set]
set [definition, in Flanguage]
set [library]
set_v [inductive, in set]
sfst [definition, in Lnormalization]
sfst [definition, in Fsoundness]
shift [definition, in Llanguage]
shift [definition, in typesystem]
shift [definition, in Flanguage]
SKind [constructor, in Lnormalization]
SKind [constructor, in Fsoundness]
skipn_app_length [lemma, in list]
skipn_overflow [lemma, in list]
slift [definition, in Lnormalization]
slift [definition, in Fsoundness]
SN [inductive, in Llanguage]
Snd [constructor, in Llanguage]
Snd [constructor, in Flanguage]
SN_Gen [lemma, in Lsemantics]
SN_subst_Var [lemma, in Lsemantics]
SN_Inr [lemma, in Lsemantics]
SN_Inl [lemma, in Lsemantics]
SN_Pair [lemma, in Lsemantics]
SN_Lam [lemma, in Lsemantics]
SN_Var [lemma, in Lsemantics]
SN_ [constructor, in Llanguage]
sobj [inductive, in Lnormalization]
sobj [inductive, in Fsoundness]
soundness [lemma, in Lsoundness]
soundness_aux [lemma, in Lsoundness]
SPair [constructor, in Lnormalization]
SPair [constructor, in Fsoundness]
SPEnv [constructor, in Lnormalization]
SPEnv [constructor, in Fsoundness]
split_Cl [lemma, in Fsemantics]
sprod [definition, in Lnormalization]
sprod [definition, in Fsoundness]
SProp [constructor, in Lnormalization]
SProp [constructor, in Fsoundness]
srec [definition, in Fsoundness]
srecsort [definition, in Fsoundness]
SSet [constructor, in Lnormalization]
SSet [constructor, in Fsoundness]
ssnd [definition, in Lnormalization]
ssnd [definition, in Fsoundness]
sstar [definition, in Lnormalization]
sstar [definition, in Fsoundness]
ssubst [definition, in Lnormalization]
ssubst [definition, in Fsoundness]
STEnv [constructor, in Lnormalization]
STEnv [constructor, in Fsoundness]
stenv_length [lemma, in Lnormalization]
stenv_length [lemma, in Fsoundness]
sterm [definition, in Lnormalization]
sterm [definition, in Fsoundness]
String [constructor, in typechecker]
SType [constructor, in Lnormalization]
SType [constructor, in Fsoundness]
Subst [definition, in Lsemantics]
subst [definition, in Llanguage]
subst [definition, in typesystem]
Subst [definition, in Fsemantics]
subst [definition, in Flanguage]
subst_subst_0_0 [lemma, in Llanguage]
subst_subst_0 [lemma, in Llanguage]
subst_subst [lemma, in Llanguage]
subst_lift_0 [lemma, in Llanguage]
subst_lift [lemma, in Llanguage]
subst_idx [definition, in Llanguage]
subst_subst_0_0 [lemma, in typesystem]
subst_subst_0 [lemma, in typesystem]
subst_subst [lemma, in typesystem]
subst_lift_0 [lemma, in typesystem]
subst_lift [lemma, in typesystem]
subst_idx [definition, in typesystem]
subst_lower [lemma, in Flanguage]
subst_subst_0_0 [lemma, in Flanguage]
subst_subst_0 [lemma, in Flanguage]
subst_subst [lemma, in Flanguage]
subst_lift_0 [lemma, in Flanguage]
subst_lift [lemma, in Flanguage]
subst_idx [definition, in Flanguage]
sunit [definition, in Lnormalization]
SUnit [constructor, in Lnormalization]
sunit [definition, in Fsoundness]
SUnit [constructor, in Fsoundness]
T
TArr [constructor, in typesystem]tArr [constructor, in typechecker]
TBot [constructor, in typesystem]
tBot [constructor, in typechecker]
tenv [abbreviation, in typesystem]
teq [constructor, in typechecker]
term [inductive, in Llanguage]
term [inductive, in Flanguage]
Term [constructor, in typechecker]
term_ge_kfill [lemma, in Llanguage]
term_lt_0 [lemma, in Flanguage]
term_lt_min [lemma, in Flanguage]
term_le_min [lemma, in Flanguage]
term_lt_exists [lemma, in Flanguage]
term_le_exists [lemma, in Flanguage]
term_le_max [lemma, in Flanguage]
term_le_lower [lemma, in Flanguage]
term_lt_red [lemma, in Flanguage]
term_le_red [lemma, in Flanguage]
term_ge_red [lemma, in Flanguage]
term_ge_subst [lemma, in Flanguage]
term_ge_lift [lemma, in Flanguage]
term_ge_lower [lemma, in Flanguage]
term_ge_dec [lemma, in Flanguage]
term_ge [definition, in Flanguage]
term_lt [definition, in Flanguage]
term_le [definition, in Flanguage]
term_ge_OK [lemma, in Lsoundness]
TFor [constructor, in typesystem]
tFor [constructor, in typechecker]
TFst [constructor, in typesystem]
tFst [constructor, in typechecker]
TMu [constructor, in typesystem]
tMu [constructor, in typechecker]
Todo [constructor, in typechecker]
TOne [constructor, in typesystem]
tPack [constructor, in typechecker]
TPair [constructor, in typesystem]
tPair [constructor, in typechecker]
TPi [constructor, in typesystem]
tPi [constructor, in typechecker]
TProd [constructor, in typesystem]
tProd [constructor, in typechecker]
traverse [definition, in Llanguage]
traverse [definition, in typesystem]
traverse [definition, in Flanguage]
TSnd [constructor, in typesystem]
tSnd [constructor, in typechecker]
TSum [constructor, in typesystem]
tSum [constructor, in typechecker]
TTop [constructor, in typesystem]
tTop [constructor, in typechecker]
TUnit [constructor, in typesystem]
tUnit [constructor, in typechecker]
tUnpack [constructor, in typechecker]
TVar [constructor, in typesystem]
tVar [constructor, in typechecker]
TVoid [constructor, in typesystem]
type [abbreviation, in typesystem]
typechecker [library]
typechecker_v [inductive, in typechecker]
typesystem [library]
typesystemdec [library]
typesystemdec_v [inductive, in typesystemdec]
typesystemextra [library]
typesystemextra_v [inductive, in typesystemextra]
typesystem_v [inductive, in typesystem]
U
unary_fuel_red [lemma, in Flanguage]unary_fuel_subst [lemma, in Flanguage]
unary_fuel_lift [lemma, in Flanguage]
unary_fuel_traverse [lemma, in Flanguage]
unary_fuel_map_trivial [lemma, in Flanguage]
unary_fuel_map [lemma, in Flanguage]
unary_fuel_2 [lemma, in Flanguage]
unary_fuel_1 [lemma, in Flanguage]
unary_fuel [definition, in Flanguage]
unfold_Cl [lemma, in Lsemantics]
unfold_Cl [lemma, in Fsemantics]
unfold_OK [lemma, in Fsemantics]
Union [definition, in set]
Unit [constructor, in Llanguage]
Unit [constructor, in Flanguage]
V
V [definition, in Llanguage]V [definition, in Flanguage]
value [definition, in Llanguage]
Var [constructor, in Llanguage]
Var [constructor, in Flanguage]
Version [inductive, in mxx]
vF [constructor, in mxx]
vP [constructor, in mxx]
vS [constructor, in mxx]
V_value [lemma, in Llanguage]
V_drop [lemma, in Llanguage]
V_subst_N [lemma, in Flanguage]
V_Inr [lemma, in Flanguage]
V_Inl [lemma, in Flanguage]
V_Pair [lemma, in Flanguage]
V_Lam [lemma, in Flanguage]
V_Unit [lemma, in Flanguage]
V_Var [lemma, in Flanguage]
W
WF [constructor, in typesystem]WF [definition, in Fsemantics]
WFj [definition, in Fsemantics]
WFj_Mu [lemma, in Fsemantics]
WFj_min [lemma, in Fsemantics]
WFj_EExi [lemma, in Fsemantics]
WFj_PExi [lemma, in Fsemantics]
WFj_EFor [lemma, in Fsemantics]
WFj_EPi [lemma, in Fsemantics]
WFj_ESum [lemma, in Fsemantics]
WFj_EProd [lemma, in Fsemantics]
WFj_EArr [lemma, in Fsemantics]
WFj_dec [lemma, in Fsemantics]
WFj_WF [lemma, in Fsemantics]
wf_der [lemma, in Fnormalization]
WF_EPi [lemma, in Fsemantics]
WF_PPi [lemma, in Fsemantics]
WF_ESum [lemma, in Fsemantics]
WF_PSum [lemma, in Fsemantics]
WF_EProd [lemma, in Fsemantics]
WF_PProd [lemma, in Fsemantics]
WF_EArr [lemma, in Fsemantics]
WF_PArr [lemma, in Fsemantics]
WF_iter_lt [lemma, in Fsemantics]
WF_approx_le [lemma, in Fsemantics]
WF_swap [lemma, in Fsemantics]
WF_CST [lemma, in Fsemantics]
WHCons [constructor, in typesystem]
WHNil [constructor, in typesystem]
WKOne [constructor, in typesystem]
wKOne [constructor, in typechecker]
WKProd [constructor, in typesystem]
wKProd [constructor, in typechecker]
WKRes [constructor, in typesystem]
wKRes [constructor, in typechecker]
WKStar [constructor, in typesystem]
wKStar [constructor, in typechecker]
WPAnd [constructor, in typesystem]
wPAnd [constructor, in typechecker]
WPCoer [constructor, in typesystem]
wPCoer [constructor, in typechecker]
WPExi [constructor, in typesystem]
wPExi [constructor, in typechecker]
WPFor [constructor, in typesystem]
wPFor [constructor, in typechecker]
WPTrue [constructor, in typesystem]
wPTrue [constructor, in typechecker]
WYCons [constructor, in typesystem]
WYNil [constructor, in typesystem]
X
xS [definition, in typechecker]Y
Yapp [inductive, in typesystem]Yapp_Jwf [lemma, in typesystemextra]
Yapp_subst [lemma, in typesystemextra]
Yapp_lift [lemma, in typesystemextra]
Yapp_cobj_rev [lemma, in typesystemextra]
Yapp_cobj [lemma, in typesystemextra]
Yapp_semobj_rev [lemma, in Lnormalization]
Yapp_semobj_rev [lemma, in Fsoundness]
Yapp0 [constructor, in typesystem]
Yapp1 [constructor, in typesystem]
YCons [constructor, in typesystem]
Yesb [constructor, in typechecker]
YNil [constructor, in typesystem]
Ynth [inductive, in typesystem]
Ynth_extra [lemma, in typesystemextra]
Ynth_subst [lemma, in typesystemextra]
Ynth_lift [lemma, in typesystemextra]
Ynth_cobj [lemma, in typesystemextra]
Ynth_mem [lemma, in Fsoundness]
Ynth_prop [lemma, in Fsoundness]
Ynth0 [constructor, in typesystem]
Ynth1 [constructor, in typesystem]
Ynth2 [constructor, in typesystem]
other
_ >>= _ [notation, in typechecker]!0 _ [notation, in typechecker]
!1 _ _ [notation, in typechecker]
!2 _ _ _ [notation, in typechecker]
!3 _ _ _ _ [notation, in typechecker]
!4 _ _ _ _ _ [notation, in typechecker]
Notation Index
other
_ >>= _ [in typechecker]!0 _ [in typechecker]
!1 _ _ [in typechecker]
!2 _ _ _ [in typechecker]
!3 _ _ _ _ [in typechecker]
!4 _ _ _ _ _ [in typechecker]
Module Index
F
F [in Llanguage]Library Index
E
extF
FlanguageFnormalization
Fsemantics
Fsoundness
Ftypesystem
I
IndexL
listLlanguage
Lnormalization
Lsemantics
Lsoundness
Ltypesystem
M
minmaxmxx
S
setT
typecheckertypesystem
typesystemdec
typesystemextra
Lemma Index
A
and_extensionality [in ext]approx_eq [in Fsemantics]
approx_inc [in Fsemantics]
approx_swap [in Fsemantics]
approx_min [in Fsemantics]
approx_approx [in Fsemantics]
approx_fold [in Fsemantics]
approx_unfold [in Fsemantics]
approx0 [in Fsemantics]
approx0_eq [in Fsemantics]
app_insn2 [in Lnormalization]
app_deln2 [in Lnormalization]
app_deln_length [in Lnormalization]
app_insn2 [in Fsoundness]
app_deln2 [in Fsoundness]
app_deln_length [in Fsoundness]
arrow_extensionality [in ext]
B
binary_fuel_unary [in Flanguage]binary_fuel_lift [in Flanguage]
binary_fuel_refl [in Flanguage]
binary_fuel_trans [in Flanguage]
binary_fuel_map_trivial [in Flanguage]
binary_fuel_map [in Flanguage]
C
CE_EBot [in Lsemantics]CE_ETop [in Lsemantics]
CE_EExi [in Lsemantics]
CE_EPi [in Lsemantics]
CE_EFor [in Lsemantics]
CE_ESum [in Lsemantics]
CE_EVoid [in Lsemantics]
CE_EProd [in Lsemantics]
CE_EOne [in Lsemantics]
CE_EArr [in Lsemantics]
CE_Cl [in Lsemantics]
CE_SN [in Lsemantics]
CE_CPexp [in Lsemantics]
CE_EMu [in Fsemantics]
CE_EBot [in Fsemantics]
CE_ETop [in Fsemantics]
CE_EExi [in Fsemantics]
CE_EPi [in Fsemantics]
CE_EFor [in Fsemantics]
CE_ESum [in Fsemantics]
CE_EVoid [in Fsemantics]
CE_EProd [in Fsemantics]
CE_EOne [in Fsemantics]
CE_EArr [in Fsemantics]
CE_Cl [in Fsemantics]
CE_CPexp [in Fsemantics]
CF_iter_F [in Fsemantics]
Cl_For [in Lsemantics]
Cl_def [in Lsemantics]
Cl_approx_For [in Fsemantics]
Cl_approx_eq [in Fsemantics]
Cl_approx [in Fsemantics]
Cl_CE [in Fsemantics]
Cl_monotone [in Fsemantics]
Cl_def [in Fsemantics]
CNprevalue_is_absurd [in Llanguage]
CN_drop [in Llanguage]
CN_red [in Llanguage]
CN_N [in Llanguage]
CN_le_term [in Flanguage]
CN_red [in Flanguage]
CN_subst [in Flanguage]
CN_N [in Flanguage]
cobj_unsubst [in typesystemextra]
cobj_eq [in typesystemextra]
cobj_subst [in typesystemextra]
cobj_unlift [in typesystemextra]
cobj_lift [in typesystemextra]
cobj_sound [in Lnormalization]
cobj_dec_cobj [in typesystemdec]
cobj_sound [in Fsoundness]
CST_WF [in Fsemantics]
cut_length [in list]
Cv [in Fsemantics]
C_EJudg [in Lsemantics]
C_EBot [in Lsemantics]
C_ETop [in Lsemantics]
C_PExi [in Lsemantics]
C_PPi [in Lsemantics]
C_EFor [in Lsemantics]
C_PSum [in Lsemantics]
C_PVoid [in Lsemantics]
C_PProd [in Lsemantics]
C_POne [in Lsemantics]
C_PArr [in Lsemantics]
C_Cl [in Lsemantics]
C_SN [in Lsemantics]
C_CE [in Lsemantics]
C_EJudg [in Fsemantics]
C_approx [in Fsemantics]
C_EBot [in Fsemantics]
C_ETop [in Fsemantics]
C_PExi [in Fsemantics]
C_PPi [in Fsemantics]
C_EFor [in Fsemantics]
C_PSum [in Fsemantics]
C_PVoid [in Fsemantics]
C_PProd [in Fsemantics]
C_POne [in Fsemantics]
C_PArr [in Fsemantics]
C_Cl [in Fsemantics]
C_OK [in Fsemantics]
C_CE [in Fsemantics]
D
DecCN [in Fsemantics]DecN [in Fsemantics]
DecNV [in Fsemantics]
destruct_Cl_CN [in Lsemantics]
destruct_Cl_CN [in Fsemantics]
drop_red_exists [in Llanguage]
drop_fill [in Llanguage]
drop_kfill [in Llanguage]
drop_subst [in Llanguage]
drop_lift [in Llanguage]
drop_lower [in Llanguage]
E
EAbsurd_sem [in Lsemantics]EAbsurd_sem [in Fsemantics]
EApp_sem [in Lsemantics]
EApp_sem [in Fsemantics]
ECoer_sem [in Lsemantics]
ECoer_sem [in Fsemantics]
Edistrib [in Lsemantics]
Edistrib [in Fsemantics]
EFst_sem [in Lsemantics]
EFst_sem [in Fsemantics]
EGen_sem [in Lsemantics]
EGen_sem [in Fsemantics]
EInl_sem [in Lsemantics]
EInl_sem [in Fsemantics]
EInr_sem [in Lsemantics]
EInr_sem [in Fsemantics]
EInst_sem [in Lsemantics]
EInst_sem [in Fsemantics]
EJudg_Var [in Lsemantics]
EJudg_Var [in Fsemantics]
ELam_sem [in Lsemantics]
ELam_sem [in Fsemantics]
EMatch_sem [in Lsemantics]
EMatch_sem [in Fsemantics]
EPair_sem [in Lsemantics]
EPair_sem [in Fsemantics]
Err_drop [in Llanguage]
ESnd_sem [in Lsemantics]
ESnd_sem [in Fsemantics]
EUnit_sem [in Lsemantics]
EUnit_sem [in Fsemantics]
EVar_sem [in Lsemantics]
EVar_sem [in Fsemantics]
EVoid_EBot [in Fsemantics]
exists_extensionality [in ext]
ExpSN [in Llanguage]
extEq [in set]
F
fold_Cl [in Lsemantics]fold_Cl [in Fsemantics]
fold_OK [in Fsemantics]
forall_extensionality [in ext]
Forall_map_impl [in list]
Forall_map [in list]
Forall_app [in list]
Forall_nth [in list]
G
Gnth_extra [in typesystemextra]Gnth_type [in Lnormalization]
Gnth_dec_Gnth [in typesystemdec]
Gnth_type [in Fsoundness]
H
Happ_jobj [in typesystemextra]Happ_Jwf_0 [in typesystemextra]
Happ_Jwf [in typesystemextra]
Happ_Hlength_lt [in typesystemextra]
Happ_Hlength_eq [in typesystemextra]
Happ_assoc_left [in typesystemextra]
Happ_assoc_right [in typesystemextra]
Happ_exists [in typesystemextra]
Happ_subst [in typesystemextra]
Happ_lift [in typesystemextra]
Happ_HCons_move [in typesystemextra]
Happ_HNil_eq [in typesystemextra]
Happ_HNil [in typesystemextra]
Happ_cobj_rev [in typesystemextra]
Happ_cobj [in typesystemextra]
Happ_fH_rev [in Lnormalization]
Happ_fH_nil [in Lnormalization]
Happ_fH [in Lnormalization]
Happ_semobj_rev2 [in Lnormalization]
Happ_semobj [in Lnormalization]
Happ_HNil [in Lnormalization]
Happ_fH_rev [in Fsoundness]
Happ_fH_nil [in Fsoundness]
Happ_fH [in Fsoundness]
Happ_semobj_rev2 [in Fsoundness]
Happ_semobj [in Fsoundness]
Happ_eq [in typesystem]
Hlength_Happ [in typesystemextra]
Hlength_subst [in typesystem]
Hlength_lift [in typesystem]
Hnth_extra [in typesystemextra]
Hnth_HCons_Hlength [in typesystemextra]
Hnth_Happ_subst [in typesystemextra]
Hnth_Happ_lift [in typesystemextra]
Hnth_lift [in typesystemextra]
Hnth_Hlength_exact [in typesystemextra]
Hnth_Hlength_KOne [in typesystemextra]
Hnth_cobj [in typesystemextra]
Hnth_mem [in Lnormalization]
Hnth_dec_Hnth [in typesystemdec]
Hnth_mem [in Fsoundness]
Hnth_eq [in typesystem]
I
Inc_approx [in Fsemantics]ind_red [in Fnormalization]
irred_value [in Llanguage]
is_free_sound [in typesystemdec]
iter_le [in Fsemantics]
iter_dec [in Fsemantics]
J
JCoer_aux [in typechecker]JCProp_aux [in typechecker]
jeq_KRes_rev [in typesystemextra]
jeq_KRes_rev_aux [in typesystemextra]
jeq_KProd_rev [in typesystemextra]
jeq_KProd_rev_aux [in typesystemextra]
jeq_KOne_rev [in typesystemextra]
jeq_KOne_rev_aux [in typesystemextra]
jeq_KStar_rev [in typesystemextra]
jeq_KStar_rev_aux [in typesystemextra]
jeq_class [in typesystemextra]
jeq_subst [in typesystemextra]
jeq_lift [in typesystemextra]
jeq_Hlength [in typesystemextra]
jeq_sound [in Lnormalization]
jeq_sound [in Fsoundness]
JH_extra [in typesystemextra]
jlift_subst2_0 [in typesystem]
jlift_subst2 [in typesystem]
jlift_fusion [in typesystem]
jlift_lift_0 [in typesystem]
jlift_lift [in typesystem]
jlift_0 [in typesystem]
jobj_PF [in typesystemextra]
jobj_FP [in typesystemextra]
jobj_FS [in typesystemextra]
jobj_extra [in typesystemextra]
jobj_TPi_inversion [in typesystemextra]
jobj_TPi_inversion_ctx [in typesystemextra]
jobj_TMu_inversion [in typesystemextra]
jobj_TMu_inversion_ctx [in typesystemextra]
jobj_TFor_inversion [in typesystemextra]
jobj_TFor_inversion_ctx [in typesystemextra]
jobj_TSum_inversion [in typesystemextra]
jobj_TSum_inversion_ctx [in typesystemextra]
jobj_TProd_inversion [in typesystemextra]
jobj_TProd_inversion_ctx [in typesystemextra]
jobj_TArr_inversion [in typesystemextra]
jobj_TArr_inversion_ctx [in typesystemextra]
jobj_subst_0 [in typesystemextra]
jobj_subst [in typesystemextra]
jobj_subst_aux1 [in typesystemextra]
jobj_shift_0 [in typesystemextra]
jobj_lift_0 [in typesystemextra]
jobj_lift [in typesystemextra]
jobj_class [in typesystemextra]
jobj_sound [in Lnormalization]
jobj_sound [in Fsoundness]
JPCoer_aux [in typechecker]
jrec_subst_0 [in typesystemextra]
jrec_subst [in typesystemextra]
jrec_lift_0 [in typesystemextra]
jrec_lift [in typesystemextra]
jrec_dec_jrec [in typesystemdec]
jrec_sound [in Fsoundness]
jterm_PF [in typesystemextra]
jterm_FP [in typesystemextra]
jterm_FS [in typesystemextra]
jterm_extra [in typesystemextra]
jterm_sound [in Lnormalization]
jterm_sound [in Fsoundness]
jterm_aux_rev [in Lsoundness]
jterm_aux [in Lsoundness]
K
KRes_ctx_jeq [in typesystemextra]L
le_term_lt [in Flanguage]le_term_le [in Flanguage]
le_term_red [in Flanguage]
le_term_subst [in Flanguage]
le_term_lower_trivial [in Flanguage]
le_term_lower [in Flanguage]
le_max_l' [in minmax]
le_max_r' [in minmax]
le_min_l' [in minmax]
le_min_r' [in minmax]
lift_subst [in Llanguage]
lift_lift [in Llanguage]
lift_0 [in Llanguage]
lift_subst2_0 [in typesystem]
lift_subst2 [in typesystem]
lift_subst1_0 [in typesystem]
lift_subst1 [in typesystem]
lift_shift_0 [in typesystem]
lift_lift_0 [in typesystem]
lift_lift [in typesystem]
lift_fusion [in typesystem]
lift_0 [in typesystem]
lift_subst [in Flanguage]
lift_lift [in Flanguage]
lift_0 [in Flanguage]
lower_subst [in Flanguage]
lower_lower [in Flanguage]
lower_lift [in Flanguage]
lt_term_le [in Flanguage]
M
map_fuel_lift [in Flanguage]measure_lower [in Fnormalization]
Mu_Mu' [in Fsemantics]
Mu_fold [in Fsemantics]
Mu_unfold [in Fsemantics]
Mu_approx_iter [in Fsemantics]
N
NE_id [in Fsemantics]normalization [in Lnormalization]
normalization_aux [in Lnormalization]
NotArr_drop [in Llanguage]
NotArr_le_term [in Flanguage]
NotArr_subst [in Flanguage]
NotPi_drop [in Llanguage]
NotPi_le_term [in Flanguage]
NotPi_subst [in Flanguage]
NotProd_drop [in Llanguage]
NotProd_le_term [in Flanguage]
NotProd_subst [in Flanguage]
NotSum_drop [in Llanguage]
NotSum_le_term [in Flanguage]
NotSum_subst [in Flanguage]
nth_insn2_minus [in Lnormalization]
nth_insn2 [in Lnormalization]
nth_insn2_nil [in Lnormalization]
nth_insneq [in Lnormalization]
nth_insn1 [in Lnormalization]
nth_deln1 [in Lnormalization]
nth_deln2 [in Lnormalization]
nth_insn2_minus [in Fsoundness]
nth_insn2 [in Fsoundness]
nth_insn2_nil [in Fsoundness]
nth_insneq [in Fsoundness]
nth_insn1 [in Fsoundness]
nth_deln1 [in Fsoundness]
nth_deln2 [in Fsoundness]
Nvalue_is_prevalue [in Llanguage]
NV_Var [in Flanguage]
N_drop [in Llanguage]
N_dec [in Llanguage]
N_dec [in Flanguage]
O
OKOKstep [in Lsoundness]OKstepOK [in Lsoundness]
OKV [in Fsemantics]
OK_Gen [in Fsemantics]
OK_subst_Var [in Fsemantics]
OK_Inr [in Fsemantics]
OK_Inl [in Fsemantics]
OK_Pair [in Fsemantics]
OK_Lam [in Fsemantics]
OK_Unit [in Fsemantics]
OK_Var [in Fsemantics]
OK_def [in Fsemantics]
P
Pdec_EJudg [in Fsemantics]Pdec_OK [in Fsemantics]
Pexp_EExi [in Lsemantics]
Pexp_EFor [in Lsemantics]
Pexp_Cl [in Lsemantics]
Pexp_SN [in Lsemantics]
Pexp_EExi [in Fsemantics]
Pexp_EFor [in Fsemantics]
Pexp_Cl [in Fsemantics]
Pexp_OK [in Fsemantics]
Pok_EJudg [in Fsemantics]
Pred_EJudg [in Lsemantics]
Pred_SN [in Lsemantics]
Pred_EJudg [in Fsemantics]
Pred_OK [in Fsemantics]
prevalue_is_value [in Llanguage]
progre [in Llanguage]
Psn_EJudg [in Lsemantics]
Push_right_Arr [in Fsemantics]
R
RedCN [in Lsemantics]RedCN [in Fsemantics]
red_subst [in Llanguage]
red_drop [in Llanguage]
red_measure [in Fnormalization]
red_lower [in Flanguage]
red_subst [in Flanguage]
red_0 [in Flanguage]
replicate [in list]
R_Var [in Lsemantics]
R_lower [in Fsemantics]
R_Var [in Fsemantics]
S
semobj_subst_rev [in Lnormalization]semobj_subst [in Lnormalization]
semobj_lift_rev [in Lnormalization]
semobj_lift [in Lnormalization]
semobj_eq [in Lnormalization]
semobj_subst_rev [in Fsoundness]
semobj_subst [in Fsoundness]
semobj_lift_rev [in Fsoundness]
semobj_lift [in Fsoundness]
semobj_eq [in Fsoundness]
skipn_app_length [in list]
skipn_overflow [in list]
SN_Gen [in Lsemantics]
SN_subst_Var [in Lsemantics]
SN_Inr [in Lsemantics]
SN_Inl [in Lsemantics]
SN_Pair [in Lsemantics]
SN_Lam [in Lsemantics]
SN_Var [in Lsemantics]
soundness [in Lsoundness]
soundness_aux [in Lsoundness]
split_Cl [in Fsemantics]
stenv_length [in Lnormalization]
stenv_length [in Fsoundness]
subst_subst_0_0 [in Llanguage]
subst_subst_0 [in Llanguage]
subst_subst [in Llanguage]
subst_lift_0 [in Llanguage]
subst_lift [in Llanguage]
subst_subst_0_0 [in typesystem]
subst_subst_0 [in typesystem]
subst_subst [in typesystem]
subst_lift_0 [in typesystem]
subst_lift [in typesystem]
subst_lower [in Flanguage]
subst_subst_0_0 [in Flanguage]
subst_subst_0 [in Flanguage]
subst_subst [in Flanguage]
subst_lift_0 [in Flanguage]
subst_lift [in Flanguage]
T
term_ge_kfill [in Llanguage]term_lt_0 [in Flanguage]
term_lt_min [in Flanguage]
term_le_min [in Flanguage]
term_lt_exists [in Flanguage]
term_le_exists [in Flanguage]
term_le_max [in Flanguage]
term_le_lower [in Flanguage]
term_lt_red [in Flanguage]
term_le_red [in Flanguage]
term_ge_red [in Flanguage]
term_ge_subst [in Flanguage]
term_ge_lift [in Flanguage]
term_ge_lower [in Flanguage]
term_ge_dec [in Flanguage]
term_ge_OK [in Lsoundness]
U
unary_fuel_red [in Flanguage]unary_fuel_subst [in Flanguage]
unary_fuel_lift [in Flanguage]
unary_fuel_traverse [in Flanguage]
unary_fuel_map_trivial [in Flanguage]
unary_fuel_map [in Flanguage]
unary_fuel_2 [in Flanguage]
unary_fuel_1 [in Flanguage]
unfold_Cl [in Lsemantics]
unfold_Cl [in Fsemantics]
unfold_OK [in Fsemantics]
V
V_value [in Llanguage]V_drop [in Llanguage]
V_subst_N [in Flanguage]
V_Inr [in Flanguage]
V_Inl [in Flanguage]
V_Pair [in Flanguage]
V_Lam [in Flanguage]
V_Unit [in Flanguage]
V_Var [in Flanguage]
W
WFj_Mu [in Fsemantics]WFj_min [in Fsemantics]
WFj_EExi [in Fsemantics]
WFj_PExi [in Fsemantics]
WFj_EFor [in Fsemantics]
WFj_EPi [in Fsemantics]
WFj_ESum [in Fsemantics]
WFj_EProd [in Fsemantics]
WFj_EArr [in Fsemantics]
WFj_dec [in Fsemantics]
WFj_WF [in Fsemantics]
wf_der [in Fnormalization]
WF_EPi [in Fsemantics]
WF_PPi [in Fsemantics]
WF_ESum [in Fsemantics]
WF_PSum [in Fsemantics]
WF_EProd [in Fsemantics]
WF_PProd [in Fsemantics]
WF_EArr [in Fsemantics]
WF_PArr [in Fsemantics]
WF_iter_lt [in Fsemantics]
WF_approx_le [in Fsemantics]
WF_swap [in Fsemantics]
WF_CST [in Fsemantics]
Y
Yapp_Jwf [in typesystemextra]Yapp_subst [in typesystemextra]
Yapp_lift [in typesystemextra]
Yapp_cobj_rev [in typesystemextra]
Yapp_cobj [in typesystemextra]
Yapp_semobj_rev [in Lnormalization]
Yapp_semobj_rev [in Fsoundness]
Ynth_extra [in typesystemextra]
Ynth_subst [in typesystemextra]
Ynth_lift [in typesystemextra]
Ynth_cobj [in typesystemextra]
Ynth_mem [in Fsoundness]
Ynth_prop [in Fsoundness]
Constructor Index
A
Absurd [in Llanguage]Absurd [in Flanguage]
acheck [in typechecker]
Acheck [in typechecker]
AC2 [in typechecker]
AG [in typechecker]
AH [in typechecker]
AK [in typechecker]
AP [in typechecker]
App [in Llanguage]
App [in Flanguage]
AT [in typechecker]
Awf [in typechecker]
B
BadSyntax [in typechecker]C
CAEnv [in typesystem]CE_ [in Lsemantics]
CE_ [in Fsemantics]
CGCons [in typesystem]
CGNil [in typesystem]
CHCons [in typesystem]
CHNil [in typesystem]
CKind [in typesystem]
CKOne [in typesystem]
CKProd [in typesystem]
CKRes [in typesystem]
CKStar [in typesystem]
ClExp [in Lsemantics]
ClR [in Lsemantics]
CPAnd [in typesystem]
CPCoer [in typesystem]
CPEnv [in typesystem]
CPExi [in typesystem]
CPFor [in typesystem]
CProp [in typesystem]
CPTrue [in typesystem]
CTArr [in typesystem]
CTBot [in typesystem]
CTEnv [in typesystem]
CTFor [in typesystem]
CTFst [in typesystem]
CTMu [in typesystem]
CTOne [in typesystem]
CTPair [in typesystem]
CTPi [in typesystem]
CTProd [in typesystem]
CTSnd [in typesystem]
CTSum [in typesystem]
CTTop [in typesystem]
CTUnit [in typesystem]
CTVar [in typesystem]
CTVoid [in typesystem]
CtxAbsurd [in Llanguage]
CtxAbsurd [in Flanguage]
CtxApp1 [in Llanguage]
CtxApp1 [in Flanguage]
CtxApp2 [in Llanguage]
CtxApp2 [in Flanguage]
CtxFst [in Llanguage]
CtxFst [in Flanguage]
CtxInl [in Llanguage]
CtxInl [in Flanguage]
CtxInr [in Llanguage]
CtxInr [in Flanguage]
CtxInst [in Llanguage]
CtxInst [in Flanguage]
CtxLam [in Llanguage]
CtxLam [in Flanguage]
CtxMatch1 [in Llanguage]
CtxMatch1 [in Flanguage]
CtxMatch2 [in Llanguage]
CtxMatch2 [in Flanguage]
CtxMatch3 [in Llanguage]
CtxMatch3 [in Flanguage]
CtxPair1 [in Llanguage]
CtxPair1 [in Flanguage]
CtxPair2 [in Llanguage]
CtxPair2 [in Flanguage]
CtxSnd [in Llanguage]
CtxSnd [in Flanguage]
CType [in typesystem]
CYCons [in typesystem]
CYNil [in typesystem]
C_ [in Lsemantics]
C_ [in Fsemantics]
E
eApp [in typechecker]eCoer [in typechecker]
EC1 [in typechecker]
EC2 [in typechecker]
eFst [in typechecker]
EG [in typechecker]
eGen [in typechecker]
EH [in typechecker]
eInl [in typechecker]
eInr [in typechecker]
eInst [in typechecker]
EK [in typechecker]
eLam [in typechecker]
eMatch [in typechecker]
Empty [in typechecker]
EP [in typechecker]
ePair [in typechecker]
EQcongrGCons [in typesystem]
EQcongrHCons [in typesystem]
EQcongrKProd [in typesystem]
EQcongrKRes [in typesystem]
EQcongrPAnd [in typesystem]
EQcongrPCoer [in typesystem]
EQcongrPExi [in typesystem]
EQcongrPFor [in typesystem]
EQcongrTArr [in typesystem]
EQcongrTFor [in typesystem]
EQcongrTFst [in typesystem]
EQcongrTMu [in typesystem]
EQcongrTPair [in typesystem]
EQcongrTPi [in typesystem]
EQcongrTProd [in typesystem]
EQcongrTSnd [in typesystem]
EQcongrTSum [in typesystem]
EQcongrYCons [in typesystem]
EQrefl [in typesystem]
EQsym [in typesystem]
EQTFstPair [in typesystem]
EQtrans [in typesystem]
EQTSndPair [in typesystem]
Err [in typechecker]
ErrAbsurd [in Llanguage]
ErrAbsurd [in Flanguage]
ErrApp [in Llanguage]
ErrApp [in Flanguage]
ErrCtx [in Llanguage]
ErrCtx [in Flanguage]
ErrFst [in Llanguage]
ErrFst [in Flanguage]
ErrInst [in Llanguage]
ErrInst [in Flanguage]
ErrMatch [in Llanguage]
ErrMatch [in Flanguage]
ErrSnd [in Llanguage]
ErrSnd [in Flanguage]
eSnd [in typechecker]
ET [in typechecker]
eVar [in typechecker]
Ewf [in typechecker]
ExpectedGotClass [in typechecker]
ExpectedGotJudg [in typechecker]
ExpectedGotJwf [in typechecker]
ExpectedGotObj [in typechecker]
ExpectedJEnv [in typechecker]
F
Fst [in Llanguage]Fst [in Flanguage]
G
gArr [in typechecker]gBot [in typechecker]
GCons [in typesystem]
Gen [in Llanguage]
Gen [in Flanguage]
gFold [in typechecker]
gGen [in typechecker]
gInst [in typechecker]
GNil [in typesystem]
Gnth0 [in typesystem]
Gnth1 [in typesystem]
Gnth2 [in typesystem]
GotTermType [in typechecker]
gPi [in typechecker]
gProd [in typechecker]
gProp [in typechecker]
gRefl [in typechecker]
gSum [in typechecker]
gTop [in typechecker]
gTrans [in typechecker]
gUnfold [in typechecker]
gWeak [in typechecker]
H
Happ0 [in typesystem]Happ1 [in typesystem]
Hcheck [in typechecker]
HCons [in typesystem]
hCons [in typechecker]
HNil [in typesystem]
hNil [in typechecker]
Hnth0 [in typesystem]
Hnth1 [in typesystem]
Hnth2 [in typesystem]
I
Impossible [in typechecker]Inl [in Llanguage]
Inl [in Flanguage]
Inr [in Llanguage]
Inr [in Flanguage]
Inst [in Llanguage]
Inst [in Flanguage]
J
JAbsurd [in Ftypesystem]JAbsurd [in Ltypesystem]
JApp [in Ftypesystem]
JApp [in Ltypesystem]
JC [in typesystem]
JCArr [in typesystem]
JCBot [in typesystem]
JCFold [in typesystem]
JCGen [in typesystem]
JCInst [in typesystem]
JCoer [in Ftypesystem]
JCoer [in Ltypesystem]
JCPi [in typesystem]
JCProd [in typesystem]
JCProp [in typesystem]
JCRefl [in typesystem]
JCSum [in typesystem]
JCTop [in typesystem]
JCTrans [in typesystem]
JCUnfold [in typesystem]
JCWeak [in typesystem]
JFst [in Ftypesystem]
JFst [in Ltypesystem]
JG [in typesystem]
JGCons [in typesystem]
JGen [in Ftypesystem]
JGen [in Ltypesystem]
JGNil [in typesystem]
JH [in typesystem]
JHCons [in typesystem]
JHNil [in typesystem]
JInl [in Ftypesystem]
JInl [in Ltypesystem]
JInr [in Ftypesystem]
JInr [in Ltypesystem]
JInst [in Ftypesystem]
JInst [in Ltypesystem]
JK [in typesystem]
JKexi [in typesystem]
JLam [in Ftypesystem]
JLam [in Ltypesystem]
JMatch [in Ftypesystem]
JMatch [in Ltypesystem]
JP [in typesystem]
JPair [in Ftypesystem]
JPair [in Ltypesystem]
JPAndFst [in typesystem]
JPAndPair [in typesystem]
JPAndSnd [in typesystem]
JPCoer [in typesystem]
JPeq [in typesystem]
JPExi [in typesystem]
JPFix [in typesystem]
JPForElim [in typesystem]
JPForIntro [in typesystem]
JPRes [in typesystem]
JPTrue [in typesystem]
JPVar [in typesystem]
JSnd [in Ftypesystem]
JSnd [in Ltypesystem]
JT [in typesystem]
JTArr [in typesystem]
JTBot [in typesystem]
JTeq [in typesystem]
JTFor [in typesystem]
JTFst [in typesystem]
JTMu [in typesystem]
JTOne [in typesystem]
JTPack [in typesystem]
JTPair [in typesystem]
JTPi [in typesystem]
JTProd [in typesystem]
JTSnd [in typesystem]
JTSum [in typesystem]
JTTop [in typesystem]
JTUnit [in typesystem]
JTUnpack [in typesystem]
JTVar [in typesystem]
JTVoid [in typesystem]
JUnit [in Ftypesystem]
JUnit [in Ltypesystem]
JVar [in Ftypesystem]
JVar [in Ltypesystem]
Jwf [in typesystem]
K
kexi [in typechecker]KOne [in typesystem]
KProd [in typesystem]
KRes [in typesystem]
KRes0 [in typesystemextra]
KRes1 [in typesystemextra]
KStar [in typesystem]
L
Lam [in Llanguage]Lam [in Flanguage]
M
Match [in Llanguage]Match [in Flanguage]
N
NE [in typesystem]Nob [in typechecker]
NoRecTypes [in typechecker]
NotWellFounded [in typechecker]
O
Obj [in typechecker]ocheck [in typechecker]
OK [in typechecker]
OK_ [in Lsoundness]
P
Pair [in Llanguage]Pair [in Flanguage]
PAnd [in typesystem]
pApp [in typechecker]
PCoer [in typesystem]
pCoer [in typechecker]
peq [in typechecker]
PExi [in typesystem]
pExi [in typechecker]
pFix [in typechecker]
PFor [in typesystem]
pFst [in typechecker]
pLam [in typechecker]
pPair [in typechecker]
pRes [in typechecker]
pSnd [in typechecker]
PTrue [in typesystem]
pTrue [in typechecker]
pVar [in typechecker]
R
RECArr [in typesystem]RECFor [in typesystem]
RECMu [in typesystem]
RECne [in typesystem]
RECPi [in typesystem]
RECProd [in typesystem]
RECSum [in typesystem]
RECVar [in typesystem]
RECwf [in typesystem]
RedApp [in Llanguage]
RedApp [in Flanguage]
RedCtx [in Llanguage]
RedCtx [in Flanguage]
RedFst [in Llanguage]
RedFst [in Flanguage]
RedInl [in Llanguage]
RedInl [in Flanguage]
RedInr [in Llanguage]
RedInr [in Flanguage]
RedInst [in Llanguage]
RedInst [in Flanguage]
RedSnd [in Llanguage]
RedSnd [in Flanguage]
S
SAEnv [in Lnormalization]SAEnv [in Fsoundness]
semGCons [in Lnormalization]
semGCons [in Fsoundness]
semGNil [in Lnormalization]
semGNil [in Fsoundness]
semHCons [in Lnormalization]
semHCons [in Fsoundness]
semHNil [in Lnormalization]
semHNil [in Fsoundness]
semKOne [in Lnormalization]
semKOne [in Fsoundness]
semKProd [in Lnormalization]
semKProd [in Fsoundness]
semKRes [in Lnormalization]
semKRes [in Fsoundness]
semKStar [in Lnormalization]
semKStar [in Fsoundness]
semPAnd [in Lnormalization]
semPAnd [in Fsoundness]
semPCoer [in Lnormalization]
semPCoer [in Fsoundness]
semPExi [in Lnormalization]
semPExi [in Fsoundness]
semPFor [in Lnormalization]
semPFor [in Fsoundness]
semPTrue [in Lnormalization]
semPTrue [in Fsoundness]
semTArr [in Lnormalization]
semTArr [in Fsoundness]
semTBot [in Lnormalization]
semTBot [in Fsoundness]
semTFor [in Lnormalization]
semTFor [in Fsoundness]
semTFst [in Lnormalization]
semTFst [in Fsoundness]
semTMu [in Lnormalization]
semTMu [in Fsoundness]
semTOne [in Lnormalization]
semTOne [in Fsoundness]
semTPair [in Lnormalization]
semTPair [in Fsoundness]
semTPi [in Lnormalization]
semTPi [in Fsoundness]
semTProd [in Lnormalization]
semTProd [in Fsoundness]
semTSnd [in Lnormalization]
semTSnd [in Fsoundness]
semTSum [in Lnormalization]
semTSum [in Fsoundness]
semTTop [in Lnormalization]
semTTop [in Fsoundness]
semTUnit [in Lnormalization]
semTUnit [in Fsoundness]
semTVar [in Lnormalization]
semTVar [in Fsoundness]
semTVoid [in Lnormalization]
semTVoid [in Fsoundness]
semYCons [in Lnormalization]
semYCons [in Fsoundness]
semYNil [in Lnormalization]
semYNil [in Fsoundness]
SKind [in Lnormalization]
SKind [in Fsoundness]
Snd [in Llanguage]
Snd [in Flanguage]
SN_ [in Llanguage]
SPair [in Lnormalization]
SPair [in Fsoundness]
SPEnv [in Lnormalization]
SPEnv [in Fsoundness]
SProp [in Lnormalization]
SProp [in Fsoundness]
SSet [in Lnormalization]
SSet [in Fsoundness]
STEnv [in Lnormalization]
STEnv [in Fsoundness]
String [in typechecker]
SType [in Lnormalization]
SType [in Fsoundness]
SUnit [in Lnormalization]
SUnit [in Fsoundness]
T
TArr [in typesystem]tArr [in typechecker]
TBot [in typesystem]
tBot [in typechecker]
teq [in typechecker]
Term [in typechecker]
TFor [in typesystem]
tFor [in typechecker]
TFst [in typesystem]
tFst [in typechecker]
TMu [in typesystem]
tMu [in typechecker]
Todo [in typechecker]
TOne [in typesystem]
tPack [in typechecker]
TPair [in typesystem]
tPair [in typechecker]
TPi [in typesystem]
tPi [in typechecker]
TProd [in typesystem]
tProd [in typechecker]
TSnd [in typesystem]
tSnd [in typechecker]
TSum [in typesystem]
tSum [in typechecker]
TTop [in typesystem]
tTop [in typechecker]
TUnit [in typesystem]
tUnit [in typechecker]
tUnpack [in typechecker]
TVar [in typesystem]
tVar [in typechecker]
TVoid [in typesystem]
U
Unit [in Llanguage]Unit [in Flanguage]
V
Var [in Llanguage]Var [in Flanguage]
vF [in mxx]
vP [in mxx]
vS [in mxx]
W
WF [in typesystem]WHCons [in typesystem]
WHNil [in typesystem]
WKOne [in typesystem]
wKOne [in typechecker]
WKProd [in typesystem]
wKProd [in typechecker]
WKRes [in typesystem]
wKRes [in typechecker]
WKStar [in typesystem]
wKStar [in typechecker]
WPAnd [in typesystem]
wPAnd [in typechecker]
WPCoer [in typesystem]
wPCoer [in typechecker]
WPExi [in typesystem]
wPExi [in typechecker]
WPFor [in typesystem]
wPFor [in typechecker]
WPTrue [in typesystem]
wPTrue [in typechecker]
WYCons [in typesystem]
WYNil [in typesystem]
Y
Yapp0 [in typesystem]Yapp1 [in typesystem]
YCons [in typesystem]
Yesb [in typechecker]
YNil [in typesystem]
Ynth0 [in typesystem]
Ynth1 [in typesystem]
Ynth2 [in typesystem]
Axiom Index
P
propositional_extensionality [in ext]Inductive Index
A
agree [in typechecker]asig [in typechecker]
Asig [in typechecker]
C
Cl [in Lsemantics]class [in typesystem]
cobj [in typesystem]
Ctx [in Llanguage]
Ctx [in Flanguage]
E
eobj [in typechecker]Err [in Llanguage]
Err [in Flanguage]
eterm [in typechecker]
exn [in typechecker]
ext_v [in ext]
F
Flanguage_v [in Flanguage]Fnormalization_v [in Fnormalization]
Fsemantics_v [in Fsemantics]
Fsoundness_v [in Fsoundness]
Ftypesystem_v [in Ftypesystem]
G
Gnth [in typesystem]H
Happ [in typesystem]Hnth [in typesystem]
I
Index_v [in Index]J
jenv [in typechecker]jeq [in typesystem]
jobj [in typesystem]
jrec [in typesystem]
jterm [in Ftypesystem]
jterm [in Ltypesystem]
judg [in typesystem]
K
KRes_ctx [in typesystemextra]L
list_v [in list]Llanguage_v [in Llanguage]
Lnormalization_v [in Lnormalization]
Lsemantics_v [in Lsemantics]
Lsoundness_v [in Lsoundness]
Ltypesystem_v [in Ltypesystem]
M
message [in typechecker]minmax_v [in minmax]
mxx_v [in mxx]
O
obj [in typesystem]OK [in Lsoundness]
optb [in typechecker]
osig [in typechecker]
R
recsort [in typesystem]red [in Llanguage]
red [in Flanguage]
S
sem [in Lnormalization]sem [in Fsoundness]
semobj [in Lnormalization]
semobj [in Fsoundness]
set_v [in set]
SN [in Llanguage]
sobj [in Lnormalization]
sobj [in Fsoundness]
T
term [in Llanguage]term [in Flanguage]
typechecker_v [in typechecker]
typesystemdec_v [in typesystemdec]
typesystemextra_v [in typesystemextra]
typesystem_v [in typesystem]
V
Version [in mxx]Y
Yapp [in typesystem]Ynth [in typesystem]
Projection Index
C
Cdec [in Fsemantics]CEdec [in Fsemantics]
CEexp [in Lsemantics]
CEexp [in Fsemantics]
CEok [in Fsemantics]
CEred [in Lsemantics]
CEred [in Fsemantics]
CEsn [in Lsemantics]
Cok [in Fsemantics]
Cred [in Lsemantics]
Cred [in Fsemantics]
Csn [in Lsemantics]
Abbreviation Index
A
aenv [in typesystem]K
kind [in typesystem]P
penv [in typesystem]prop [in typesystem]
T
tenv [in typesystem]type [in typesystem]
Definition Index
A
approx [in Fsemantics]atc [in typechecker]
Atc [in typechecker]
atcj [in typechecker]
B
binary_fuel [in Flanguage]bind [in typechecker]
C
ccljudg1 [in typesystemextra]cdrop [in Llanguage]
CF [in Fsemantics]
Cl [in Fsemantics]
classjudg [in typesystemextra]
class_dec [in typesystemdec]
Cmp [in set]
CN [in Llanguage]
CN [in Flanguage]
cobj_dec [in typesystemdec]
CST [in Fsemantics]
D
Dec [in Fsemantics]DecV [in Fsemantics]
deln [in Lnormalization]
deln [in Fsoundness]
der [in Fnormalization]
do_cobj [in typechecker]
drop [in Llanguage]
E
EArr [in Lsemantics]EArr [in Fsemantics]
EBot [in Lsemantics]
EBot [in Fsemantics]
EExi [in Lsemantics]
EExi [in Fsemantics]
EExi_preserve [in Lsemantics]
EExi_preserve [in Fsemantics]
EFor [in Lsemantics]
EFor [in Fsemantics]
EFor_preserve [in Lsemantics]
EFor_preserve [in Fsemantics]
EJudg [in Lsemantics]
EJudg [in Fsemantics]
EMu [in Fsemantics]
EOne [in Lsemantics]
EOne [in Fsemantics]
EPi [in Lsemantics]
EPi [in Fsemantics]
EProd [in Lsemantics]
EProd [in Fsemantics]
Eq [in set]
ESum [in Lsemantics]
ESum [in Fsemantics]
ETop [in Lsemantics]
ETop [in Fsemantics]
EVoid [in Lsemantics]
EVoid [in Fsemantics]
Exp [in Lsemantics]
Exp [in Fsemantics]
ExpFix [in Fsemantics]
extrajudg [in typesystemextra]
F
fill [in Llanguage]fill [in Flanguage]
Fix [in Fnormalization]
For [in Lsemantics]
For [in Fsemantics]
G
getb [in typechecker]getstar [in Lnormalization]
getstar [in Fsoundness]
get_jrec [in typesystemdec]
get_Gnth [in typesystemdec]
get_Hnth [in typesystemdec]
get_cobj [in typesystemdec]
Gnth_dec [in typesystemdec]
H
Hlength [in typesystem]Hnth_dec [in typesystemdec]
hypjudg1 [in typesystemextra]
hypjudg2 [in typesystemextra]
I
Inc [in set]insn [in Lnormalization]
insn [in Fsoundness]
Inter [in set]
irred [in Llanguage]
is_free [in typesystemdec]
iter [in Fsemantics]
J
jeq_agree_KRes [in typesystemextra]jeq_agree_KProd [in typesystemextra]
jlift [in typesystem]
jrec_dec [in typesystemdec]
jsubst [in typesystem]
K
kfill [in Llanguage]L
le_term [in Flanguage]lift [in Llanguage]
lift [in typesystem]
lift [in Flanguage]
lift_idx [in Llanguage]
lift_idx [in typesystem]
lift_idx [in Flanguage]
lower [in Flanguage]
lt2 [in Lnormalization]
lt2 [in Fsoundness]
M
mapb0 [in typechecker]mapb1 [in typechecker]
mapb2 [in typechecker]
mapb3 [in typechecker]
mapb4 [in typechecker]
map_fuel [in Flanguage]
mE [in mxx]
measure [in Fnormalization]
Mode [in mxx]
mR [in mxx]
mS [in mxx]
Mu [in Fsemantics]
Mu' [in Fsemantics]
N
N [in Llanguage]N [in Flanguage]
NE [in Fsemantics]
NotArr [in Llanguage]
NotArr [in Flanguage]
NotPi [in Llanguage]
NotPi [in Flanguage]
NotProd [in Llanguage]
NotProd [in Flanguage]
NotSum [in Llanguage]
NotSum [in Flanguage]
NV [in Flanguage]
O
obj_dec [in typesystemdec]OK [in Fsemantics]
OKstep [in Lsoundness]
otc [in typechecker]
otcj [in typechecker]
P
PArr [in Lsemantics]PArr [in Fsemantics]
Pdec [in Fsemantics]
PExi [in Lsemantics]
PExi [in Fsemantics]
PExi_preserve [in Lsemantics]
PExi_preserve [in Fsemantics]
Pexp [in Lsemantics]
Pexp [in Fsemantics]
Pok [in Fsemantics]
POne [in Lsemantics]
POne [in Fsemantics]
PPi [in Lsemantics]
PPi [in Fsemantics]
PProd [in Lsemantics]
PProd [in Fsemantics]
Pred [in Lsemantics]
Pred [in Fsemantics]
Psn [in Lsemantics]
PSum [in Lsemantics]
PSum [in Fsemantics]
PVoid [in Lsemantics]
PVoid [in Fsemantics]
R
Red [in Lsemantics]Red [in Fsemantics]
S
semclass [in Lnormalization]semclass [in Fsoundness]
semenv [in Lnormalization]
semenv [in Fsoundness]
semjudg [in Lnormalization]
semjudg [in Fsoundness]
seq [in Lnormalization]
seq [in Fsoundness]
set [in Llanguage]
set [in set]
set [in Flanguage]
sfst [in Lnormalization]
sfst [in Fsoundness]
shift [in Llanguage]
shift [in typesystem]
shift [in Flanguage]
slift [in Lnormalization]
slift [in Fsoundness]
sprod [in Lnormalization]
sprod [in Fsoundness]
srec [in Fsoundness]
srecsort [in Fsoundness]
ssnd [in Lnormalization]
ssnd [in Fsoundness]
sstar [in Lnormalization]
sstar [in Fsoundness]
ssubst [in Lnormalization]
ssubst [in Fsoundness]
sterm [in Lnormalization]
sterm [in Fsoundness]
Subst [in Lsemantics]
subst [in Llanguage]
subst [in typesystem]
Subst [in Fsemantics]
subst [in Flanguage]
subst_idx [in Llanguage]
subst_idx [in typesystem]
subst_idx [in Flanguage]
sunit [in Lnormalization]
sunit [in Fsoundness]
T
term_ge [in Flanguage]term_lt [in Flanguage]
term_le [in Flanguage]
traverse [in Llanguage]
traverse [in typesystem]
traverse [in Flanguage]
U
unary_fuel [in Flanguage]Union [in set]
V
V [in Llanguage]V [in Flanguage]
value [in Llanguage]
W
WF [in Fsemantics]WFj [in Fsemantics]
X
xS [in typechecker]Record Index
C
C [in Lsemantics]C [in Fsemantics]
CE [in Lsemantics]
CE [in Fsemantics]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1309 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (503 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (487 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (64 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (205 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 entries) |
This page has been generated by coqdoc