| 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 | (819 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 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 | (450 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 | (143 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 | (21 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 | (19 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 | (5 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 | (157 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 | (6 entries) |
Global Index
A
and_extensionality [lemma, in ext]App [constructor, in Llanguage]
App [constructor, in Flanguage]
approx [definition, in Fsemantics]
approx_For [lemma, 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_sem [lemma, in Lsemantics]
Arr [definition, in Lsemantics]
Arr [constructor, in typesystem]
B
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]
Bot [definition, in Lsemantics]
Bot [constructor, in typesystem]
C
C [record, in Lsemantics]C [record, in Fsemantics]
CCcoer [constructor, in typesystemequiv]
CCcons [constructor, in typesystemequiv]
CCnil [constructor, in typesystemequiv]
CCpair [constructor, in typesystemequiv]
CCtype [constructor, in typesystemequiv]
Cdec [projection, in Fsemantics]
CE [record, in Lsemantics]
CE [record, in Fsemantics]
CEcoer [constructor, in typesystemequiv]
CEdec [projection, in Fsemantics]
CEexp [projection, in Lsemantics]
CEexp [projection, in Fsemantics]
CElist [constructor, in typesystemequiv]
CEok [projection, in Fsemantics]
CEprod [constructor, in typesystemequiv]
CEred [projection, in Lsemantics]
CEred [projection, in Fsemantics]
CEsn [projection, in Lsemantics]
CEtype [constructor, in typesystemequiv]
CE_Bot [lemma, in Lsemantics]
CE_Top [lemma, in Lsemantics]
CE_Exi [lemma, in Lsemantics]
CE_For [lemma, in Lsemantics]
CE_Prod [lemma, in Lsemantics]
CE_Arr [lemma, in Lsemantics]
CE_Cl [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_For [lemma, in Fsemantics]
CE_EProd [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]
Cl [inductive, in Lsemantics]
Cl [definition, in Fsemantics]
ClExp [constructor, in Lsemantics]
ClR [constructor, in Lsemantics]
Cl_Lc [lemma, in Lsemantics]
Cl_monotone [lemma, in Lsemantics]
Cl_def [lemma, in Lsemantics]
Cl_approx_For [lemma, in Fsemantics]
Cl_For [lemma, in Fsemantics]
Cl_approx_eq [lemma, in Fsemantics]
Cl_approx [lemma, in Fsemantics]
Cl_Lc [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]
CNvalue_is_prevalue [lemma, in Llanguage]
CN_N [lemma, in Llanguage]
CN_N [lemma, in Flanguage]
coer_coer_env_lift_app [lemma, in typesystemequiv]
coer_coer_env_app [lemma, in typesystemequiv]
coer_coer_env_lift [lemma, in typesystemequiv]
coer_coer_env_listcoer_subst [lemma, in typesystemequiv]
coer_coer_env_listcoer [lemma, in typesystemequiv]
coer_coer_env_listprodtype [lemma, in typesystemequiv]
coer_coer_env_listtype [lemma, in typesystemequiv]
coer_coer_env_type [lemma, in typesystemequiv]
coer_coer_env [inductive, in typesystemequiv]
coer_ext_env [inductive, in typesystemequiv]
coer_left_type_listcoer_subst [lemma, in typesystemequiv]
coer_left_type_listcoer [lemma, in typesystemequiv]
coer_left_type_listprodtype [lemma, in typesystemequiv]
coer_left_type_listtype [lemma, in typesystemequiv]
coer_left_type_type [lemma, in typesystemequiv]
coer_left_type [inductive, in typesystemequiv]
Coer_sem [lemma, in Lsemantics]
coer_env [definition, in typesystem]
Cok [projection, in Fsemantics]
CRcoer [constructor, in typesystemequiv]
CRcons [constructor, in typesystemequiv]
Cred [projection, in Lsemantics]
Cred [projection, in Fsemantics]
CRnil [constructor, in typesystemequiv]
CRpair [constructor, in typesystemequiv]
CRtype [constructor, in typesystemequiv]
Csn [projection, in Lsemantics]
CST [definition, in Fsemantics]
CST_WF [lemma, in Fsemantics]
CT [record, in Lsemantics]
CT [record, in Fsemantics]
CTcn [projection, in Lsemantics]
CTcn [projection, in Fsemantics]
CTdec [projection, in Fsemantics]
CTok [projection, in Fsemantics]
CTred [projection, in Lsemantics]
CTred [projection, in Fsemantics]
CTsn [projection, in Lsemantics]
CT_PExi [lemma, in Lsemantics]
CT_For [lemma, in Lsemantics]
CT_PProd [lemma, in Lsemantics]
CT_PArr [lemma, in Lsemantics]
CT_Lc [lemma, in Lsemantics]
CT_CPcn [lemma, in Lsemantics]
CT_ [constructor, in Lsemantics]
CT_TMu [lemma, in Fsemantics]
CT_approx [lemma, in Fsemantics]
CT_TBot [lemma, in Fsemantics]
CT_TTop [lemma, in Fsemantics]
CT_TExi [lemma, in Fsemantics]
CT_For [lemma, in Fsemantics]
CT_TProd [lemma, in Fsemantics]
CT_TArr [lemma, in Fsemantics]
CT_Lc [lemma, in Fsemantics]
CT_CPcn [lemma, in Fsemantics]
CT_ [constructor, in Fsemantics]
cut_length [lemma, in list]
Cv [lemma, in Fsemantics]
CVar_sound [lemma, in Fsoundness]
C_Judg [lemma, in Lsemantics]
C_Bot [lemma, in Lsemantics]
C_Top [lemma, in Lsemantics]
C_PExi [lemma, in Lsemantics]
C_For [lemma, in Lsemantics]
C_PProd [lemma, in Lsemantics]
C_PArr [lemma, in Lsemantics]
C_Cl [lemma, in Lsemantics]
C_CE [lemma, in Lsemantics]
C_CT [lemma, in Lsemantics]
C_ [constructor, in Lsemantics]
C_TJudg [lemma, in Fsemantics]
C_EJudg [lemma, in Fsemantics]
C_approx [lemma, in Fsemantics]
C_TBot [lemma, in Fsemantics]
C_EBot [lemma, in Fsemantics]
C_TTop [lemma, in Fsemantics]
C_ETop [lemma, in Fsemantics]
C_TExi [lemma, in Fsemantics]
C_For [lemma, in Fsemantics]
C_PProd [lemma, in Fsemantics]
C_PArr [lemma, in Fsemantics]
C_Cl [lemma, in Fsemantics]
C_CE [lemma, in Fsemantics]
C_CT [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]
der [definition, in Fnormalization]
destruct_Cl_N [lemma, in Lsemantics]
destruct_Cl_CN [lemma, in Lsemantics]
destruct_Cl_N [lemma, in Fsemantics]
destruct_Cl_CN [lemma, in Fsemantics]
distrib [lemma, in Lsemantics]
dmap [definition, in typesystem]
dmap_app [lemma, in typesystem]
dmap_subst_lift [lemma, in typesystem]
dmap_lift_subst2 [lemma, in typesystem]
dmap_lift_subst1 [lemma, in typesystem]
dmap_lift_lift [lemma, in typesystem]
dmap_lift_plus [lemma, in typesystem]
dmap_lift_fusion [lemma, in typesystem]
dmap_lift_0 [lemma, in typesystem]
drop [definition, in Llanguage]
drop_red_exists [lemma, in Llanguage]
drop_fill [lemma, in Llanguage]
drop_subst [lemma, in Llanguage]
drop_lift [lemma, in Llanguage]
drop_lessen [lemma, in Llanguage]
E
EApp_sem [lemma, in Fsemantics]EArr [definition, in Fsemantics]
EBot [definition, in Fsemantics]
Ecoer [constructor, in typesystem]
ECoer_sem [lemma, in Fsemantics]
Econs [constructor, in typesystem]
Edistrib [lemma, in Fsemantics]
EExi [definition, in Fsemantics]
EExi_preserve [definition, in Fsemantics]
EFst_sem [lemma, in Fsemantics]
EJudg [definition, in Fsemantics]
EJudg_Var [lemma, in Fsemantics]
ELam_sem [lemma, in Fsemantics]
elift [definition, in typesystem]
EMu [definition, in Fsemantics]
EMu_sub [lemma, in Fsemantics]
Enil [constructor, in typesystem]
Epair [constructor, in typesystem]
EPair_sem [lemma, in Fsemantics]
EProd [definition, in Fsemantics]
Eq [definition, in set]
Err [inductive, in Llanguage]
Err [inductive, in Flanguage]
ErrApp [constructor, in Llanguage]
ErrApp [constructor, in Flanguage]
ErrCtxApp1 [constructor, in Llanguage]
ErrCtxApp1 [constructor, in Flanguage]
ErrCtxApp2 [constructor, in Llanguage]
ErrCtxApp2 [constructor, in Flanguage]
ErrCtxFst [constructor, in Llanguage]
ErrCtxFst [constructor, in Flanguage]
ErrCtxLam [constructor, in Llanguage]
ErrCtxLam [constructor, in Flanguage]
ErrCtxPair1 [constructor, in Llanguage]
ErrCtxPair1 [constructor, in Flanguage]
ErrCtxPair2 [constructor, in Llanguage]
ErrCtxPair2 [constructor, in Flanguage]
ErrCtxSnd [constructor, in Llanguage]
ErrCtxSnd [constructor, in Flanguage]
ErrFst [constructor, in Llanguage]
ErrFst [constructor, in Flanguage]
ErrSnd [constructor, in Llanguage]
ErrSnd [constructor, in Flanguage]
Err_drop [lemma, in Llanguage]
ESnd_sem [lemma, in Fsemantics]
esubst [definition, in typesystem]
ETop [definition, in Fsemantics]
etraverse [definition, in typesystem]
Etype [constructor, in typesystem]
EVar_sem [lemma, in Fsemantics]
examples [library]
Exi [definition, in Lsemantics]
exists_extensionality [lemma, in ext]
Exi_preserve [definition, in Lsemantics]
Exp [definition, in Lsemantics]
Exp [definition, in Fsemantics]
ExpFix [definition, in Fsemantics]
ExpSN [lemma, in Llanguage]
ext [library]
extEq [lemma, in set]
extract [inductive, in typesystem]
extract_subst [lemma, in typesystem]
extract_lift [lemma, in typesystem]
extract_inject [lemma, in typesystem]
extract_inj [lemma, in typesystem]
extract_eq [lemma, in typesystem]
F
Fake [definition, in Fsoundness]fill [definition, in Llanguage]
Fix [definition, in Fnormalization]
Flanguage [library]
Fnormalization [library]
fold_Cl [lemma, in Lsemantics]
fold_Cl [lemma, in Fsemantics]
fold_OK [lemma, in Fsemantics]
For [definition, in Lsemantics]
For [constructor, in typesystem]
For [definition, in Fsemantics]
Forall_coer2sem_type [lemma, in Fsoundness]
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]
For_preserve [definition, in Lsemantics]
For_approx [lemma, in Fsemantics]
For_preserve [definition, in Fsemantics]
Fsemantics [library]
Fsoundness [library]
Fst [constructor, in Llanguage]
Fst [constructor, in Flanguage]
Fst_sem [lemma, in Lsemantics]
Ftypesystem [library]
I
Inc [definition, in set]Incf [definition, in typesystem]
Incf_nil [lemma, in typesystem]
Incf_refl [lemma, in typesystem]
Incf_app [lemma, in typesystem]
Incf_lift [lemma, in typesystem]
Inc_approx [lemma, in Fsemantics]
ind_red [lemma, in Fnormalization]
inject [definition, in typesystem]
inject_extract [lemma, in typesystem]
inj_list [definition, in typesystem]
Inter [definition, in set]
irred [definition, in Llanguage]
irred_value [lemma, in Llanguage]
iter [definition, in Fsemantics]
iter_le [lemma, in Fsemantics]
iter_dec [lemma, in Fsemantics]
iter_preserve [lemma, in Fsemantics]
J
JApp [constructor, in Ftypesystem]JApp [constructor, in Ltypesystem]
JCArr [constructor, in typesystem]
JCBot [constructor, in typesystem]
JCFix [constructor, in typesystem]
JCFold [constructor, in typesystem]
JCGen [constructor, in typesystem]
JCInst [constructor, in typesystem]
JCoer [constructor, in Ftypesystem]
JCoer [constructor, in Ltypesystem]
jcoer [definition, in typesystem]
jcoer_sound [lemma, in Fsoundness]
jcoer_rebuild_jterm_env [lemma, in typesystemequiv]
jcoer_env_jerasable_Z [lemma, in typesystemequiv]
jcoer_env_lift [lemma, in typesystemequiv]
jcoer_env [definition, in typesystemequiv]
jcoer_extract_left_type [lemma, in typesystem]
jcoer_extract_right_type [lemma, in typesystem]
jcoer_extract_jerasable_env [lemma, in typesystem]
jcoer_weak_coerY_0 [lemma, in typesystem]
jcoer_weak_coerY [lemma, in typesystem]
JCProd [constructor, in typesystem]
JCRefl [constructor, in typesystem]
JCTop [constructor, in typesystem]
JCTrans [constructor, in typesystem]
JCUnfold [constructor, in typesystem]
JCVar [constructor, in typesystem]
JCWeak [constructor, in typesystem]
JEcons [constructor, in typesystem]
JEnil [constructor, in typesystem]
jerasable [inductive, in typesystem]
jerasable_env_sound [lemma, in Fsoundness]
jerasable_sound [lemma, in Fsoundness]
jerasable_env_up_1 [lemma, in typesystemequiv]
jerasable_bind_up_1 [lemma, in typesystemequiv]
jerasable_up_1 [lemma, in typesystemequiv]
jerasable_env_jerasable_Z [lemma, in typesystemequiv]
jerasable_env_bind [lemma, in typesystemequiv]
jerasable_env_lift [lemma, in typesystemequiv]
jerasable_bind_lift [lemma, in typesystemequiv]
jerasable_bind_only_type [lemma, in typesystemequiv]
jerasable_list_app [lemma, in typesystemequiv]
jerasable_env_up_2 [lemma, in typesystemequiv]
jerasable_bind_up_2 [lemma, in typesystemequiv]
jerasable_up_2 [lemma, in typesystemequiv]
jerasable_env_down [lemma, in typesystemequiv]
jerasable_bind_down [lemma, in typesystemequiv]
jerasable_down [lemma, in typesystemequiv]
jerasable_subst_0 [lemma, in typesystem]
jerasable_subst [lemma, in typesystem]
jerasable_nth_subst [lemma, in typesystem]
jerasable_nth [lemma, in typesystem]
jerasable_lift_0 [lemma, in typesystem]
jerasable_lift [lemma, in typesystem]
jerasable_weak_coer_0 [lemma, in typesystem]
jerasable_weak_coer [lemma, in typesystem]
jerasable_env [inductive, in typesystem]
jerasable_bind [definition, in typesystem]
JFst [constructor, in Ftypesystem]
JFst [constructor, in Ltypesystem]
JLam [constructor, in Ftypesystem]
JLam [constructor, in Ltypesystem]
JPair [constructor, in Ftypesystem]
JPair [constructor, in Ltypesystem]
JSCons [constructor, in typesystem]
JSnd [constructor, in Ftypesystem]
JSnd [constructor, in Ltypesystem]
JSNil [constructor, in typesystem]
JSPair [constructor, in typesystem]
JTArr [constructor, in typesystem]
JTBot [constructor, in typesystem]
jterm [inductive, in Ftypesystem]
jterm [inductive, in Ltypesystem]
jterm_extract_jtype [lemma, in Ftypesystem]
jterm_extract_jterm_env [lemma, in Ftypesystem]
jterm_sound [lemma, in Fsoundness]
jterm_env_sound [lemma, in Fsoundness]
jterm_up_1 [lemma, in typesystemequiv]
jterm_env_up_1 [lemma, in typesystemequiv]
jterm_up_2 [lemma, in typesystemequiv]
jterm_env_up_2 [lemma, in typesystemequiv]
jterm_down [lemma, in typesystemequiv]
jterm_env_down [lemma, in typesystemequiv]
jterm_extract_jtype [lemma, in Ltypesystem]
jterm_extract_jterm_env [lemma, in Ltypesystem]
jterm_env_extract_jerasable_env [lemma, in typesystem]
jterm_env [definition, in typesystem]
jterm_sound [lemma, in Lsoundness]
jterm_aux_rev [lemma, in Lsoundness]
jterm_aux [lemma, in Lsoundness]
jterm_2_delta [lemma, in examples]
jterm_0_delta [lemma, in examples]
jterm_2_id [lemma, in examples]
jterm_env_1 [lemma, in examples]
jterm_0_id [lemma, in examples]
JTFor [constructor, in typesystem]
JTMu [constructor, in typesystem]
JTProd [constructor, in typesystem]
JTTop [constructor, in typesystem]
JTVar [constructor, in typesystem]
jtype [definition, in typesystem]
jtype_sound [lemma, in Fsoundness]
Judg [definition, in Lsemantics]
Judg_Var [lemma, in Lsemantics]
JVar [constructor, in Ftypesystem]
JVar [constructor, in Ltypesystem]
jwf [inductive, in typesystem]
jwf_sound [lemma, in Fsoundness]
jwf_subst_0 [lemma, in typesystem]
jwf_subst [lemma, in typesystem]
jwf_lift_0 [lemma, in typesystem]
jwf_lift [lemma, in typesystem]
jwf_delta [lemma, in examples]
L
Lam [constructor, in Llanguage]Lam [constructor, in Flanguage]
Lam_sem [lemma, in Lsemantics]
Lc [definition, in Lsemantics]
Lc [definition, in Fsemantics]
Lc_Cl [lemma, in Lsemantics]
Lc_Cl [lemma, in Fsemantics]
lessen [definition, in Flanguage]
lessen_subst [lemma, in Flanguage]
lessen_lessen [lemma, in Flanguage]
lessen_lift [lemma, 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_lessen_trivial [lemma, in Flanguage]
le_term_lessen [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_inject [lemma, in typesystem]
lift_subst2_0_1 [lemma, in typesystem]
lift_subst2_0 [lemma, in typesystem]
lift_subst1_0 [lemma, in typesystem]
lift_subst2 [lemma, in typesystem]
lift_subst1 [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]
Llanguage [library]
Lsemantics [library]
Lsoundness [library]
Ltypesystem [library]
lt_term_le [lemma, in Flanguage]
M
map_fuel_lift [lemma, in Flanguage]map_fuel [definition, in Flanguage]
measure [definition, in Fnormalization]
measure_lessen [lemma, in Fnormalization]
minmax [library]
Mu [constructor, in typesystem]
Mu [definition, in Fsemantics]
Mu_sub [lemma, 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]
M01 [lemma, in mxx]
M11 [lemma, in mxx]
M12 [lemma, in mxx]
M22 [lemma, in mxx]
N
N [definition, in Llanguage]N [definition, in Flanguage]
NE [constructor, in typesystem]
NE [definition, in Fsemantics]
NE_id [lemma, in Fsemantics]
nth_sem [lemma, in Fsoundness]
nth_jerasable_env [lemma, in typesystemequiv]
nth_jerasable_env_aux [lemma, in typesystemequiv]
NV [definition, in Flanguage]
NV_Var [lemma, in Flanguage]
N_drop [lemma, in Llanguage]
N_dec [lemma, in Llanguage]
N_dec [lemma, in Flanguage]
O
OK [definition, in Fsemantics]OK [inductive, in Lsoundness]
OKOKstep [lemma, in Lsoundness]
OKstep [definition, in Lsoundness]
OKstepOK [lemma, in Lsoundness]
OKV [lemma, in Fsemantics]
OK_subst_Var [lemma, in Fsemantics]
OK_Pair [lemma, in Fsemantics]
OK_Lam [lemma, in Fsemantics]
OK_Var [lemma, in Fsemantics]
OK_def [lemma, in Fsemantics]
OK_ [constructor, in Lsoundness]
OK_term_id [lemma, in examples]
omega_shit_1 [lemma, in typesystem]
omega_shit_0 [lemma, in typesystem]
P
Pair [constructor, in Llanguage]Pair [constructor, in Flanguage]
Pair_sem [lemma, in Lsemantics]
PArr [definition, in Lsemantics]
PArr [definition, in Fsemantics]
Pcn [definition, in Lsemantics]
Pcn [definition, in Fsemantics]
Pcn_PExi [lemma, in Lsemantics]
Pcn_For [lemma, in Lsemantics]
Pcn_PProd [lemma, in Lsemantics]
Pcn_PArr [lemma, in Lsemantics]
Pcn_approx [lemma, in Fsemantics]
Pcn_TExi [lemma, in Fsemantics]
Pcn_For [lemma, in Fsemantics]
Pcn_PProd [lemma, in Fsemantics]
Pcn_PArr [lemma, in Fsemantics]
Pdec [definition, in Fsemantics]
Pdec_TJudg [lemma, in Fsemantics]
Pdec_EJudg [lemma, in Fsemantics]
Pdec_OK [lemma, in Fsemantics]
PExi [definition, in Lsemantics]
PExi_preserve [definition, in Lsemantics]
Pexp [definition, in Lsemantics]
Pexp [definition, in Fsemantics]
Pexp_Exi [lemma, in Lsemantics]
Pexp_For [lemma, in Lsemantics]
Pexp_Cl [lemma, in Lsemantics]
Pexp_SN [lemma, in Lsemantics]
Pexp_EExi [lemma, in Fsemantics]
Pexp_For [lemma, in Fsemantics]
Pexp_Cl [lemma, in Fsemantics]
Pexp_OK [lemma, in Fsemantics]
pmap [definition, in typesystem]
Pok [definition, in Fsemantics]
Pok_TJudg [lemma, in Fsemantics]
Pok_EJudg [lemma, in Fsemantics]
PProd [definition, in Lsemantics]
PProd [definition, in Fsemantics]
Pred [definition, in Lsemantics]
Pred [definition, in Fsemantics]
Pred_Judg [lemma, in Lsemantics]
Pred_SN [lemma, in Lsemantics]
Pred_TJudg [lemma, in Fsemantics]
Pred_EJudg [lemma, in Fsemantics]
Pred_OK [lemma, in Fsemantics]
prevalue_is_value [lemma, in Llanguage]
Prod [definition, in Lsemantics]
Prod [constructor, in typesystem]
progre [lemma, in Llanguage]
propositional_extensionality [axiom, in ext]
Psn [definition, in Lsemantics]
Psn_Judg [lemma, in Lsemantics]
Psn_Cl [lemma, in Lsemantics]
Push_right_Arr [lemma, in Fsemantics]
R
red [inductive, in Llanguage]Red [definition, in Lsemantics]
Red [definition, in Fsemantics]
red [inductive, in Flanguage]
RedApp [constructor, in Llanguage]
RedApp [constructor, in Flanguage]
RedCN [lemma, in Lsemantics]
RedCN [lemma, in Fsemantics]
RedCtxApp1 [constructor, in Llanguage]
RedCtxApp1 [constructor, in Flanguage]
RedCtxApp2 [constructor, in Llanguage]
RedCtxApp2 [constructor, in Flanguage]
RedCtxFst [constructor, in Llanguage]
RedCtxFst [constructor, in Flanguage]
RedCtxLam [constructor, in Llanguage]
RedCtxLam [constructor, in Flanguage]
RedCtxPair1 [constructor, in Llanguage]
RedCtxPair1 [constructor, in Flanguage]
RedCtxPair2 [constructor, in Llanguage]
RedCtxPair2 [constructor, in Flanguage]
RedCtxSnd [constructor, in Llanguage]
RedCtxSnd [constructor, in Flanguage]
RedFst [constructor, in Llanguage]
RedFst [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_lessen [lemma, in Flanguage]
red_subst [lemma, in Flanguage]
red_0 [lemma, in Flanguage]
replicate [lemma, in list]
R_Var [lemma, in Lsemantics]
R_lessen [lemma, in Fsemantics]
R_Var [lemma, in Fsemantics]
S
scoer [definition, in Fsoundness]Scoer [constructor, in typesystem]
Scons [constructor, in typesystem]
sem_term_env_lift [lemma, in Fsoundness]
sem_erasable_env_lift [lemma, in Fsoundness]
sem_erasable_env_app [lemma, in Fsoundness]
sem_coer_env2sem_type [lemma, in Fsoundness]
sem_type2sem_coer_env [lemma, in Fsoundness]
sem_coer_env_k_app [lemma, in Fsoundness]
sem_coer_env_app [lemma, in Fsoundness]
sem_coer_env_shift [lemma, in Fsoundness]
sem_coer_env_k_lift [lemma, in Fsoundness]
sem_coer_env_lift [lemma, in Fsoundness]
sem_coer_env_to_k [lemma, in Fsoundness]
sem_coer_env_k_dec [lemma, in Fsoundness]
sem_term_env [definition, in Fsoundness]
sem_erasable_env [definition, in Fsoundness]
sem_coer_env_k [definition, in Fsoundness]
sem_coer_env [definition, in Fsoundness]
sem_type_env [definition, in Fsoundness]
sem_type_subst1_0 [lemma, in Fsoundness]
sem_type_subst_0 [lemma, in Fsoundness]
sem_type_subst [lemma, in Fsoundness]
sem_type_lift_0 [lemma, in Fsoundness]
sem_type_shift [lemma, in Fsoundness]
sem_type_lift [lemma, in Fsoundness]
sem_type [definition, in Fsoundness]
serasable [definition, in Fsoundness]
serasable_env [definition, in Fsoundness]
serasable_sem2Forall_type [lemma, in Fsoundness]
serasable_sem [definition, in Fsoundness]
set [definition, in Llanguage]
set [definition, in set]
set [definition, in Flanguage]
set [library]
shift [definition, in Llanguage]
shift [definition, in typesystem]
shift [definition, in Flanguage]
slift [definition, in typesystem]
Slist [constructor, in typesystem]
Slistcoer [abbreviation, in typesystem]
Slistprodtype [abbreviation, in typesystem]
Slisttype [abbreviation, in typesystem]
SN [inductive, in Llanguage]
Snd [constructor, in Llanguage]
Snd [constructor, in Flanguage]
Snd_sem [lemma, in Lsemantics]
Snil [constructor, in typesystem]
SN_ [constructor, in Llanguage]
SN_subst_Var [lemma, in Lsemantics]
SN_Pair [lemma, in Lsemantics]
SN_Lam [lemma, in Lsemantics]
SN_Var [lemma, in Lsemantics]
sort [inductive, in typesystem]
sort_type [definition, in typesystem]
Spair [constructor, in typesystem]
split_Cl [lemma, in Lsemantics]
split_Cl [lemma, in Fsemantics]
Sprod [constructor, in typesystem]
Sprodtype [abbreviation, in typesystem]
ssubst [definition, in typesystem]
sterm [definition, in Fsoundness]
sterm_env [definition, in Fsoundness]
stype [definition, in Fsoundness]
Stype [constructor, in typesystem]
subst [definition, in Llanguage]
Subst [definition, in Lsemantics]
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_inject [lemma, in typesystem]
subst_app_0 [lemma, in typesystem]
subst_app [lemma, in typesystem]
subst_subst_0_1 [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_lessen [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]
subst1 [definition, in typesystem]
swf [definition, in Fsoundness]
swfsort [definition, in Fsoundness]
T
TApp_sem [lemma, in Fsemantics]TArr [definition, in Fsemantics]
TBot [definition, in Fsemantics]
TCoer_sem [lemma, in Fsemantics]
term [inductive, in Llanguage]
term [inductive, in Flanguage]
term_ge_fill [lemma, in Llanguage]
term_env [definition, in typesystem]
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_lessen [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_lessen [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]
term_omega_red [lemma, in examples]
term_omega [definition, in examples]
term_delta [definition, in examples]
term_id [definition, in examples]
TExi [definition, in Fsemantics]
TExi_preserve [definition, in Fsemantics]
TFst_sem [lemma, in Fsemantics]
TJudg [definition, in Fsemantics]
TJudg_Var [lemma, in Fsemantics]
TLam_sem [lemma, in Fsemantics]
TMu [definition, in Fsemantics]
Top [definition, in Lsemantics]
Top [constructor, in typesystem]
TPair_sem [lemma, in Fsemantics]
TProd [definition, in Fsemantics]
traverse [definition, in Llanguage]
traverse [definition, in typesystem]
traverse [definition, in Flanguage]
TSnd_sem [lemma, in Fsemantics]
TTop [definition, in Fsemantics]
TVar_sem [lemma, in Fsemantics]
type [inductive, in typesystem]
typesystem [library]
typesystemequiv [library]
type_env [abbreviation, in typesystem]
type_omega [definition, in examples]
type_delta [definition, in examples]
type_id [definition, in examples]
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]
V
V [definition, in Llanguage]V [definition, in Flanguage]
value [definition, in Llanguage]
Var [constructor, in Llanguage]
Var [constructor, in typesystem]
Var [constructor, in Flanguage]
Var_x [definition, in Llanguage]
Var_sem [lemma, in Lsemantics]
Var_a [definition, in typesystem]
Var_x [definition, in Flanguage]
V_value [lemma, in Llanguage]
V_drop [lemma, in Llanguage]
V_subst_N [lemma, in Flanguage]
V_Pair [lemma, in Flanguage]
V_Lam [lemma, in Flanguage]
V_Var [lemma, in Flanguage]
W
WF [constructor, in typesystem]WF [definition, in Fsemantics]
WFArr [constructor, in typesystem]
WFFor [constructor, in typesystem]
WFj [definition, in Fsemantics]
WFj_Mu [lemma, in Fsemantics]
WFj_min [lemma, in Fsemantics]
WFj_EExi [lemma, in Fsemantics]
WFj_TExi [lemma, in Fsemantics]
WFj_For [lemma, in Fsemantics]
WFj_EProd [lemma, in Fsemantics]
WFj_EArr [lemma, in Fsemantics]
WFj_ [lemma, in Fsemantics]
WFj_WF [lemma, in Fsemantics]
WFj_dec [lemma, in Fsemantics]
WFMu [constructor, in typesystem]
WFne [constructor, in typesystem]
WFProd [constructor, in typesystem]
wfsort [inductive, in typesystem]
WFVar [constructor, in typesystem]
WFwf [constructor, in typesystem]
wf_der [lemma, in Fnormalization]
WF_period [lemma, in Fsemantics]
WF_TProd [lemma, in Fsemantics]
WF_EProd [lemma, in Fsemantics]
WF_PProd [lemma, in Fsemantics]
WF_TArr [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]
Library Index
E
examplesext
F
FlanguageFnormalization
Fsemantics
Fsoundness
Ftypesystem
L
listLlanguage
Lsemantics
Lsoundness
Ltypesystem
M
minmaxmxx
S
setT
typesystemtypesystemequiv
Lemma Index
A
and_extensionality [in ext]approx_For [in Fsemantics]
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_sem [in Lsemantics]
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_Bot [in Lsemantics]CE_Top [in Lsemantics]
CE_Exi [in Lsemantics]
CE_For [in Lsemantics]
CE_Prod [in Lsemantics]
CE_Arr [in Lsemantics]
CE_Cl [in Lsemantics]
CE_CPexp [in Lsemantics]
CE_EMu [in Fsemantics]
CE_EBot [in Fsemantics]
CE_ETop [in Fsemantics]
CE_EExi [in Fsemantics]
CE_For [in Fsemantics]
CE_EProd [in Fsemantics]
CE_EArr [in Fsemantics]
CE_Cl [in Fsemantics]
CE_CPexp [in Fsemantics]
CF_iter_F [in Fsemantics]
Cl_Lc [in Lsemantics]
Cl_monotone [in Lsemantics]
Cl_def [in Lsemantics]
Cl_approx_For [in Fsemantics]
Cl_For [in Fsemantics]
Cl_approx_eq [in Fsemantics]
Cl_approx [in Fsemantics]
Cl_Lc [in Fsemantics]
Cl_CE [in Fsemantics]
Cl_monotone [in Fsemantics]
Cl_def [in Fsemantics]
CNvalue_is_prevalue [in Llanguage]
CN_N [in Llanguage]
CN_N [in Flanguage]
coer_coer_env_lift_app [in typesystemequiv]
coer_coer_env_app [in typesystemequiv]
coer_coer_env_lift [in typesystemequiv]
coer_coer_env_listcoer_subst [in typesystemequiv]
coer_coer_env_listcoer [in typesystemequiv]
coer_coer_env_listprodtype [in typesystemequiv]
coer_coer_env_listtype [in typesystemequiv]
coer_coer_env_type [in typesystemequiv]
coer_left_type_listcoer_subst [in typesystemequiv]
coer_left_type_listcoer [in typesystemequiv]
coer_left_type_listprodtype [in typesystemequiv]
coer_left_type_listtype [in typesystemequiv]
coer_left_type_type [in typesystemequiv]
Coer_sem [in Lsemantics]
CST_WF [in Fsemantics]
CT_PExi [in Lsemantics]
CT_For [in Lsemantics]
CT_PProd [in Lsemantics]
CT_PArr [in Lsemantics]
CT_Lc [in Lsemantics]
CT_CPcn [in Lsemantics]
CT_TMu [in Fsemantics]
CT_approx [in Fsemantics]
CT_TBot [in Fsemantics]
CT_TTop [in Fsemantics]
CT_TExi [in Fsemantics]
CT_For [in Fsemantics]
CT_TProd [in Fsemantics]
CT_TArr [in Fsemantics]
CT_Lc [in Fsemantics]
CT_CPcn [in Fsemantics]
cut_length [in list]
Cv [in Fsemantics]
CVar_sound [in Fsoundness]
C_Judg [in Lsemantics]
C_Bot [in Lsemantics]
C_Top [in Lsemantics]
C_PExi [in Lsemantics]
C_For [in Lsemantics]
C_PProd [in Lsemantics]
C_PArr [in Lsemantics]
C_Cl [in Lsemantics]
C_CE [in Lsemantics]
C_CT [in Lsemantics]
C_TJudg [in Fsemantics]
C_EJudg [in Fsemantics]
C_approx [in Fsemantics]
C_TBot [in Fsemantics]
C_EBot [in Fsemantics]
C_TTop [in Fsemantics]
C_ETop [in Fsemantics]
C_TExi [in Fsemantics]
C_For [in Fsemantics]
C_PProd [in Fsemantics]
C_PArr [in Fsemantics]
C_Cl [in Fsemantics]
C_CE [in Fsemantics]
C_CT [in Fsemantics]
D
DecCN [in Fsemantics]DecN [in Fsemantics]
DecNV [in Fsemantics]
destruct_Cl_N [in Lsemantics]
destruct_Cl_CN [in Lsemantics]
destruct_Cl_N [in Fsemantics]
destruct_Cl_CN [in Fsemantics]
distrib [in Lsemantics]
dmap_app [in typesystem]
dmap_subst_lift [in typesystem]
dmap_lift_subst2 [in typesystem]
dmap_lift_subst1 [in typesystem]
dmap_lift_lift [in typesystem]
dmap_lift_plus [in typesystem]
dmap_lift_fusion [in typesystem]
dmap_lift_0 [in typesystem]
drop_red_exists [in Llanguage]
drop_fill [in Llanguage]
drop_subst [in Llanguage]
drop_lift [in Llanguage]
drop_lessen [in Llanguage]
E
EApp_sem [in Fsemantics]ECoer_sem [in Fsemantics]
Edistrib [in Fsemantics]
EFst_sem [in Fsemantics]
EJudg_Var [in Fsemantics]
ELam_sem [in Fsemantics]
EMu_sub [in Fsemantics]
EPair_sem [in Fsemantics]
Err_drop [in Llanguage]
ESnd_sem [in Fsemantics]
EVar_sem [in Fsemantics]
exists_extensionality [in ext]
ExpSN [in Llanguage]
extEq [in set]
extract_subst [in typesystem]
extract_lift [in typesystem]
extract_inject [in typesystem]
extract_inj [in typesystem]
extract_eq [in typesystem]
F
fold_Cl [in Lsemantics]fold_Cl [in Fsemantics]
fold_OK [in Fsemantics]
Forall_coer2sem_type [in Fsoundness]
forall_extensionality [in ext]
Forall_map_impl [in list]
Forall_map [in list]
Forall_app [in list]
Forall_nth [in list]
For_approx [in Fsemantics]
Fst_sem [in Lsemantics]
I
Incf_nil [in typesystem]Incf_refl [in typesystem]
Incf_app [in typesystem]
Incf_lift [in typesystem]
Inc_approx [in Fsemantics]
ind_red [in Fnormalization]
inject_extract [in typesystem]
irred_value [in Llanguage]
iter_le [in Fsemantics]
iter_dec [in Fsemantics]
iter_preserve [in Fsemantics]
J
jcoer_sound [in Fsoundness]jcoer_rebuild_jterm_env [in typesystemequiv]
jcoer_env_jerasable_Z [in typesystemequiv]
jcoer_env_lift [in typesystemequiv]
jcoer_extract_left_type [in typesystem]
jcoer_extract_right_type [in typesystem]
jcoer_extract_jerasable_env [in typesystem]
jcoer_weak_coerY_0 [in typesystem]
jcoer_weak_coerY [in typesystem]
jerasable_env_sound [in Fsoundness]
jerasable_sound [in Fsoundness]
jerasable_env_up_1 [in typesystemequiv]
jerasable_bind_up_1 [in typesystemequiv]
jerasable_up_1 [in typesystemequiv]
jerasable_env_jerasable_Z [in typesystemequiv]
jerasable_env_bind [in typesystemequiv]
jerasable_env_lift [in typesystemequiv]
jerasable_bind_lift [in typesystemequiv]
jerasable_bind_only_type [in typesystemequiv]
jerasable_list_app [in typesystemequiv]
jerasable_env_up_2 [in typesystemequiv]
jerasable_bind_up_2 [in typesystemequiv]
jerasable_up_2 [in typesystemequiv]
jerasable_env_down [in typesystemequiv]
jerasable_bind_down [in typesystemequiv]
jerasable_down [in typesystemequiv]
jerasable_subst_0 [in typesystem]
jerasable_subst [in typesystem]
jerasable_nth_subst [in typesystem]
jerasable_nth [in typesystem]
jerasable_lift_0 [in typesystem]
jerasable_lift [in typesystem]
jerasable_weak_coer_0 [in typesystem]
jerasable_weak_coer [in typesystem]
jterm_extract_jtype [in Ftypesystem]
jterm_extract_jterm_env [in Ftypesystem]
jterm_sound [in Fsoundness]
jterm_env_sound [in Fsoundness]
jterm_up_1 [in typesystemequiv]
jterm_env_up_1 [in typesystemequiv]
jterm_up_2 [in typesystemequiv]
jterm_env_up_2 [in typesystemequiv]
jterm_down [in typesystemequiv]
jterm_env_down [in typesystemequiv]
jterm_extract_jtype [in Ltypesystem]
jterm_extract_jterm_env [in Ltypesystem]
jterm_env_extract_jerasable_env [in typesystem]
jterm_sound [in Lsoundness]
jterm_aux_rev [in Lsoundness]
jterm_aux [in Lsoundness]
jterm_2_delta [in examples]
jterm_0_delta [in examples]
jterm_2_id [in examples]
jterm_env_1 [in examples]
jterm_0_id [in examples]
jtype_sound [in Fsoundness]
Judg_Var [in Lsemantics]
jwf_sound [in Fsoundness]
jwf_subst_0 [in typesystem]
jwf_subst [in typesystem]
jwf_lift_0 [in typesystem]
jwf_lift [in typesystem]
jwf_delta [in examples]
L
Lam_sem [in Lsemantics]Lc_Cl [in Lsemantics]
Lc_Cl [in Fsemantics]
lessen_subst [in Flanguage]
lessen_lessen [in Flanguage]
lessen_lift [in Flanguage]
le_term_lt [in Flanguage]
le_term_le [in Flanguage]
le_term_red [in Flanguage]
le_term_subst [in Flanguage]
le_term_lessen_trivial [in Flanguage]
le_term_lessen [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_inject [in typesystem]
lift_subst2_0_1 [in typesystem]
lift_subst2_0 [in typesystem]
lift_subst1_0 [in typesystem]
lift_subst2 [in typesystem]
lift_subst1 [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]
lt_term_le [in Flanguage]
M
map_fuel_lift [in Flanguage]measure_lessen [in Fnormalization]
Mu_sub [in Fsemantics]
Mu_Mu' [in Fsemantics]
Mu_fold [in Fsemantics]
Mu_unfold [in Fsemantics]
Mu_approx_iter [in Fsemantics]
M01 [in mxx]
M11 [in mxx]
M12 [in mxx]
M22 [in mxx]
N
NE_id [in Fsemantics]nth_sem [in Fsoundness]
nth_jerasable_env [in typesystemequiv]
nth_jerasable_env_aux [in typesystemequiv]
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_subst_Var [in Fsemantics]
OK_Pair [in Fsemantics]
OK_Lam [in Fsemantics]
OK_Var [in Fsemantics]
OK_def [in Fsemantics]
OK_term_id [in examples]
omega_shit_1 [in typesystem]
omega_shit_0 [in typesystem]
P
Pair_sem [in Lsemantics]Pcn_PExi [in Lsemantics]
Pcn_For [in Lsemantics]
Pcn_PProd [in Lsemantics]
Pcn_PArr [in Lsemantics]
Pcn_approx [in Fsemantics]
Pcn_TExi [in Fsemantics]
Pcn_For [in Fsemantics]
Pcn_PProd [in Fsemantics]
Pcn_PArr [in Fsemantics]
Pdec_TJudg [in Fsemantics]
Pdec_EJudg [in Fsemantics]
Pdec_OK [in Fsemantics]
Pexp_Exi [in Lsemantics]
Pexp_For [in Lsemantics]
Pexp_Cl [in Lsemantics]
Pexp_SN [in Lsemantics]
Pexp_EExi [in Fsemantics]
Pexp_For [in Fsemantics]
Pexp_Cl [in Fsemantics]
Pexp_OK [in Fsemantics]
Pok_TJudg [in Fsemantics]
Pok_EJudg [in Fsemantics]
Pred_Judg [in Lsemantics]
Pred_SN [in Lsemantics]
Pred_TJudg [in Fsemantics]
Pred_EJudg [in Fsemantics]
Pred_OK [in Fsemantics]
prevalue_is_value [in Llanguage]
progre [in Llanguage]
Psn_Judg [in Lsemantics]
Psn_Cl [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_lessen [in Flanguage]
red_subst [in Flanguage]
red_0 [in Flanguage]
replicate [in list]
R_Var [in Lsemantics]
R_lessen [in Fsemantics]
R_Var [in Fsemantics]
S
sem_term_env_lift [in Fsoundness]sem_erasable_env_lift [in Fsoundness]
sem_erasable_env_app [in Fsoundness]
sem_coer_env2sem_type [in Fsoundness]
sem_type2sem_coer_env [in Fsoundness]
sem_coer_env_k_app [in Fsoundness]
sem_coer_env_app [in Fsoundness]
sem_coer_env_shift [in Fsoundness]
sem_coer_env_k_lift [in Fsoundness]
sem_coer_env_lift [in Fsoundness]
sem_coer_env_to_k [in Fsoundness]
sem_coer_env_k_dec [in Fsoundness]
sem_type_subst1_0 [in Fsoundness]
sem_type_subst_0 [in Fsoundness]
sem_type_subst [in Fsoundness]
sem_type_lift_0 [in Fsoundness]
sem_type_shift [in Fsoundness]
sem_type_lift [in Fsoundness]
serasable_sem2Forall_type [in Fsoundness]
Snd_sem [in Lsemantics]
SN_subst_Var [in Lsemantics]
SN_Pair [in Lsemantics]
SN_Lam [in Lsemantics]
SN_Var [in Lsemantics]
split_Cl [in Lsemantics]
split_Cl [in Fsemantics]
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_inject [in typesystem]
subst_app_0 [in typesystem]
subst_app [in typesystem]
subst_subst_0_1 [in typesystem]
subst_subst_0 [in typesystem]
subst_subst [in typesystem]
subst_lift_0 [in typesystem]
subst_lift [in typesystem]
subst_lessen [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
TApp_sem [in Fsemantics]TCoer_sem [in Fsemantics]
term_ge_fill [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_lessen [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_lessen [in Flanguage]
term_ge_dec [in Flanguage]
term_ge_OK [in Lsoundness]
term_omega_red [in examples]
TFst_sem [in Fsemantics]
TJudg_Var [in Fsemantics]
TLam_sem [in Fsemantics]
TPair_sem [in Fsemantics]
TSnd_sem [in Fsemantics]
TVar_sem [in Fsemantics]
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
Var_sem [in Lsemantics]V_value [in Llanguage]
V_drop [in Llanguage]
V_subst_N [in Flanguage]
V_Pair [in Flanguage]
V_Lam [in Flanguage]
V_Var [in Flanguage]
W
WFj_Mu [in Fsemantics]WFj_min [in Fsemantics]
WFj_EExi [in Fsemantics]
WFj_TExi [in Fsemantics]
WFj_For [in Fsemantics]
WFj_EProd [in Fsemantics]
WFj_EArr [in Fsemantics]
WFj_ [in Fsemantics]
WFj_WF [in Fsemantics]
WFj_dec [in Fsemantics]
wf_der [in Fnormalization]
WF_period [in Fsemantics]
WF_TProd [in Fsemantics]
WF_EProd [in Fsemantics]
WF_PProd [in Fsemantics]
WF_TArr [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]
Constructor Index
A
App [in Llanguage]App [in Flanguage]
Arr [in typesystem]
B
Bot [in typesystem]C
CCcoer [in typesystemequiv]CCcons [in typesystemequiv]
CCnil [in typesystemequiv]
CCpair [in typesystemequiv]
CCtype [in typesystemequiv]
CEcoer [in typesystemequiv]
CElist [in typesystemequiv]
CEprod [in typesystemequiv]
CEtype [in typesystemequiv]
CE_ [in Lsemantics]
CE_ [in Fsemantics]
ClExp [in Lsemantics]
ClR [in Lsemantics]
CRcoer [in typesystemequiv]
CRcons [in typesystemequiv]
CRnil [in typesystemequiv]
CRpair [in typesystemequiv]
CRtype [in typesystemequiv]
CT_ [in Lsemantics]
CT_ [in Fsemantics]
C_ [in Lsemantics]
C_ [in Fsemantics]
E
Ecoer [in typesystem]Econs [in typesystem]
Enil [in typesystem]
Epair [in typesystem]
ErrApp [in Llanguage]
ErrApp [in Flanguage]
ErrCtxApp1 [in Llanguage]
ErrCtxApp1 [in Flanguage]
ErrCtxApp2 [in Llanguage]
ErrCtxApp2 [in Flanguage]
ErrCtxFst [in Llanguage]
ErrCtxFst [in Flanguage]
ErrCtxLam [in Llanguage]
ErrCtxLam [in Flanguage]
ErrCtxPair1 [in Llanguage]
ErrCtxPair1 [in Flanguage]
ErrCtxPair2 [in Llanguage]
ErrCtxPair2 [in Flanguage]
ErrCtxSnd [in Llanguage]
ErrCtxSnd [in Flanguage]
ErrFst [in Llanguage]
ErrFst [in Flanguage]
ErrSnd [in Llanguage]
ErrSnd [in Flanguage]
Etype [in typesystem]
F
For [in typesystem]Fst [in Llanguage]
Fst [in Flanguage]
J
JApp [in Ftypesystem]JApp [in Ltypesystem]
JCArr [in typesystem]
JCBot [in typesystem]
JCFix [in typesystem]
JCFold [in typesystem]
JCGen [in typesystem]
JCInst [in typesystem]
JCoer [in Ftypesystem]
JCoer [in Ltypesystem]
JCProd [in typesystem]
JCRefl [in typesystem]
JCTop [in typesystem]
JCTrans [in typesystem]
JCUnfold [in typesystem]
JCVar [in typesystem]
JCWeak [in typesystem]
JEcons [in typesystem]
JEnil [in typesystem]
JFst [in Ftypesystem]
JFst [in Ltypesystem]
JLam [in Ftypesystem]
JLam [in Ltypesystem]
JPair [in Ftypesystem]
JPair [in Ltypesystem]
JSCons [in typesystem]
JSnd [in Ftypesystem]
JSnd [in Ltypesystem]
JSNil [in typesystem]
JSPair [in typesystem]
JTArr [in typesystem]
JTBot [in typesystem]
JTFor [in typesystem]
JTMu [in typesystem]
JTProd [in typesystem]
JTTop [in typesystem]
JTVar [in typesystem]
JVar [in Ftypesystem]
JVar [in Ltypesystem]
L
Lam [in Llanguage]Lam [in Flanguage]
M
Mu [in typesystem]N
NE [in typesystem]O
OK_ [in Lsoundness]P
Pair [in Llanguage]Pair [in Flanguage]
Prod [in typesystem]
R
RedApp [in Llanguage]RedApp [in Flanguage]
RedCtxApp1 [in Llanguage]
RedCtxApp1 [in Flanguage]
RedCtxApp2 [in Llanguage]
RedCtxApp2 [in Flanguage]
RedCtxFst [in Llanguage]
RedCtxFst [in Flanguage]
RedCtxLam [in Llanguage]
RedCtxLam [in Flanguage]
RedCtxPair1 [in Llanguage]
RedCtxPair1 [in Flanguage]
RedCtxPair2 [in Llanguage]
RedCtxPair2 [in Flanguage]
RedCtxSnd [in Llanguage]
RedCtxSnd [in Flanguage]
RedFst [in Llanguage]
RedFst [in Flanguage]
RedSnd [in Llanguage]
RedSnd [in Flanguage]
S
Scoer [in typesystem]Scons [in typesystem]
Slist [in typesystem]
Snd [in Llanguage]
Snd [in Flanguage]
Snil [in typesystem]
SN_ [in Llanguage]
Spair [in typesystem]
Sprod [in typesystem]
Stype [in typesystem]
T
Top [in typesystem]V
Var [in Llanguage]Var [in typesystem]
Var [in Flanguage]
W
WF [in typesystem]WFArr [in typesystem]
WFFor [in typesystem]
WFMu [in typesystem]
WFne [in typesystem]
WFProd [in typesystem]
WFVar [in typesystem]
WFwf [in typesystem]
Axiom Index
P
propositional_extensionality [in ext]Inductive Index
C
Cl [in Lsemantics]coer_coer_env [in typesystemequiv]
coer_ext_env [in typesystemequiv]
coer_left_type [in typesystemequiv]
E
Err [in Llanguage]Err [in Flanguage]
extract [in typesystem]
J
jerasable [in typesystem]jerasable_env [in typesystem]
jterm [in Ftypesystem]
jterm [in Ltypesystem]
jwf [in typesystem]
O
OK [in Lsoundness]R
red [in Llanguage]red [in Flanguage]
S
SN [in Llanguage]sort [in typesystem]
T
term [in Llanguage]term [in Flanguage]
type [in typesystem]
W
wfsort [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]
CTcn [in Lsemantics]
CTcn [in Fsemantics]
CTdec [in Fsemantics]
CTok [in Fsemantics]
CTred [in Lsemantics]
CTred [in Fsemantics]
CTsn [in Lsemantics]
Abbreviation Index
S
Slistcoer [in typesystem]Slistprodtype [in typesystem]
Slisttype [in typesystem]
Sprodtype [in typesystem]
T
type_env [in typesystem]Definition Index
A
approx [in Fsemantics]Arr [in Lsemantics]
B
binary_fuel [in Flanguage]Bot [in Lsemantics]
C
CF [in Fsemantics]Cl [in Fsemantics]
Cmp [in set]
CN [in Llanguage]
CN [in Flanguage]
coer_env [in typesystem]
CST [in Fsemantics]
D
Dec [in Fsemantics]DecV [in Fsemantics]
der [in Fnormalization]
dmap [in typesystem]
drop [in Llanguage]
E
EArr [in Fsemantics]EBot [in Fsemantics]
EExi [in Fsemantics]
EExi_preserve [in Fsemantics]
EJudg [in Fsemantics]
elift [in typesystem]
EMu [in Fsemantics]
EProd [in Fsemantics]
Eq [in set]
esubst [in typesystem]
ETop [in Fsemantics]
etraverse [in typesystem]
Exi [in Lsemantics]
Exi_preserve [in Lsemantics]
Exp [in Lsemantics]
Exp [in Fsemantics]
ExpFix [in Fsemantics]
F
Fake [in Fsoundness]fill [in Llanguage]
Fix [in Fnormalization]
For [in Lsemantics]
For [in Fsemantics]
For_preserve [in Lsemantics]
For_preserve [in Fsemantics]
I
Inc [in set]Incf [in typesystem]
inject [in typesystem]
inj_list [in typesystem]
Inter [in set]
irred [in Llanguage]
iter [in Fsemantics]
J
jcoer [in typesystem]jcoer_env [in typesystemequiv]
jerasable_bind [in typesystem]
jterm_env [in typesystem]
jtype [in typesystem]
Judg [in Lsemantics]
L
Lc [in Lsemantics]Lc [in Fsemantics]
lessen [in Flanguage]
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]
M
map_fuel [in Flanguage]measure [in Fnormalization]
Mu [in Fsemantics]
Mu' [in Fsemantics]
N
N [in Llanguage]N [in Flanguage]
NE [in Fsemantics]
NV [in Flanguage]
O
OK [in Fsemantics]OKstep [in Lsoundness]
P
PArr [in Lsemantics]PArr [in Fsemantics]
Pcn [in Lsemantics]
Pcn [in Fsemantics]
Pdec [in Fsemantics]
PExi [in Lsemantics]
PExi_preserve [in Lsemantics]
Pexp [in Lsemantics]
Pexp [in Fsemantics]
pmap [in typesystem]
Pok [in Fsemantics]
PProd [in Lsemantics]
PProd [in Fsemantics]
Pred [in Lsemantics]
Pred [in Fsemantics]
Prod [in Lsemantics]
Psn [in Lsemantics]
R
Red [in Lsemantics]Red [in Fsemantics]
S
scoer [in Fsoundness]sem_term_env [in Fsoundness]
sem_erasable_env [in Fsoundness]
sem_coer_env_k [in Fsoundness]
sem_coer_env [in Fsoundness]
sem_type_env [in Fsoundness]
sem_type [in Fsoundness]
serasable [in Fsoundness]
serasable_env [in Fsoundness]
serasable_sem [in Fsoundness]
set [in Llanguage]
set [in set]
set [in Flanguage]
shift [in Llanguage]
shift [in typesystem]
shift [in Flanguage]
slift [in typesystem]
sort_type [in typesystem]
ssubst [in typesystem]
sterm [in Fsoundness]
sterm_env [in Fsoundness]
stype [in Fsoundness]
subst [in Llanguage]
Subst [in Lsemantics]
subst [in typesystem]
Subst [in Fsemantics]
subst [in Flanguage]
subst_idx [in Llanguage]
subst_idx [in typesystem]
subst_idx [in Flanguage]
subst1 [in typesystem]
swf [in Fsoundness]
swfsort [in Fsoundness]
T
TArr [in Fsemantics]TBot [in Fsemantics]
term_env [in typesystem]
term_ge [in Flanguage]
term_lt [in Flanguage]
term_le [in Flanguage]
term_omega [in examples]
term_delta [in examples]
term_id [in examples]
TExi [in Fsemantics]
TExi_preserve [in Fsemantics]
TJudg [in Fsemantics]
TMu [in Fsemantics]
Top [in Lsemantics]
TProd [in Fsemantics]
traverse [in Llanguage]
traverse [in typesystem]
traverse [in Flanguage]
TTop [in Fsemantics]
type_omega [in examples]
type_delta [in examples]
type_id [in examples]
U
unary_fuel [in Flanguage]Union [in set]
V
V [in Llanguage]V [in Flanguage]
value [in Llanguage]
Var_x [in Llanguage]
Var_a [in typesystem]
Var_x [in Flanguage]
W
WF [in Fsemantics]WFj [in Fsemantics]
Record Index
C
C [in Lsemantics]C [in Fsemantics]
CE [in Lsemantics]
CE [in Fsemantics]
CT [in Lsemantics]
CT [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 | (819 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 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 | (450 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 | (143 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 | (21 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 | (19 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 | (5 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 | (157 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 | (6 entries) |
This page has been generated by coqdoc