| 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 | (830 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (21 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 | (312 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 | (285 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 | (11 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 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 | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 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 | (96 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
Abs [constructor, in CoqInCoq.Termes]ABS [constructor, in CoqInCoq.Expr]
absurd_prop [definition, in CoqInCoq.Consistency]
abs_par_red [constructor, in CoqInCoq.Termes]
abs_red_r [constructor, in CoqInCoq.Termes]
abs_red_l [constructor, in CoqInCoq.Termes]
Abs_sound [lemma, in CoqInCoq.Can]
adapt_int_inv [lemma, in CoqInCoq.Int_stab]
adapt_class_equal [projection, in CoqInCoq.Strong_Norm]
adapt_trm_in_int [projection, in CoqInCoq.Strong_Norm]
add_typ [definition, in CoqInCoq.Infer]
adj_T [constructor, in CoqInCoq.Class]
adj_t [constructor, in CoqInCoq.Class]
adj_cls [inductive, in CoqInCoq.Class]
alpha [inductive, in CoqInCoq.Expr]
alp_prod [constructor, in CoqInCoq.Expr]
alp_app [constructor, in CoqInCoq.Expr]
alp_abs [constructor, in CoqInCoq.Expr]
alp_ref [constructor, in CoqInCoq.Expr]
alp_srt [constructor, in CoqInCoq.Expr]
answer [definition, in CoqInCoq.Machine]
App [constructor, in CoqInCoq.Termes]
APP [constructor, in CoqInCoq.Expr]
applist [definition, in CoqInCoq.Consistency]
applist_assoc [lemma, in CoqInCoq.Consistency]
Apply_err [constructor, in CoqInCoq.Infer]
app_par_red [constructor, in CoqInCoq.Termes]
app_red_r [constructor, in CoqInCoq.Termes]
app_red_l [constructor, in CoqInCoq.Termes]
ast [inductive, in CoqInCoq.Machine]
AST_QUIT [constructor, in CoqInCoq.Machine]
AST_LIST [constructor, in CoqInCoq.Machine]
AST_DELETE [constructor, in CoqInCoq.Machine]
AST_AXIOM [constructor, in CoqInCoq.Machine]
AST_CHECK [constructor, in CoqInCoq.Machine]
AST_INFER [constructor, in CoqInCoq.Machine]
atom_inhabitants [lemma, in CoqInCoq.Consistency]
atom_reduction [lemma, in CoqInCoq.Consistency]
AXIOM [constructor, in CoqInCoq.Machine]
B
beta [constructor, in CoqInCoq.Termes]Beta_Reduction [section, in CoqInCoq.Termes]
Bsbt_prod [constructor, in CoqInCoq.Termes]
Bsbt_abs [constructor, in CoqInCoq.Termes]
C
Can [definition, in CoqInCoq.Can]Can [library]
cand_sn [lemma, in CoqInCoq.Can]
cand_sat [lemma, in CoqInCoq.Can]
Cannot_delete [constructor, in CoqInCoq.Machine]
can_adapt [definition, in CoqInCoq.Int_stab]
can_interp [inductive, in CoqInCoq.Int_stab]
ca_T [constructor, in CoqInCoq.Int_stab]
ca_K [constructor, in CoqInCoq.Int_stab]
Ce_delete [constructor, in CoqInCoq.Machine]
Ce_axiom [constructor, in CoqInCoq.Machine]
Ce_decl_error [constructor, in CoqInCoq.Machine]
Ce_chk_error [constructor, in CoqInCoq.Machine]
Ce_inf_error [constructor, in CoqInCoq.Machine]
CHECK [constructor, in CoqInCoq.Machine]
check_typ [definition, in CoqInCoq.Infer]
Chke_exp [constructor, in CoqInCoq.Infer]
Chke_type [constructor, in CoqInCoq.Infer]
Chke_subj [constructor, in CoqInCoq.Infer]
chk_error_no_type [lemma, in CoqInCoq.Infer]
chk_error [inductive, in CoqInCoq.Infer]
church_rosser [lemma, in CoqInCoq.Conv]
Church_Rosser [section, in CoqInCoq.Conv]
class [inductive, in CoqInCoq.Class]
Class [library]
class_red [lemma, in CoqInCoq.Class]
class_sound [lemma, in CoqInCoq.Class]
class_subst [lemma, in CoqInCoq.Class]
class_trm [lemma, in CoqInCoq.Class]
class_typ_ord [lemma, in CoqInCoq.Class]
class_typ [lemma, in CoqInCoq.Class]
class_knd [lemma, in CoqInCoq.Class]
class_env_trunc [lemma, in CoqInCoq.Class]
class_env [definition, in CoqInCoq.Class]
class_of_ik [definition, in CoqInCoq.Int_typ]
clos_red_star [lemma, in CoqInCoq.Can]
clos_exp [projection, in CoqInCoq.Can]
clos_red [projection, in CoqInCoq.Can]
cls [definition, in CoqInCoq.Class]
cls_of_int [definition, in CoqInCoq.Int_typ]
cl_term_conv [lemma, in CoqInCoq.Class]
cl_term_red [lemma, in CoqInCoq.Class]
cl_term_red1 [lemma, in CoqInCoq.Class]
cl_term_sound [lemma, in CoqInCoq.Class]
cl_term_subst [lemma, in CoqInCoq.Class]
cl_trunc [lemma, in CoqInCoq.Class]
cl_term_lift [lemma, in CoqInCoq.Class]
cl_term [definition, in CoqInCoq.Class]
coc_consistency [lemma, in CoqInCoq.Consistency]
coc_consistency_nf [lemma, in CoqInCoq.Consistency]
coerce_CR [definition, in CoqInCoq.Int_typ]
command [inductive, in CoqInCoq.Machine]
commut_case [lemma, in CoqInCoq.Class]
commut_red1_subterm [lemma, in CoqInCoq.Termes]
commut_lift_subst [lemma, in CoqInCoq.Termes]
commut_lift_subst_rec [lemma, in CoqInCoq.Termes]
compute_nf [definition, in CoqInCoq.Conv_Dec]
com_answer [definition, in CoqInCoq.Machine]
com_error [inductive, in CoqInCoq.Machine]
confluence_red [lemma, in CoqInCoq.Conv]
confluence_par_red [lemma, in CoqInCoq.Conv]
confluence_Ered [lemma, in CoqInCoq.Ered]
confluence_Epar_red [lemma, in CoqInCoq.Ered]
Consistency [library]
cons_names [projection, in CoqInCoq.Machine]
cons_env [projection, in CoqInCoq.Machine]
Context_listing [constructor, in CoqInCoq.Machine]
conv [inductive, in CoqInCoq.Termes]
Conv [library]
conv_sort_prod [lemma, in CoqInCoq.Conv]
conv_kind_prop [lemma, in CoqInCoq.Conv]
conv_sort [lemma, in CoqInCoq.Conv]
conv_conv_subst [lemma, in CoqInCoq.Termes]
conv_conv_lift [lemma, in CoqInCoq.Termes]
conv_conv_prod [lemma, in CoqInCoq.Termes]
conv_Econv [lemma, in CoqInCoq.Ered]
conv_int_typ [lemma, in CoqInCoq.Int_stab]
conv_prod_atom [lemma, in CoqInCoq.Consistency]
conv_sort_atom [lemma, in CoqInCoq.Consistency]
Conv_Dec [library]
Correct [constructor, in CoqInCoq.Machine]
cv_skel [definition, in CoqInCoq.Class]
D
dangerous_int_injection [lemma, in CoqInCoq.MlTypes]dangerous_discr [axiom, in CoqInCoq.MlTypes]
db_prod [constructor, in CoqInCoq.Termes]
db_app [constructor, in CoqInCoq.Termes]
db_abs [constructor, in CoqInCoq.Termes]
db_ref [constructor, in CoqInCoq.Termes]
db_srt [constructor, in CoqInCoq.Termes]
Db_error [constructor, in CoqInCoq.Infer]
Decax_type [constructor, in CoqInCoq.Infer]
Decax_ill [constructor, in CoqInCoq.Infer]
Decidabilite_typage [section, in CoqInCoq.Infer]
decide_typ [lemma, in CoqInCoq.Infer]
decide_wf [lemma, in CoqInCoq.Infer]
decl_err_not_wf [lemma, in CoqInCoq.Infer]
decl_error [inductive, in CoqInCoq.Infer]
default_can [definition, in CoqInCoq.Can]
def_inv [lemma, in CoqInCoq.Can]
def_can_cr [lemma, in CoqInCoq.Can]
def_cons [definition, in CoqInCoq.Int_typ]
def_intt_id [lemma, in CoqInCoq.Strong_Norm]
def_adapt [lemma, in CoqInCoq.Strong_Norm]
def_intp_can [lemma, in CoqInCoq.Strong_Norm]
def_intt [definition, in CoqInCoq.Strong_Norm]
def_intp [definition, in CoqInCoq.Strong_Norm]
DELETE [constructor, in CoqInCoq.Machine]
Delete_axiom [constructor, in CoqInCoq.Machine]
distr_subst [lemma, in CoqInCoq.Termes]
distr_subst_rec [lemma, in CoqInCoq.Termes]
distr_lift_subst [lemma, in CoqInCoq.Termes]
distr_lift_subst_rec [lemma, in CoqInCoq.Termes]
E
Eabs [constructor, in CoqInCoq.Ered]Eabs_par_red [constructor, in CoqInCoq.Ered]
Eabs_red_r [constructor, in CoqInCoq.Ered]
Eabs_red_l [constructor, in CoqInCoq.Ered]
Eapp_par_red [constructor, in CoqInCoq.Ered]
Eapp_red_r [constructor, in CoqInCoq.Ered]
Eapp_red_l [constructor, in CoqInCoq.Ered]
ea_ax [constructor, in CoqInCoq.Machine]
ea_chk2 [constructor, in CoqInCoq.Machine]
ea_chk1 [constructor, in CoqInCoq.Machine]
ea_inf [constructor, in CoqInCoq.Machine]
Ebeta [constructor, in CoqInCoq.Ered]
Econv [inductive, in CoqInCoq.Ered]
Econv_Econv_subst [lemma, in CoqInCoq.Ered]
Econv_Econv_lift [lemma, in CoqInCoq.Ered]
Econv_Type_abs [lemma, in CoqInCoq.Ered]
Econv_abs [lemma, in CoqInCoq.Ered]
Econv_sort_prod [lemma, in CoqInCoq.Ered]
Econv_Econv_app [lemma, in CoqInCoq.Ered]
Econv_Econv_prod [lemma, in CoqInCoq.Ered]
Econv_church_rosser [lemma, in CoqInCoq.Ered]
EConv_Conv [lemma, in CoqInCoq.Equiv]
Econv_eq [lemma, in CoqInCoq.Equiv]
EE_c [constructor, in CoqInCoq.Equiv]
EE_n [constructor, in CoqInCoq.Equiv]
empty_state [definition, in CoqInCoq.Machine]
Enormal [definition, in CoqInCoq.Ered]
env [definition, in CoqInCoq.Types]
Epar_red_Ered [lemma, in CoqInCoq.Ered]
Epar_red1_subst [lemma, in CoqInCoq.Ered]
Epar_red1_lift [lemma, in CoqInCoq.Ered]
Epar_red1_Epar_red [lemma, in CoqInCoq.Ered]
Epar_red [definition, in CoqInCoq.Ered]
Epar_abs [constructor, in CoqInCoq.Ered]
Epar_beta [constructor, in CoqInCoq.Ered]
Epar_red1 [inductive, in CoqInCoq.Ered]
Eprod_par_red [constructor, in CoqInCoq.Ered]
Eprod_red_r [constructor, in CoqInCoq.Ered]
Eprod_red_l [constructor, in CoqInCoq.Ered]
eqi_T [constructor, in CoqInCoq.Int_typ]
eqi_K [constructor, in CoqInCoq.Int_typ]
eqterm [definition, in CoqInCoq.Conv_Dec]
Equiv [library]
equiv_no_undef [lemma, in CoqInCoq.Expr]
equiv_unique [lemma, in CoqInCoq.Expr]
equiv_free_db [lemma, in CoqInCoq.Expr]
equiv_env_item [lemma, in CoqInCoq.Equiv]
equiv_env [inductive, in CoqInCoq.Equiv]
eqv_prod [constructor, in CoqInCoq.Expr]
eqv_app [constructor, in CoqInCoq.Expr]
eqv_abs [constructor, in CoqInCoq.Expr]
eqv_ref [constructor, in CoqInCoq.Expr]
eqv_srt [constructor, in CoqInCoq.Expr]
EQ_skel [lemma, in CoqInCoq.Class]
eq_can_Pi [lemma, in CoqInCoq.Can]
eq_cand_incl [lemma, in CoqInCoq.Can]
eq_can_trans [lemma, in CoqInCoq.Can]
eq_can_sym [lemma, in CoqInCoq.Can]
eq_can [definition, in CoqInCoq.Can]
eq_cand [definition, in CoqInCoq.Can]
eq_can_extr [lemma, in CoqInCoq.Int_typ]
Ered [inductive, in CoqInCoq.Ered]
Ered [library]
Ered_sort_mem [lemma, in CoqInCoq.Ered]
Ered_sort_mem2 [lemma, in CoqInCoq.Ered]
Ered_prod_prod [lemma, in CoqInCoq.Ered]
Ered_Enormal [lemma, in CoqInCoq.Ered]
Ered_Econv [lemma, in CoqInCoq.Ered]
Ered_Ered_prod [lemma, in CoqInCoq.Ered]
Ered_Ered_abs [lemma, in CoqInCoq.Ered]
Ered_Ered_app [lemma, in CoqInCoq.Ered]
Ered_Epar_red [lemma, in CoqInCoq.Ered]
Ered_normal_NF_Econv [lemma, in CoqInCoq.Equiv]
Ered1 [inductive, in CoqInCoq.Ered]
Ered1_sort_mem [lemma, in CoqInCoq.Ered]
Ered1_Ered_ind [lemma, in CoqInCoq.Ered]
Ered1_subst_l [lemma, in CoqInCoq.Ered]
Ered1_subst_r [lemma, in CoqInCoq.Ered]
Ered1_lift [lemma, in CoqInCoq.Ered]
Ered1_Epar_red1 [lemma, in CoqInCoq.Ered]
Ered1_normal_NF_Econv [lemma, in CoqInCoq.Equiv]
Ered1_normal_normal [lemma, in CoqInCoq.Equiv]
Erefl [constructor, in CoqInCoq.Ered]
Erefl_conv [constructor, in CoqInCoq.Ered]
Eref_par_red [constructor, in CoqInCoq.Ered]
error [inductive, in CoqInCoq.Machine]
Esort_par_red [constructor, in CoqInCoq.Ered]
Etrans_conv_exp [constructor, in CoqInCoq.Ered]
Etrans_conv_red [constructor, in CoqInCoq.Ered]
Etrans_red [constructor, in CoqInCoq.Ered]
Etyp [inductive, in CoqInCoq.ETypes]
ETypes [library]
Etype_prop_set [lemma, in CoqInCoq.ETypes]
Etype_Econv [constructor, in CoqInCoq.ETypes]
Etype_prod [constructor, in CoqInCoq.ETypes]
Etype_app [constructor, in CoqInCoq.ETypes]
Etype_abs [constructor, in CoqInCoq.ETypes]
Etype_var [constructor, in CoqInCoq.ETypes]
Etype_set [constructor, in CoqInCoq.ETypes]
Etype_prop [constructor, in CoqInCoq.ETypes]
Etyp_mem_kind [lemma, in CoqInCoq.ETypes]
Etyp_inversion [lemma, in CoqInCoq.ETypes]
Etyp_Ewf [lemma, in CoqInCoq.ETypes]
Etyp_free_db [lemma, in CoqInCoq.ETypes]
Etyp_typ [lemma, in CoqInCoq.Equiv]
Etyp_NF_Econv_Econv [lemma, in CoqInCoq.Equiv]
ev_prod_r [constructor, in CoqInCoq.Expr]
ev_prod_l [constructor, in CoqInCoq.Expr]
ev_app_r [constructor, in CoqInCoq.Expr]
ev_app_l [constructor, in CoqInCoq.Expr]
ev_abs_r [constructor, in CoqInCoq.Expr]
ev_abs_l [constructor, in CoqInCoq.Expr]
ev_ref [constructor, in CoqInCoq.Expr]
Ewf [inductive, in CoqInCoq.ETypes]
Ewf_sort [lemma, in CoqInCoq.ETypes]
Ewf_var [constructor, in CoqInCoq.ETypes]
Ewf_nil [constructor, in CoqInCoq.ETypes]
exec_delete [definition, in CoqInCoq.Machine]
exec_axiom [definition, in CoqInCoq.Machine]
exec_check [definition, in CoqInCoq.Machine]
exec_infer [definition, in CoqInCoq.Machine]
Exiting [constructor, in CoqInCoq.Machine]
Expected_type [constructor, in CoqInCoq.Infer]
expln [inductive, in CoqInCoq.Infer]
expln_wf [lemma, in CoqInCoq.Infer]
expr [inductive, in CoqInCoq.Expr]
Expr [library]
expr_of_ast [inductive, in CoqInCoq.Machine]
expr_of_term [definition, in CoqInCoq.Expr]
expr_vars [inductive, in CoqInCoq.Expr]
Exp_appl_err [constructor, in CoqInCoq.Infer]
Exp_fun [constructor, in CoqInCoq.Infer]
Exp_type [constructor, in CoqInCoq.Infer]
Exp_lam_kind [constructor, in CoqInCoq.Infer]
Exp_db [constructor, in CoqInCoq.Infer]
Exp_kind [constructor, in CoqInCoq.Infer]
Exp_exp_type [constructor, in CoqInCoq.Infer]
Exp_under [constructor, in CoqInCoq.Infer]
extr_eq [lemma, in CoqInCoq.Int_typ]
ext_ik [definition, in CoqInCoq.Int_typ]
F
find_free_var [definition, in CoqInCoq.Names]find_free [definition, in CoqInCoq.Names]
first_item_unique [lemma, in CoqInCoq.MyList]
first_item_is_item [lemma, in CoqInCoq.MyList]
first_item [inductive, in CoqInCoq.MyList]
fit_tl [constructor, in CoqInCoq.MyList]
fit_hd [constructor, in CoqInCoq.MyList]
free_db [inductive, in CoqInCoq.Termes]
fun_item [lemma, in CoqInCoq.MyList]
fv_ext [lemma, in CoqInCoq.Names]
G
glob_unique [projection, in CoqInCoq.Machine]glob_length [projection, in CoqInCoq.Machine]
glob_wf_ctx [projection, in CoqInCoq.Machine]
glob_names [projection, in CoqInCoq.Machine]
glob_ctx [projection, in CoqInCoq.Machine]
H
hnf_proofs_sound [lemma, in CoqInCoq.Consistency]hnf_proofs [definition, in CoqInCoq.Consistency]
I
id_int_term [lemma, in CoqInCoq.Strong_Norm]iK [constructor, in CoqInCoq.Int_typ]
iki_K [lemma, in CoqInCoq.Int_typ]
ik_eq [inductive, in CoqInCoq.Int_typ]
In [inductive, in CoqInCoq.MyList]
incl [definition, in CoqInCoq.MyList]
incl_sn [projection, in CoqInCoq.Can]
incl_app_sym [lemma, in CoqInCoq.MyList]
INFER [constructor, in CoqInCoq.Machine]
infer [definition, in CoqInCoq.Infer]
Infer [library]
Infered_type [constructor, in CoqInCoq.Machine]
Infe_type_prod_r [constructor, in CoqInCoq.Infer]
Infe_type_prod_l [constructor, in CoqInCoq.Infer]
Infe_appl_err [constructor, in CoqInCoq.Infer]
Infe_fun [constructor, in CoqInCoq.Infer]
Infe_type_abs [constructor, in CoqInCoq.Infer]
Infe_lam_kind [constructor, in CoqInCoq.Infer]
Infe_db [constructor, in CoqInCoq.Infer]
Infe_kind [constructor, in CoqInCoq.Infer]
Infe_under [constructor, in CoqInCoq.Infer]
Infe_subt [constructor, in CoqInCoq.Infer]
inf_error_no_type [lemma, in CoqInCoq.Infer]
inf_error [inductive, in CoqInCoq.Infer]
inj_var_of_nat [lemma, in CoqInCoq.Names]
insert [inductive, in CoqInCoq.MyList]
insert_tl [constructor, in CoqInCoq.MyList]
insert_hd [constructor, in CoqInCoq.MyList]
ins_item_lt [lemma, in CoqInCoq.Types]
ins_item_ge [lemma, in CoqInCoq.Types]
ins_S [constructor, in CoqInCoq.Types]
ins_O [constructor, in CoqInCoq.Types]
ins_in_env [inductive, in CoqInCoq.Types]
ins_eq [lemma, in CoqInCoq.MyList]
ins_gt [lemma, in CoqInCoq.MyList]
ins_le [lemma, in CoqInCoq.MyList]
ins_int_inv [lemma, in CoqInCoq.Int_typ]
ins_in_cls [lemma, in CoqInCoq.Int_typ]
interp_ast [definition, in CoqInCoq.Machine]
interp_command [definition, in CoqInCoq.Machine]
intP [definition, in CoqInCoq.Int_typ]
intt [definition, in CoqInCoq.Int_term]
int_term_subst [lemma, in CoqInCoq.Int_term]
int_term [definition, in CoqInCoq.Int_term]
int_typ_red1 [lemma, in CoqInCoq.Int_stab]
int_cons_equal [lemma, in CoqInCoq.Int_stab]
int_var_sound_lift [lemma, in CoqInCoq.Int_stab]
int_var_sound [inductive, in CoqInCoq.Int_stab]
int_typ_cr [lemma, in CoqInCoq.Int_stab]
int_equiv_int_typ [lemma, in CoqInCoq.Int_stab]
int_typ [definition, in CoqInCoq.Int_typ]
int_eq_can_cls [lemma, in CoqInCoq.Int_typ]
int_inv_int_eq_can [lemma, in CoqInCoq.Int_typ]
int_inv [definition, in CoqInCoq.Int_typ]
int_eq_can [definition, in CoqInCoq.Int_typ]
int_cons [definition, in CoqInCoq.Int_typ]
Int_K [inductive, in CoqInCoq.Int_typ]
int_sound [lemma, in CoqInCoq.Strong_Norm]
int_can_adapt [projection, in CoqInCoq.Strong_Norm]
int_adapt [record, in CoqInCoq.Strong_Norm]
int_cs [constructor, in CoqInCoq.Strong_Norm]
int_nil [constructor, in CoqInCoq.Strong_Norm]
int_of_nat [definition, in CoqInCoq.MlTypes]
Int_typ [library]
Int_stab [library]
Int_term [library]
inv_Etyp_Econv_kind [lemma, in CoqInCoq.ETypes]
inv_Etyp_prod [lemma, in CoqInCoq.ETypes]
inv_Etyp_app [lemma, in CoqInCoq.ETypes]
inv_Etyp_abs [lemma, in CoqInCoq.ETypes]
inv_Etyp_ref [lemma, in CoqInCoq.ETypes]
inv_Etyp_set [lemma, in CoqInCoq.ETypes]
inv_Etyp_prop [lemma, in CoqInCoq.ETypes]
inv_Etyp_kind [lemma, in CoqInCoq.ETypes]
inv_Etype_Econv [lemma, in CoqInCoq.ETypes]
inv_Etype [definition, in CoqInCoq.ETypes]
inv_conv_prod_r [lemma, in CoqInCoq.Conv]
inv_conv_prod_l [lemma, in CoqInCoq.Conv]
inv_par_red_abs [lemma, in CoqInCoq.Termes]
inv_Ered_Abs [lemma, in CoqInCoq.Ered]
inv_Econv_prod_r [lemma, in CoqInCoq.Ered]
inv_Econv_prod_l [lemma, in CoqInCoq.Ered]
inv_Epar_red_abs [lemma, in CoqInCoq.Ered]
inv_typ_conv_kind [lemma, in CoqInCoq.Types]
inv_typ_prod [lemma, in CoqInCoq.Types]
inv_typ_app [lemma, in CoqInCoq.Types]
inv_typ_abs [lemma, in CoqInCoq.Types]
inv_typ_ref [lemma, in CoqInCoq.Types]
inv_typ_set [lemma, in CoqInCoq.Types]
inv_typ_prop [lemma, in CoqInCoq.Types]
inv_typ_kind [lemma, in CoqInCoq.Types]
inv_type_conv [lemma, in CoqInCoq.Types]
inv_type [definition, in CoqInCoq.Types]
inv_nth_cs [lemma, in CoqInCoq.MyList]
inv_nth_nl [lemma, in CoqInCoq.MyList]
inv_typ_applist_head [lemma, in CoqInCoq.Consistency]
In_app [lemma, in CoqInCoq.MyList]
In_tl [constructor, in CoqInCoq.MyList]
In_hd [constructor, in CoqInCoq.MyList]
is_conv [definition, in CoqInCoq.Conv_Dec]
is_prop [definition, in CoqInCoq.Termes]
is_can_Pi [lemma, in CoqInCoq.Can]
is_can_prop [lemma, in CoqInCoq.Can]
is_can [definition, in CoqInCoq.Can]
is_cand [record, in CoqInCoq.Can]
is_can_coerce [lemma, in CoqInCoq.Int_typ]
is_free_var [definition, in CoqInCoq.Expr]
is_atom_app [lemma, in CoqInCoq.Consistency]
is_atom [definition, in CoqInCoq.Consistency]
is_lam [definition, in CoqInCoq.Equiv]
iT [constructor, in CoqInCoq.Int_typ]
item [inductive, in CoqInCoq.MyList]
item_lift [definition, in CoqInCoq.Types]
item_trunc [lemma, in CoqInCoq.MyList]
item_tl [constructor, in CoqInCoq.MyList]
item_hd [constructor, in CoqInCoq.MyList]
ivs_T [constructor, in CoqInCoq.Int_stab]
ivs_K [constructor, in CoqInCoq.Int_stab]
K
kind [constructor, in CoqInCoq.Termes]Kind_ill_typed [constructor, in CoqInCoq.Infer]
Knd [constructor, in CoqInCoq.Class]
L
Lambda_kind [constructor, in CoqInCoq.Infer]leqc_ord [constructor, in CoqInCoq.Class]
leqc_typ [constructor, in CoqInCoq.Class]
leqc_trm [constructor, in CoqInCoq.Class]
lift [definition, in CoqInCoq.Termes]
lift_rec0 [lemma, in CoqInCoq.Termes]
lift_ref_lt [lemma, in CoqInCoq.Termes]
lift_ref_ge [lemma, in CoqInCoq.Termes]
lift_rec [definition, in CoqInCoq.Termes]
lift_int_typ [lemma, in CoqInCoq.Int_stab]
lift0 [lemma, in CoqInCoq.Termes]
LIST [constructor, in CoqInCoq.Machine]
Listes [section, in CoqInCoq.MyList]
Listes.A [variable, in CoqInCoq.MyList]
Listes.eq_dec [variable, in CoqInCoq.MyList]
Listes.List [variable, in CoqInCoq.MyList]
ListType [library]
list_index [definition, in CoqInCoq.MyList]
list_disjoint [definition, in CoqInCoq.MyList]
list_item [definition, in CoqInCoq.MyList]
loose_eqc_stable [lemma, in CoqInCoq.Class]
loose_eqc_trans [lemma, in CoqInCoq.Class]
loose_eqc [inductive, in CoqInCoq.Class]
M
Machine [library]mem_sort_subst [lemma, in CoqInCoq.Termes]
mem_sort_lift [lemma, in CoqInCoq.Termes]
mem_app_r [constructor, in CoqInCoq.Termes]
mem_app_l [constructor, in CoqInCoq.Termes]
mem_abs_r [constructor, in CoqInCoq.Termes]
mem_abs_l [constructor, in CoqInCoq.Termes]
mem_prod_r [constructor, in CoqInCoq.Termes]
mem_prod_l [constructor, in CoqInCoq.Termes]
mem_eq [constructor, in CoqInCoq.Termes]
mem_sort [inductive, in CoqInCoq.Termes]
mem_sort2_mem_sort [lemma, in CoqInCoq.Ered]
mem_sort2_subst [lemma, in CoqInCoq.Ered]
mem_sort2_lift [lemma, in CoqInCoq.Ered]
mem_app_r2 [constructor, in CoqInCoq.Ered]
mem_app_l2 [constructor, in CoqInCoq.Ered]
mem_abs_r2 [constructor, in CoqInCoq.Ered]
mem_prod_r2 [constructor, in CoqInCoq.Ered]
mem_prod_l2 [constructor, in CoqInCoq.Ered]
mem_eq2 [constructor, in CoqInCoq.Ered]
mem_sort2 [inductive, in CoqInCoq.Ered]
message [inductive, in CoqInCoq.Machine]
MlTypes [library]
ml_x_int_inj [axiom, in CoqInCoq.MlTypes]
ml_x_int [axiom, in CoqInCoq.MlTypes]
ml_eq_string [axiom, in CoqInCoq.MlTypes]
ml_string [axiom, in CoqInCoq.MlTypes]
ml_int_case [axiom, in CoqInCoq.MlTypes]
ml_int_pred [axiom, in CoqInCoq.MlTypes]
ml_succ [axiom, in CoqInCoq.MlTypes]
ml_zero [axiom, in CoqInCoq.MlTypes]
ml_eq_int [axiom, in CoqInCoq.MlTypes]
ml_int [axiom, in CoqInCoq.MlTypes]
MyList [library]
N
name [definition, in CoqInCoq.Names]Names [library]
Name_clash [constructor, in CoqInCoq.Machine]
name_unique_first [lemma, in CoqInCoq.Names]
name_unique [definition, in CoqInCoq.Names]
name_dec [definition, in CoqInCoq.Names]
Nbsbt_prod [constructor, in CoqInCoq.Termes]
Nbsbt_app_r [constructor, in CoqInCoq.Termes]
Nbsbt_app_l [constructor, in CoqInCoq.Termes]
Nbsbt_abs [constructor, in CoqInCoq.Termes]
neutral [definition, in CoqInCoq.Can]
New_axiom [constructor, in CoqInCoq.Machine]
nf_uniqueness [lemma, in CoqInCoq.Conv]
NF_Econv_Econv [lemma, in CoqInCoq.Equiv]
NF_Econv_not_is_lam [lemma, in CoqInCoq.Equiv]
nf_prod [constructor, in CoqInCoq.Equiv]
nf_sort [constructor, in CoqInCoq.Equiv]
nf_lam [constructor, in CoqInCoq.Equiv]
nf_app [constructor, in CoqInCoq.Equiv]
nf_var [constructor, in CoqInCoq.Equiv]
NF_Econv [inductive, in CoqInCoq.Equiv]
normal [definition, in CoqInCoq.Termes]
Normalisation_Forte [section, in CoqInCoq.Termes]
normal_Econv_NF_conv [lemma, in CoqInCoq.Equiv]
normal_prop [lemma, in CoqInCoq.Equiv]
normal_prod_inv [lemma, in CoqInCoq.Equiv]
normal_app_inv [lemma, in CoqInCoq.Equiv]
normal_abs_inv [lemma, in CoqInCoq.Equiv]
normal_normal_prod [lemma, in CoqInCoq.Equiv]
normal_normal_app [lemma, in CoqInCoq.Equiv]
normal_normal_abs [lemma, in CoqInCoq.Equiv]
norm_body [definition, in CoqInCoq.Conv_Dec]
Not_a_fun [constructor, in CoqInCoq.Infer]
Not_a_type [constructor, in CoqInCoq.Infer]
not_Ered_Abs_sort [lemma, in CoqInCoq.Ered]
not_is_lam_Ered1 [lemma, in CoqInCoq.Equiv]
nth_class_env [lemma, in CoqInCoq.Class]
nth_sub_inf [lemma, in CoqInCoq.Types]
nth_sub_eq [lemma, in CoqInCoq.Types]
nth_sub_sup [lemma, in CoqInCoq.Types]
nth_lift_int [lemma, in CoqInCoq.Int_stab]
nth_sound [lemma, in CoqInCoq.MyList]
nth_def [definition, in CoqInCoq.MyList]
O
oi_intro [constructor, in CoqInCoq.Names]one_step_conv_exp [lemma, in CoqInCoq.Termes]
one_step_red [lemma, in CoqInCoq.Termes]
one_step_Econv_exp [lemma, in CoqInCoq.Ered]
ord_norm [definition, in CoqInCoq.Conv_Dec]
ord_norm1 [definition, in CoqInCoq.Conv_Dec]
ord_insert [inductive, in CoqInCoq.Names]
P
Papply_err [constructor, in CoqInCoq.Machine]par_red1_subst [lemma, in CoqInCoq.Termes]
par_red1_lift [lemma, in CoqInCoq.Termes]
par_red_red [lemma, in CoqInCoq.Termes]
par_red [definition, in CoqInCoq.Termes]
par_beta [constructor, in CoqInCoq.Termes]
par_red1 [inductive, in CoqInCoq.Termes]
Pcannot_delete [constructor, in CoqInCoq.Machine]
Pcontext_listing [constructor, in CoqInCoq.Machine]
Pcorrect [constructor, in CoqInCoq.Machine]
Pdb_error [constructor, in CoqInCoq.Machine]
Pdelete_axiom [constructor, in CoqInCoq.Machine]
permute_lift [lemma, in CoqInCoq.Termes]
permute_lift_rec [lemma, in CoqInCoq.Termes]
perror [inductive, in CoqInCoq.Machine]
Pexiting [constructor, in CoqInCoq.Machine]
Pexpected_type [constructor, in CoqInCoq.Machine]
Pi [definition, in CoqInCoq.Can]
Pinfered_type [constructor, in CoqInCoq.Machine]
Pkind_ill_typed [constructor, in CoqInCoq.Machine]
Plambda_kind [constructor, in CoqInCoq.Machine]
pmessage [inductive, in CoqInCoq.Machine]
Pname_clash [constructor, in CoqInCoq.Machine]
Pnew_axiom [constructor, in CoqInCoq.Machine]
Pnot_a_fun [constructor, in CoqInCoq.Machine]
Pnot_a_type [constructor, in CoqInCoq.Machine]
PROD [constructor, in CoqInCoq.Class]
Prod [constructor, in CoqInCoq.Termes]
PROD [constructor, in CoqInCoq.Expr]
prod_par_red [constructor, in CoqInCoq.Termes]
prod_red_r [constructor, in CoqInCoq.Termes]
prod_red_l [constructor, in CoqInCoq.Termes]
prod_inhabitants [lemma, in CoqInCoq.Consistency]
prod_not_atom [lemma, in CoqInCoq.Consistency]
PROP [constructor, in CoqInCoq.Class]
prop [constructor, in CoqInCoq.Termes]
prt_names [definition, in CoqInCoq.Names]
Ptype_error [constructor, in CoqInCoq.Machine]
ptype_error [inductive, in CoqInCoq.Machine]
Punbound_vars [constructor, in CoqInCoq.Machine]
Punder [constructor, in CoqInCoq.Machine]
Q
QUIT [constructor, in CoqInCoq.Machine]R
red [inductive, in CoqInCoq.Termes]red_red1_ord_norm [lemma, in CoqInCoq.Conv_Dec]
red_normal [lemma, in CoqInCoq.Termes]
red_sort_mem [lemma, in CoqInCoq.Termes]
red_par_red [lemma, in CoqInCoq.Termes]
red_conv [lemma, in CoqInCoq.Termes]
red_sort_sort [lemma, in CoqInCoq.Termes]
red_prod_prod [lemma, in CoqInCoq.Termes]
red_red_prod [lemma, in CoqInCoq.Termes]
red_red_abs [lemma, in CoqInCoq.Termes]
red_red_app [lemma, in CoqInCoq.Termes]
red_to_prod [definition, in CoqInCoq.Infer]
red_to_sort [definition, in CoqInCoq.Infer]
red_Ered [lemma, in CoqInCoq.Ered]
red_item [lemma, in CoqInCoq.Types]
red_int_typ [lemma, in CoqInCoq.Int_stab]
red1 [inductive, in CoqInCoq.Termes]
red1_par_red1 [lemma, in CoqInCoq.Termes]
red1_subst_l [lemma, in CoqInCoq.Termes]
red1_subst_r [lemma, in CoqInCoq.Termes]
red1_lift [lemma, in CoqInCoq.Termes]
red1_red_ind [lemma, in CoqInCoq.Termes]
red1_Ered1 [lemma, in CoqInCoq.Ered]
red1_env_tl [constructor, in CoqInCoq.Types]
red1_env_hd [constructor, in CoqInCoq.Types]
red1_in_env [inductive, in CoqInCoq.Types]
Ref [constructor, in CoqInCoq.Termes]
REF [constructor, in CoqInCoq.Expr]
refl_loose_eqc_cls [lemma, in CoqInCoq.Class]
refl_loose_eqc [lemma, in CoqInCoq.Class]
refl_par_red1 [lemma, in CoqInCoq.Termes]
refl_conv [constructor, in CoqInCoq.Termes]
refl_red [constructor, in CoqInCoq.Termes]
refl_Epar_red1 [lemma, in CoqInCoq.Ered]
refl_equiv_env [lemma, in CoqInCoq.Equiv]
refl_NF_Econv [lemma, in CoqInCoq.Equiv]
ref_par_red [constructor, in CoqInCoq.Termes]
rmv [definition, in CoqInCoq.Names]
S
Sbtrm_nobind [constructor, in CoqInCoq.Termes]Sbtrm_bind [constructor, in CoqInCoq.Termes]
set [constructor, in CoqInCoq.Termes]
shift_intt [definition, in CoqInCoq.Int_term]
simpl_subst [lemma, in CoqInCoq.Termes]
simpl_subst_rec [lemma, in CoqInCoq.Termes]
simpl_lift [lemma, in CoqInCoq.Termes]
simpl_lift_rec [lemma, in CoqInCoq.Termes]
skel [inductive, in CoqInCoq.Class]
skel_sound [lemma, in CoqInCoq.Class]
skel_int [definition, in CoqInCoq.Int_typ]
sn [definition, in CoqInCoq.Termes]
sn_subst [lemma, in CoqInCoq.Termes]
sn_prod [lemma, in CoqInCoq.Termes]
sn_red_sn [lemma, in CoqInCoq.Termes]
sort [inductive, in CoqInCoq.Termes]
sort_par_red [constructor, in CoqInCoq.Termes]
sort_level_ind [lemma, in CoqInCoq.Termes]
sort_not_atom [lemma, in CoqInCoq.Consistency]
Srt [constructor, in CoqInCoq.Termes]
SRT [constructor, in CoqInCoq.Expr]
state [record, in CoqInCoq.Machine]
state_ext [record, in CoqInCoq.Machine]
strip_lemma [lemma, in CoqInCoq.Conv]
strip_lemma_Epar_red1 [lemma, in CoqInCoq.Ered]
Strong_Norm [library]
str_confluence_par_red1 [lemma, in CoqInCoq.Conv]
str_confluent [definition, in CoqInCoq.Conv]
str_confluence_Epar_red1 [lemma, in CoqInCoq.Ered]
str_norm [lemma, in CoqInCoq.Strong_Norm]
subject_reduction [lemma, in CoqInCoq.Types]
subj_red [lemma, in CoqInCoq.Types]
subst [definition, in CoqInCoq.Termes]
substitution [lemma, in CoqInCoq.Types]
subst_ref_eq [lemma, in CoqInCoq.Termes]
subst_ref_gt [lemma, in CoqInCoq.Termes]
subst_ref_lt [lemma, in CoqInCoq.Termes]
subst_rec [definition, in CoqInCoq.Termes]
subst_Ered1_r [lemma, in CoqInCoq.Ered]
subst_rec_Ered1_r [lemma, in CoqInCoq.Ered]
subst_int_typ [lemma, in CoqInCoq.Int_stab]
subterm [inductive, in CoqInCoq.Termes]
subterm_ord_norm [lemma, in CoqInCoq.Conv_Dec]
subterm_sn [lemma, in CoqInCoq.Termes]
subterm_prod [lemma, in CoqInCoq.Termes]
subterm_abs [lemma, in CoqInCoq.Termes]
subt_nobind [inductive, in CoqInCoq.Termes]
subt_bind [inductive, in CoqInCoq.Termes]
sub_S [constructor, in CoqInCoq.Types]
sub_O [constructor, in CoqInCoq.Types]
sub_in_env [inductive, in CoqInCoq.Types]
Syf_db_failed [constructor, in CoqInCoq.Machine]
sym_conv [lemma, in CoqInCoq.Termes]
sym_Econv [lemma, in CoqInCoq.Ered]
sym_NF_Econv [lemma, in CoqInCoq.Equiv]
synthesis [definition, in CoqInCoq.Machine]
synthesis_trans [inductive, in CoqInCoq.Machine]
synth_answer [definition, in CoqInCoq.Machine]
synth_deterministic [lemma, in CoqInCoq.Machine]
synth_no_confusion [lemma, in CoqInCoq.Machine]
synth_error [inductive, in CoqInCoq.Machine]
Sy_quit [constructor, in CoqInCoq.Machine]
Sy_list [constructor, in CoqInCoq.Machine]
Sy_delete [constructor, in CoqInCoq.Machine]
Sy_axiom [constructor, in CoqInCoq.Machine]
Sy_check [constructor, in CoqInCoq.Machine]
Sy_infer [constructor, in CoqInCoq.Machine]
T
TCs [constructor, in CoqInCoq.ListType]tc_T [constructor, in CoqInCoq.Class]
tc_t [constructor, in CoqInCoq.Class]
term [inductive, in CoqInCoq.Termes]
Termes [section, in CoqInCoq.Termes]
Termes [library]
term_of_expr [definition, in CoqInCoq.Expr]
term_expr_equiv [inductive, in CoqInCoq.Expr]
Te_int [constructor, in CoqInCoq.Machine]
Te_sy [constructor, in CoqInCoq.Machine]
Te_cannot_delete [constructor, in CoqInCoq.Machine]
Te_type_error [constructor, in CoqInCoq.Machine]
Te_name_clash [constructor, in CoqInCoq.Machine]
Tfaf_cs [constructor, in CoqInCoq.ListType]
Tfaf_nil [constructor, in CoqInCoq.ListType]
Tfa_cs [constructor, in CoqInCoq.ListType]
Tfa_nil [constructor, in CoqInCoq.ListType]
Tfa2_cs [constructor, in CoqInCoq.ListType]
Tfa2_nil [constructor, in CoqInCoq.ListType]
Tfor_all2 [inductive, in CoqInCoq.ListType]
Tfor_all_fold [inductive, in CoqInCoq.ListType]
Tfor_all [inductive, in CoqInCoq.ListType]
thinning [lemma, in CoqInCoq.Types]
thinning_n [lemma, in CoqInCoq.Types]
TIns [inductive, in CoqInCoq.ListType]
Tins_eq [lemma, in CoqInCoq.ListType]
Tins_gt [lemma, in CoqInCoq.ListType]
Tins_le [lemma, in CoqInCoq.ListType]
TIns_tl [constructor, in CoqInCoq.ListType]
TIns_hd [constructor, in CoqInCoq.ListType]
TList [inductive, in CoqInCoq.ListType]
TListes [section, in CoqInCoq.ListType]
TListes.A [variable, in CoqInCoq.ListType]
TList_iter [definition, in CoqInCoq.ListType]
Tmap [definition, in CoqInCoq.ListType]
Tm_exit [constructor, in CoqInCoq.Machine]
Tm_listing [constructor, in CoqInCoq.Machine]
Tm_delete [constructor, in CoqInCoq.Machine]
Tm_axiom [constructor, in CoqInCoq.Machine]
Tm_check [constructor, in CoqInCoq.Machine]
Tm_infer [constructor, in CoqInCoq.Machine]
TNl [constructor, in CoqInCoq.ListType]
Tnth_def [definition, in CoqInCoq.ListType]
top_trans_error_no_confusion [lemma, in CoqInCoq.Machine]
top_error [inductive, in CoqInCoq.Machine]
Top_int [constructor, in CoqInCoq.Machine]
top_trans [inductive, in CoqInCoq.Machine]
Tpe_apply_err [constructor, in CoqInCoq.Machine]
Tpe_not_a_fun [constructor, in CoqInCoq.Machine]
Tpe_not_a_type [constructor, in CoqInCoq.Machine]
Tpe_lam_kind [constructor, in CoqInCoq.Machine]
Tpe_db_error [constructor, in CoqInCoq.Machine]
Tpe_is_kind [constructor, in CoqInCoq.Machine]
Tpe_exp_type [constructor, in CoqInCoq.Machine]
Tpe_under [constructor, in CoqInCoq.Machine]
transition [inductive, in CoqInCoq.Machine]
transl_error [definition, in CoqInCoq.Machine]
transl_ty_error [definition, in CoqInCoq.Machine]
transl_message [definition, in CoqInCoq.Machine]
transl_err [inductive, in CoqInCoq.Machine]
transl_type_error [inductive, in CoqInCoq.Machine]
transl_msg [inductive, in CoqInCoq.Machine]
transl_name [inductive, in CoqInCoq.Expr]
trans_error_no_confusion [lemma, in CoqInCoq.Machine]
trans_conv_conv [lemma, in CoqInCoq.Termes]
trans_red_red [lemma, in CoqInCoq.Termes]
trans_conv_exp [constructor, in CoqInCoq.Termes]
trans_conv_red [constructor, in CoqInCoq.Termes]
trans_red [constructor, in CoqInCoq.Termes]
trans_Econv_Econv [lemma, in CoqInCoq.Ered]
trans_Ered_Ered [lemma, in CoqInCoq.Ered]
trans_NF_Econv_NF_Econv [lemma, in CoqInCoq.Equiv]
Trm [constructor, in CoqInCoq.Class]
trm_in_int [inductive, in CoqInCoq.Strong_Norm]
trunc [inductive, in CoqInCoq.MyList]
trunc_S [constructor, in CoqInCoq.MyList]
trunc_O [constructor, in CoqInCoq.MyList]
Tr_quit [constructor, in CoqInCoq.Machine]
Tr_list [constructor, in CoqInCoq.Machine]
Tr_delete [constructor, in CoqInCoq.Machine]
Tr_axiom [constructor, in CoqInCoq.Machine]
Tr_check [constructor, in CoqInCoq.Machine]
Tr_infer [constructor, in CoqInCoq.Machine]
tr_tl [constructor, in CoqInCoq.Expr]
tr_hd [constructor, in CoqInCoq.Expr]
tr_nil [constructor, in CoqInCoq.Expr]
TSmap [definition, in CoqInCoq.ListType]
TTrunc [inductive, in CoqInCoq.ListType]
Ttr_S [constructor, in CoqInCoq.ListType]
Ttr_O [constructor, in CoqInCoq.ListType]
Typ [constructor, in CoqInCoq.Class]
typ [inductive, in CoqInCoq.Types]
Typage [section, in CoqInCoq.ETypes]
Typage [section, in CoqInCoq.Types]
TypeChecker [section, in CoqInCoq.Infer]
Types [library]
Type_error [constructor, in CoqInCoq.Machine]
type_error [inductive, in CoqInCoq.Infer]
type_reduction [lemma, in CoqInCoq.Types]
type_free_db [lemma, in CoqInCoq.Types]
type_kind_not_conv [lemma, in CoqInCoq.Types]
type_case [lemma, in CoqInCoq.Types]
type_prop_set [lemma, in CoqInCoq.Types]
type_conv [constructor, in CoqInCoq.Types]
type_prod [constructor, in CoqInCoq.Types]
type_app [constructor, in CoqInCoq.Types]
type_abs [constructor, in CoqInCoq.Types]
type_var [constructor, in CoqInCoq.Types]
type_set [constructor, in CoqInCoq.Types]
type_prop [constructor, in CoqInCoq.Types]
type_sn [lemma, in CoqInCoq.Strong_Norm]
typ_Etyp [lemma, in CoqInCoq.ETypes]
typ_cls [inductive, in CoqInCoq.Class]
typ_skel [definition, in CoqInCoq.Class]
typ_conv_conv [lemma, in CoqInCoq.Types]
typ_red_env [lemma, in CoqInCoq.Types]
typ_unique [lemma, in CoqInCoq.Types]
typ_sub_weak [lemma, in CoqInCoq.Types]
typ_weak_weak [lemma, in CoqInCoq.Types]
typ_mem_kind [lemma, in CoqInCoq.Types]
typ_inversion [lemma, in CoqInCoq.Types]
typ_wf [lemma, in CoqInCoq.Types]
typ_free_db [lemma, in CoqInCoq.Types]
typ_sort_Econv_Econv [lemma, in CoqInCoq.Equiv]
typ_is_nf [lemma, in CoqInCoq.Equiv]
U
undef_vars_prod [lemma, in CoqInCoq.Expr]undef_vars_app [lemma, in CoqInCoq.Expr]
undef_vars_abs [lemma, in CoqInCoq.Expr]
undef_vars_incl [lemma, in CoqInCoq.Expr]
undef_vars [definition, in CoqInCoq.Expr]
Under [constructor, in CoqInCoq.Infer]
unique_alpha [lemma, in CoqInCoq.Expr]
V
var_in_cand [lemma, in CoqInCoq.Can]var_of_nat [definition, in CoqInCoq.Names]
W
wf [inductive, in CoqInCoq.Types]wf_ord_norm [lemma, in CoqInCoq.Conv_Dec]
wf_ord_norm1 [lemma, in CoqInCoq.Conv_Dec]
wf_subterm [lemma, in CoqInCoq.Conv_Dec]
wf_sort_lift [lemma, in CoqInCoq.Types]
wf_sort [lemma, in CoqInCoq.Types]
wf_var [constructor, in CoqInCoq.Types]
wf_nil [constructor, in CoqInCoq.Types]
wf_oi [lemma, in CoqInCoq.Names]
Variable Index
L
Listes.A [in CoqInCoq.MyList]Listes.eq_dec [in CoqInCoq.MyList]
Listes.List [in CoqInCoq.MyList]
T
TListes.A [in CoqInCoq.ListType]Library Index
C
CanClass
Consistency
Conv
Conv_Dec
E
EquivEred
ETypes
Expr
I
InferInt_typ
Int_stab
Int_term
L
ListTypeM
MachineMlTypes
MyList
N
NamesS
Strong_NormT
TermesTypes
Lemma Index
A
Abs_sound [in CoqInCoq.Can]adapt_int_inv [in CoqInCoq.Int_stab]
applist_assoc [in CoqInCoq.Consistency]
atom_inhabitants [in CoqInCoq.Consistency]
atom_reduction [in CoqInCoq.Consistency]
C
cand_sn [in CoqInCoq.Can]cand_sat [in CoqInCoq.Can]
chk_error_no_type [in CoqInCoq.Infer]
church_rosser [in CoqInCoq.Conv]
class_red [in CoqInCoq.Class]
class_sound [in CoqInCoq.Class]
class_subst [in CoqInCoq.Class]
class_trm [in CoqInCoq.Class]
class_typ_ord [in CoqInCoq.Class]
class_typ [in CoqInCoq.Class]
class_knd [in CoqInCoq.Class]
class_env_trunc [in CoqInCoq.Class]
clos_red_star [in CoqInCoq.Can]
cl_term_conv [in CoqInCoq.Class]
cl_term_red [in CoqInCoq.Class]
cl_term_red1 [in CoqInCoq.Class]
cl_term_sound [in CoqInCoq.Class]
cl_term_subst [in CoqInCoq.Class]
cl_trunc [in CoqInCoq.Class]
cl_term_lift [in CoqInCoq.Class]
coc_consistency [in CoqInCoq.Consistency]
coc_consistency_nf [in CoqInCoq.Consistency]
commut_case [in CoqInCoq.Class]
commut_red1_subterm [in CoqInCoq.Termes]
commut_lift_subst [in CoqInCoq.Termes]
commut_lift_subst_rec [in CoqInCoq.Termes]
confluence_red [in CoqInCoq.Conv]
confluence_par_red [in CoqInCoq.Conv]
confluence_Ered [in CoqInCoq.Ered]
confluence_Epar_red [in CoqInCoq.Ered]
conv_sort_prod [in CoqInCoq.Conv]
conv_kind_prop [in CoqInCoq.Conv]
conv_sort [in CoqInCoq.Conv]
conv_conv_subst [in CoqInCoq.Termes]
conv_conv_lift [in CoqInCoq.Termes]
conv_conv_prod [in CoqInCoq.Termes]
conv_Econv [in CoqInCoq.Ered]
conv_int_typ [in CoqInCoq.Int_stab]
conv_prod_atom [in CoqInCoq.Consistency]
conv_sort_atom [in CoqInCoq.Consistency]
D
dangerous_int_injection [in CoqInCoq.MlTypes]decide_typ [in CoqInCoq.Infer]
decide_wf [in CoqInCoq.Infer]
decl_err_not_wf [in CoqInCoq.Infer]
def_inv [in CoqInCoq.Can]
def_can_cr [in CoqInCoq.Can]
def_intt_id [in CoqInCoq.Strong_Norm]
def_adapt [in CoqInCoq.Strong_Norm]
def_intp_can [in CoqInCoq.Strong_Norm]
distr_subst [in CoqInCoq.Termes]
distr_subst_rec [in CoqInCoq.Termes]
distr_lift_subst [in CoqInCoq.Termes]
distr_lift_subst_rec [in CoqInCoq.Termes]
E
Econv_Econv_subst [in CoqInCoq.Ered]Econv_Econv_lift [in CoqInCoq.Ered]
Econv_Type_abs [in CoqInCoq.Ered]
Econv_abs [in CoqInCoq.Ered]
Econv_sort_prod [in CoqInCoq.Ered]
Econv_Econv_app [in CoqInCoq.Ered]
Econv_Econv_prod [in CoqInCoq.Ered]
Econv_church_rosser [in CoqInCoq.Ered]
EConv_Conv [in CoqInCoq.Equiv]
Econv_eq [in CoqInCoq.Equiv]
Epar_red_Ered [in CoqInCoq.Ered]
Epar_red1_subst [in CoqInCoq.Ered]
Epar_red1_lift [in CoqInCoq.Ered]
Epar_red1_Epar_red [in CoqInCoq.Ered]
equiv_no_undef [in CoqInCoq.Expr]
equiv_unique [in CoqInCoq.Expr]
equiv_free_db [in CoqInCoq.Expr]
equiv_env_item [in CoqInCoq.Equiv]
EQ_skel [in CoqInCoq.Class]
eq_can_Pi [in CoqInCoq.Can]
eq_cand_incl [in CoqInCoq.Can]
eq_can_trans [in CoqInCoq.Can]
eq_can_sym [in CoqInCoq.Can]
eq_can_extr [in CoqInCoq.Int_typ]
Ered_sort_mem [in CoqInCoq.Ered]
Ered_sort_mem2 [in CoqInCoq.Ered]
Ered_prod_prod [in CoqInCoq.Ered]
Ered_Enormal [in CoqInCoq.Ered]
Ered_Econv [in CoqInCoq.Ered]
Ered_Ered_prod [in CoqInCoq.Ered]
Ered_Ered_abs [in CoqInCoq.Ered]
Ered_Ered_app [in CoqInCoq.Ered]
Ered_Epar_red [in CoqInCoq.Ered]
Ered_normal_NF_Econv [in CoqInCoq.Equiv]
Ered1_sort_mem [in CoqInCoq.Ered]
Ered1_Ered_ind [in CoqInCoq.Ered]
Ered1_subst_l [in CoqInCoq.Ered]
Ered1_subst_r [in CoqInCoq.Ered]
Ered1_lift [in CoqInCoq.Ered]
Ered1_Epar_red1 [in CoqInCoq.Ered]
Ered1_normal_NF_Econv [in CoqInCoq.Equiv]
Ered1_normal_normal [in CoqInCoq.Equiv]
Etype_prop_set [in CoqInCoq.ETypes]
Etyp_mem_kind [in CoqInCoq.ETypes]
Etyp_inversion [in CoqInCoq.ETypes]
Etyp_Ewf [in CoqInCoq.ETypes]
Etyp_free_db [in CoqInCoq.ETypes]
Etyp_typ [in CoqInCoq.Equiv]
Etyp_NF_Econv_Econv [in CoqInCoq.Equiv]
Ewf_sort [in CoqInCoq.ETypes]
expln_wf [in CoqInCoq.Infer]
extr_eq [in CoqInCoq.Int_typ]
F
first_item_unique [in CoqInCoq.MyList]first_item_is_item [in CoqInCoq.MyList]
fun_item [in CoqInCoq.MyList]
fv_ext [in CoqInCoq.Names]
H
hnf_proofs_sound [in CoqInCoq.Consistency]I
id_int_term [in CoqInCoq.Strong_Norm]iki_K [in CoqInCoq.Int_typ]
incl_app_sym [in CoqInCoq.MyList]
inf_error_no_type [in CoqInCoq.Infer]
inj_var_of_nat [in CoqInCoq.Names]
ins_item_lt [in CoqInCoq.Types]
ins_item_ge [in CoqInCoq.Types]
ins_eq [in CoqInCoq.MyList]
ins_gt [in CoqInCoq.MyList]
ins_le [in CoqInCoq.MyList]
ins_int_inv [in CoqInCoq.Int_typ]
ins_in_cls [in CoqInCoq.Int_typ]
int_term_subst [in CoqInCoq.Int_term]
int_typ_red1 [in CoqInCoq.Int_stab]
int_cons_equal [in CoqInCoq.Int_stab]
int_var_sound_lift [in CoqInCoq.Int_stab]
int_typ_cr [in CoqInCoq.Int_stab]
int_equiv_int_typ [in CoqInCoq.Int_stab]
int_eq_can_cls [in CoqInCoq.Int_typ]
int_inv_int_eq_can [in CoqInCoq.Int_typ]
int_sound [in CoqInCoq.Strong_Norm]
inv_Etyp_Econv_kind [in CoqInCoq.ETypes]
inv_Etyp_prod [in CoqInCoq.ETypes]
inv_Etyp_app [in CoqInCoq.ETypes]
inv_Etyp_abs [in CoqInCoq.ETypes]
inv_Etyp_ref [in CoqInCoq.ETypes]
inv_Etyp_set [in CoqInCoq.ETypes]
inv_Etyp_prop [in CoqInCoq.ETypes]
inv_Etyp_kind [in CoqInCoq.ETypes]
inv_Etype_Econv [in CoqInCoq.ETypes]
inv_conv_prod_r [in CoqInCoq.Conv]
inv_conv_prod_l [in CoqInCoq.Conv]
inv_par_red_abs [in CoqInCoq.Termes]
inv_Ered_Abs [in CoqInCoq.Ered]
inv_Econv_prod_r [in CoqInCoq.Ered]
inv_Econv_prod_l [in CoqInCoq.Ered]
inv_Epar_red_abs [in CoqInCoq.Ered]
inv_typ_conv_kind [in CoqInCoq.Types]
inv_typ_prod [in CoqInCoq.Types]
inv_typ_app [in CoqInCoq.Types]
inv_typ_abs [in CoqInCoq.Types]
inv_typ_ref [in CoqInCoq.Types]
inv_typ_set [in CoqInCoq.Types]
inv_typ_prop [in CoqInCoq.Types]
inv_typ_kind [in CoqInCoq.Types]
inv_type_conv [in CoqInCoq.Types]
inv_nth_cs [in CoqInCoq.MyList]
inv_nth_nl [in CoqInCoq.MyList]
inv_typ_applist_head [in CoqInCoq.Consistency]
In_app [in CoqInCoq.MyList]
is_can_Pi [in CoqInCoq.Can]
is_can_prop [in CoqInCoq.Can]
is_can_coerce [in CoqInCoq.Int_typ]
is_atom_app [in CoqInCoq.Consistency]
item_trunc [in CoqInCoq.MyList]
L
lift_rec0 [in CoqInCoq.Termes]lift_ref_lt [in CoqInCoq.Termes]
lift_ref_ge [in CoqInCoq.Termes]
lift_int_typ [in CoqInCoq.Int_stab]
lift0 [in CoqInCoq.Termes]
loose_eqc_stable [in CoqInCoq.Class]
loose_eqc_trans [in CoqInCoq.Class]
M
mem_sort_subst [in CoqInCoq.Termes]mem_sort_lift [in CoqInCoq.Termes]
mem_sort2_mem_sort [in CoqInCoq.Ered]
mem_sort2_subst [in CoqInCoq.Ered]
mem_sort2_lift [in CoqInCoq.Ered]
N
name_unique_first [in CoqInCoq.Names]nf_uniqueness [in CoqInCoq.Conv]
NF_Econv_Econv [in CoqInCoq.Equiv]
NF_Econv_not_is_lam [in CoqInCoq.Equiv]
normal_Econv_NF_conv [in CoqInCoq.Equiv]
normal_prop [in CoqInCoq.Equiv]
normal_prod_inv [in CoqInCoq.Equiv]
normal_app_inv [in CoqInCoq.Equiv]
normal_abs_inv [in CoqInCoq.Equiv]
normal_normal_prod [in CoqInCoq.Equiv]
normal_normal_app [in CoqInCoq.Equiv]
normal_normal_abs [in CoqInCoq.Equiv]
not_Ered_Abs_sort [in CoqInCoq.Ered]
not_is_lam_Ered1 [in CoqInCoq.Equiv]
nth_class_env [in CoqInCoq.Class]
nth_sub_inf [in CoqInCoq.Types]
nth_sub_eq [in CoqInCoq.Types]
nth_sub_sup [in CoqInCoq.Types]
nth_lift_int [in CoqInCoq.Int_stab]
nth_sound [in CoqInCoq.MyList]
O
one_step_conv_exp [in CoqInCoq.Termes]one_step_red [in CoqInCoq.Termes]
one_step_Econv_exp [in CoqInCoq.Ered]
P
par_red1_subst [in CoqInCoq.Termes]par_red1_lift [in CoqInCoq.Termes]
par_red_red [in CoqInCoq.Termes]
permute_lift [in CoqInCoq.Termes]
permute_lift_rec [in CoqInCoq.Termes]
prod_inhabitants [in CoqInCoq.Consistency]
prod_not_atom [in CoqInCoq.Consistency]
R
red_red1_ord_norm [in CoqInCoq.Conv_Dec]red_normal [in CoqInCoq.Termes]
red_sort_mem [in CoqInCoq.Termes]
red_par_red [in CoqInCoq.Termes]
red_conv [in CoqInCoq.Termes]
red_sort_sort [in CoqInCoq.Termes]
red_prod_prod [in CoqInCoq.Termes]
red_red_prod [in CoqInCoq.Termes]
red_red_abs [in CoqInCoq.Termes]
red_red_app [in CoqInCoq.Termes]
red_Ered [in CoqInCoq.Ered]
red_item [in CoqInCoq.Types]
red_int_typ [in CoqInCoq.Int_stab]
red1_par_red1 [in CoqInCoq.Termes]
red1_subst_l [in CoqInCoq.Termes]
red1_subst_r [in CoqInCoq.Termes]
red1_lift [in CoqInCoq.Termes]
red1_red_ind [in CoqInCoq.Termes]
red1_Ered1 [in CoqInCoq.Ered]
refl_loose_eqc_cls [in CoqInCoq.Class]
refl_loose_eqc [in CoqInCoq.Class]
refl_par_red1 [in CoqInCoq.Termes]
refl_Epar_red1 [in CoqInCoq.Ered]
refl_equiv_env [in CoqInCoq.Equiv]
refl_NF_Econv [in CoqInCoq.Equiv]
S
simpl_subst [in CoqInCoq.Termes]simpl_subst_rec [in CoqInCoq.Termes]
simpl_lift [in CoqInCoq.Termes]
simpl_lift_rec [in CoqInCoq.Termes]
skel_sound [in CoqInCoq.Class]
sn_subst [in CoqInCoq.Termes]
sn_prod [in CoqInCoq.Termes]
sn_red_sn [in CoqInCoq.Termes]
sort_level_ind [in CoqInCoq.Termes]
sort_not_atom [in CoqInCoq.Consistency]
strip_lemma [in CoqInCoq.Conv]
strip_lemma_Epar_red1 [in CoqInCoq.Ered]
str_confluence_par_red1 [in CoqInCoq.Conv]
str_confluence_Epar_red1 [in CoqInCoq.Ered]
str_norm [in CoqInCoq.Strong_Norm]
subject_reduction [in CoqInCoq.Types]
subj_red [in CoqInCoq.Types]
substitution [in CoqInCoq.Types]
subst_ref_eq [in CoqInCoq.Termes]
subst_ref_gt [in CoqInCoq.Termes]
subst_ref_lt [in CoqInCoq.Termes]
subst_Ered1_r [in CoqInCoq.Ered]
subst_rec_Ered1_r [in CoqInCoq.Ered]
subst_int_typ [in CoqInCoq.Int_stab]
subterm_ord_norm [in CoqInCoq.Conv_Dec]
subterm_sn [in CoqInCoq.Termes]
subterm_prod [in CoqInCoq.Termes]
subterm_abs [in CoqInCoq.Termes]
sym_conv [in CoqInCoq.Termes]
sym_Econv [in CoqInCoq.Ered]
sym_NF_Econv [in CoqInCoq.Equiv]
synth_deterministic [in CoqInCoq.Machine]
synth_no_confusion [in CoqInCoq.Machine]
T
thinning [in CoqInCoq.Types]thinning_n [in CoqInCoq.Types]
Tins_eq [in CoqInCoq.ListType]
Tins_gt [in CoqInCoq.ListType]
Tins_le [in CoqInCoq.ListType]
top_trans_error_no_confusion [in CoqInCoq.Machine]
trans_error_no_confusion [in CoqInCoq.Machine]
trans_conv_conv [in CoqInCoq.Termes]
trans_red_red [in CoqInCoq.Termes]
trans_Econv_Econv [in CoqInCoq.Ered]
trans_Ered_Ered [in CoqInCoq.Ered]
trans_NF_Econv_NF_Econv [in CoqInCoq.Equiv]
type_reduction [in CoqInCoq.Types]
type_free_db [in CoqInCoq.Types]
type_kind_not_conv [in CoqInCoq.Types]
type_case [in CoqInCoq.Types]
type_prop_set [in CoqInCoq.Types]
type_sn [in CoqInCoq.Strong_Norm]
typ_Etyp [in CoqInCoq.ETypes]
typ_conv_conv [in CoqInCoq.Types]
typ_red_env [in CoqInCoq.Types]
typ_unique [in CoqInCoq.Types]
typ_sub_weak [in CoqInCoq.Types]
typ_weak_weak [in CoqInCoq.Types]
typ_mem_kind [in CoqInCoq.Types]
typ_inversion [in CoqInCoq.Types]
typ_wf [in CoqInCoq.Types]
typ_free_db [in CoqInCoq.Types]
typ_sort_Econv_Econv [in CoqInCoq.Equiv]
typ_is_nf [in CoqInCoq.Equiv]
U
undef_vars_prod [in CoqInCoq.Expr]undef_vars_app [in CoqInCoq.Expr]
undef_vars_abs [in CoqInCoq.Expr]
undef_vars_incl [in CoqInCoq.Expr]
unique_alpha [in CoqInCoq.Expr]
V
var_in_cand [in CoqInCoq.Can]W
wf_ord_norm [in CoqInCoq.Conv_Dec]wf_ord_norm1 [in CoqInCoq.Conv_Dec]
wf_subterm [in CoqInCoq.Conv_Dec]
wf_sort_lift [in CoqInCoq.Types]
wf_sort [in CoqInCoq.Types]
wf_oi [in CoqInCoq.Names]
Constructor Index
A
Abs [in CoqInCoq.Termes]ABS [in CoqInCoq.Expr]
abs_par_red [in CoqInCoq.Termes]
abs_red_r [in CoqInCoq.Termes]
abs_red_l [in CoqInCoq.Termes]
adj_T [in CoqInCoq.Class]
adj_t [in CoqInCoq.Class]
alp_prod [in CoqInCoq.Expr]
alp_app [in CoqInCoq.Expr]
alp_abs [in CoqInCoq.Expr]
alp_ref [in CoqInCoq.Expr]
alp_srt [in CoqInCoq.Expr]
App [in CoqInCoq.Termes]
APP [in CoqInCoq.Expr]
Apply_err [in CoqInCoq.Infer]
app_par_red [in CoqInCoq.Termes]
app_red_r [in CoqInCoq.Termes]
app_red_l [in CoqInCoq.Termes]
AST_QUIT [in CoqInCoq.Machine]
AST_LIST [in CoqInCoq.Machine]
AST_DELETE [in CoqInCoq.Machine]
AST_AXIOM [in CoqInCoq.Machine]
AST_CHECK [in CoqInCoq.Machine]
AST_INFER [in CoqInCoq.Machine]
AXIOM [in CoqInCoq.Machine]
B
beta [in CoqInCoq.Termes]Bsbt_prod [in CoqInCoq.Termes]
Bsbt_abs [in CoqInCoq.Termes]
C
Cannot_delete [in CoqInCoq.Machine]ca_T [in CoqInCoq.Int_stab]
ca_K [in CoqInCoq.Int_stab]
Ce_delete [in CoqInCoq.Machine]
Ce_axiom [in CoqInCoq.Machine]
Ce_decl_error [in CoqInCoq.Machine]
Ce_chk_error [in CoqInCoq.Machine]
Ce_inf_error [in CoqInCoq.Machine]
CHECK [in CoqInCoq.Machine]
Chke_exp [in CoqInCoq.Infer]
Chke_type [in CoqInCoq.Infer]
Chke_subj [in CoqInCoq.Infer]
Context_listing [in CoqInCoq.Machine]
Correct [in CoqInCoq.Machine]
D
db_prod [in CoqInCoq.Termes]db_app [in CoqInCoq.Termes]
db_abs [in CoqInCoq.Termes]
db_ref [in CoqInCoq.Termes]
db_srt [in CoqInCoq.Termes]
Db_error [in CoqInCoq.Infer]
Decax_type [in CoqInCoq.Infer]
Decax_ill [in CoqInCoq.Infer]
DELETE [in CoqInCoq.Machine]
Delete_axiom [in CoqInCoq.Machine]
E
Eabs [in CoqInCoq.Ered]Eabs_par_red [in CoqInCoq.Ered]
Eabs_red_r [in CoqInCoq.Ered]
Eabs_red_l [in CoqInCoq.Ered]
Eapp_par_red [in CoqInCoq.Ered]
Eapp_red_r [in CoqInCoq.Ered]
Eapp_red_l [in CoqInCoq.Ered]
ea_ax [in CoqInCoq.Machine]
ea_chk2 [in CoqInCoq.Machine]
ea_chk1 [in CoqInCoq.Machine]
ea_inf [in CoqInCoq.Machine]
Ebeta [in CoqInCoq.Ered]
EE_c [in CoqInCoq.Equiv]
EE_n [in CoqInCoq.Equiv]
Epar_abs [in CoqInCoq.Ered]
Epar_beta [in CoqInCoq.Ered]
Eprod_par_red [in CoqInCoq.Ered]
Eprod_red_r [in CoqInCoq.Ered]
Eprod_red_l [in CoqInCoq.Ered]
eqi_T [in CoqInCoq.Int_typ]
eqi_K [in CoqInCoq.Int_typ]
eqv_prod [in CoqInCoq.Expr]
eqv_app [in CoqInCoq.Expr]
eqv_abs [in CoqInCoq.Expr]
eqv_ref [in CoqInCoq.Expr]
eqv_srt [in CoqInCoq.Expr]
Erefl [in CoqInCoq.Ered]
Erefl_conv [in CoqInCoq.Ered]
Eref_par_red [in CoqInCoq.Ered]
Esort_par_red [in CoqInCoq.Ered]
Etrans_conv_exp [in CoqInCoq.Ered]
Etrans_conv_red [in CoqInCoq.Ered]
Etrans_red [in CoqInCoq.Ered]
Etype_Econv [in CoqInCoq.ETypes]
Etype_prod [in CoqInCoq.ETypes]
Etype_app [in CoqInCoq.ETypes]
Etype_abs [in CoqInCoq.ETypes]
Etype_var [in CoqInCoq.ETypes]
Etype_set [in CoqInCoq.ETypes]
Etype_prop [in CoqInCoq.ETypes]
ev_prod_r [in CoqInCoq.Expr]
ev_prod_l [in CoqInCoq.Expr]
ev_app_r [in CoqInCoq.Expr]
ev_app_l [in CoqInCoq.Expr]
ev_abs_r [in CoqInCoq.Expr]
ev_abs_l [in CoqInCoq.Expr]
ev_ref [in CoqInCoq.Expr]
Ewf_var [in CoqInCoq.ETypes]
Ewf_nil [in CoqInCoq.ETypes]
Exiting [in CoqInCoq.Machine]
Expected_type [in CoqInCoq.Infer]
Exp_appl_err [in CoqInCoq.Infer]
Exp_fun [in CoqInCoq.Infer]
Exp_type [in CoqInCoq.Infer]
Exp_lam_kind [in CoqInCoq.Infer]
Exp_db [in CoqInCoq.Infer]
Exp_kind [in CoqInCoq.Infer]
Exp_exp_type [in CoqInCoq.Infer]
Exp_under [in CoqInCoq.Infer]
F
fit_tl [in CoqInCoq.MyList]fit_hd [in CoqInCoq.MyList]
I
iK [in CoqInCoq.Int_typ]INFER [in CoqInCoq.Machine]
Infered_type [in CoqInCoq.Machine]
Infe_type_prod_r [in CoqInCoq.Infer]
Infe_type_prod_l [in CoqInCoq.Infer]
Infe_appl_err [in CoqInCoq.Infer]
Infe_fun [in CoqInCoq.Infer]
Infe_type_abs [in CoqInCoq.Infer]
Infe_lam_kind [in CoqInCoq.Infer]
Infe_db [in CoqInCoq.Infer]
Infe_kind [in CoqInCoq.Infer]
Infe_under [in CoqInCoq.Infer]
Infe_subt [in CoqInCoq.Infer]
insert_tl [in CoqInCoq.MyList]
insert_hd [in CoqInCoq.MyList]
ins_S [in CoqInCoq.Types]
ins_O [in CoqInCoq.Types]
int_cs [in CoqInCoq.Strong_Norm]
int_nil [in CoqInCoq.Strong_Norm]
In_tl [in CoqInCoq.MyList]
In_hd [in CoqInCoq.MyList]
iT [in CoqInCoq.Int_typ]
item_tl [in CoqInCoq.MyList]
item_hd [in CoqInCoq.MyList]
ivs_T [in CoqInCoq.Int_stab]
ivs_K [in CoqInCoq.Int_stab]
K
kind [in CoqInCoq.Termes]Kind_ill_typed [in CoqInCoq.Infer]
Knd [in CoqInCoq.Class]
L
Lambda_kind [in CoqInCoq.Infer]leqc_ord [in CoqInCoq.Class]
leqc_typ [in CoqInCoq.Class]
leqc_trm [in CoqInCoq.Class]
LIST [in CoqInCoq.Machine]
M
mem_app_r [in CoqInCoq.Termes]mem_app_l [in CoqInCoq.Termes]
mem_abs_r [in CoqInCoq.Termes]
mem_abs_l [in CoqInCoq.Termes]
mem_prod_r [in CoqInCoq.Termes]
mem_prod_l [in CoqInCoq.Termes]
mem_eq [in CoqInCoq.Termes]
mem_app_r2 [in CoqInCoq.Ered]
mem_app_l2 [in CoqInCoq.Ered]
mem_abs_r2 [in CoqInCoq.Ered]
mem_prod_r2 [in CoqInCoq.Ered]
mem_prod_l2 [in CoqInCoq.Ered]
mem_eq2 [in CoqInCoq.Ered]
N
Name_clash [in CoqInCoq.Machine]Nbsbt_prod [in CoqInCoq.Termes]
Nbsbt_app_r [in CoqInCoq.Termes]
Nbsbt_app_l [in CoqInCoq.Termes]
Nbsbt_abs [in CoqInCoq.Termes]
New_axiom [in CoqInCoq.Machine]
nf_prod [in CoqInCoq.Equiv]
nf_sort [in CoqInCoq.Equiv]
nf_lam [in CoqInCoq.Equiv]
nf_app [in CoqInCoq.Equiv]
nf_var [in CoqInCoq.Equiv]
Not_a_fun [in CoqInCoq.Infer]
Not_a_type [in CoqInCoq.Infer]
O
oi_intro [in CoqInCoq.Names]P
Papply_err [in CoqInCoq.Machine]par_beta [in CoqInCoq.Termes]
Pcannot_delete [in CoqInCoq.Machine]
Pcontext_listing [in CoqInCoq.Machine]
Pcorrect [in CoqInCoq.Machine]
Pdb_error [in CoqInCoq.Machine]
Pdelete_axiom [in CoqInCoq.Machine]
Pexiting [in CoqInCoq.Machine]
Pexpected_type [in CoqInCoq.Machine]
Pinfered_type [in CoqInCoq.Machine]
Pkind_ill_typed [in CoqInCoq.Machine]
Plambda_kind [in CoqInCoq.Machine]
Pname_clash [in CoqInCoq.Machine]
Pnew_axiom [in CoqInCoq.Machine]
Pnot_a_fun [in CoqInCoq.Machine]
Pnot_a_type [in CoqInCoq.Machine]
PROD [in CoqInCoq.Class]
Prod [in CoqInCoq.Termes]
PROD [in CoqInCoq.Expr]
prod_par_red [in CoqInCoq.Termes]
prod_red_r [in CoqInCoq.Termes]
prod_red_l [in CoqInCoq.Termes]
PROP [in CoqInCoq.Class]
prop [in CoqInCoq.Termes]
Ptype_error [in CoqInCoq.Machine]
Punbound_vars [in CoqInCoq.Machine]
Punder [in CoqInCoq.Machine]
Q
QUIT [in CoqInCoq.Machine]R
red1_env_tl [in CoqInCoq.Types]red1_env_hd [in CoqInCoq.Types]
Ref [in CoqInCoq.Termes]
REF [in CoqInCoq.Expr]
refl_conv [in CoqInCoq.Termes]
refl_red [in CoqInCoq.Termes]
ref_par_red [in CoqInCoq.Termes]
S
Sbtrm_nobind [in CoqInCoq.Termes]Sbtrm_bind [in CoqInCoq.Termes]
set [in CoqInCoq.Termes]
sort_par_red [in CoqInCoq.Termes]
Srt [in CoqInCoq.Termes]
SRT [in CoqInCoq.Expr]
sub_S [in CoqInCoq.Types]
sub_O [in CoqInCoq.Types]
Syf_db_failed [in CoqInCoq.Machine]
Sy_quit [in CoqInCoq.Machine]
Sy_list [in CoqInCoq.Machine]
Sy_delete [in CoqInCoq.Machine]
Sy_axiom [in CoqInCoq.Machine]
Sy_check [in CoqInCoq.Machine]
Sy_infer [in CoqInCoq.Machine]
T
TCs [in CoqInCoq.ListType]tc_T [in CoqInCoq.Class]
tc_t [in CoqInCoq.Class]
Te_int [in CoqInCoq.Machine]
Te_sy [in CoqInCoq.Machine]
Te_cannot_delete [in CoqInCoq.Machine]
Te_type_error [in CoqInCoq.Machine]
Te_name_clash [in CoqInCoq.Machine]
Tfaf_cs [in CoqInCoq.ListType]
Tfaf_nil [in CoqInCoq.ListType]
Tfa_cs [in CoqInCoq.ListType]
Tfa_nil [in CoqInCoq.ListType]
Tfa2_cs [in CoqInCoq.ListType]
Tfa2_nil [in CoqInCoq.ListType]
TIns_tl [in CoqInCoq.ListType]
TIns_hd [in CoqInCoq.ListType]
Tm_exit [in CoqInCoq.Machine]
Tm_listing [in CoqInCoq.Machine]
Tm_delete [in CoqInCoq.Machine]
Tm_axiom [in CoqInCoq.Machine]
Tm_check [in CoqInCoq.Machine]
Tm_infer [in CoqInCoq.Machine]
TNl [in CoqInCoq.ListType]
Top_int [in CoqInCoq.Machine]
Tpe_apply_err [in CoqInCoq.Machine]
Tpe_not_a_fun [in CoqInCoq.Machine]
Tpe_not_a_type [in CoqInCoq.Machine]
Tpe_lam_kind [in CoqInCoq.Machine]
Tpe_db_error [in CoqInCoq.Machine]
Tpe_is_kind [in CoqInCoq.Machine]
Tpe_exp_type [in CoqInCoq.Machine]
Tpe_under [in CoqInCoq.Machine]
trans_conv_exp [in CoqInCoq.Termes]
trans_conv_red [in CoqInCoq.Termes]
trans_red [in CoqInCoq.Termes]
Trm [in CoqInCoq.Class]
trunc_S [in CoqInCoq.MyList]
trunc_O [in CoqInCoq.MyList]
Tr_quit [in CoqInCoq.Machine]
Tr_list [in CoqInCoq.Machine]
Tr_delete [in CoqInCoq.Machine]
Tr_axiom [in CoqInCoq.Machine]
Tr_check [in CoqInCoq.Machine]
Tr_infer [in CoqInCoq.Machine]
tr_tl [in CoqInCoq.Expr]
tr_hd [in CoqInCoq.Expr]
tr_nil [in CoqInCoq.Expr]
Ttr_S [in CoqInCoq.ListType]
Ttr_O [in CoqInCoq.ListType]
Typ [in CoqInCoq.Class]
Type_error [in CoqInCoq.Machine]
type_conv [in CoqInCoq.Types]
type_prod [in CoqInCoq.Types]
type_app [in CoqInCoq.Types]
type_abs [in CoqInCoq.Types]
type_var [in CoqInCoq.Types]
type_set [in CoqInCoq.Types]
type_prop [in CoqInCoq.Types]
U
Under [in CoqInCoq.Infer]W
wf_var [in CoqInCoq.Types]wf_nil [in CoqInCoq.Types]
Axiom Index
D
dangerous_discr [in CoqInCoq.MlTypes]M
ml_x_int_inj [in CoqInCoq.MlTypes]ml_x_int [in CoqInCoq.MlTypes]
ml_eq_string [in CoqInCoq.MlTypes]
ml_string [in CoqInCoq.MlTypes]
ml_int_case [in CoqInCoq.MlTypes]
ml_int_pred [in CoqInCoq.MlTypes]
ml_succ [in CoqInCoq.MlTypes]
ml_zero [in CoqInCoq.MlTypes]
ml_eq_int [in CoqInCoq.MlTypes]
ml_int [in CoqInCoq.MlTypes]
Inductive Index
A
adj_cls [in CoqInCoq.Class]alpha [in CoqInCoq.Expr]
ast [in CoqInCoq.Machine]
C
can_interp [in CoqInCoq.Int_stab]chk_error [in CoqInCoq.Infer]
class [in CoqInCoq.Class]
command [in CoqInCoq.Machine]
com_error [in CoqInCoq.Machine]
conv [in CoqInCoq.Termes]
D
decl_error [in CoqInCoq.Infer]E
Econv [in CoqInCoq.Ered]Epar_red1 [in CoqInCoq.Ered]
equiv_env [in CoqInCoq.Equiv]
Ered [in CoqInCoq.Ered]
Ered1 [in CoqInCoq.Ered]
error [in CoqInCoq.Machine]
Etyp [in CoqInCoq.ETypes]
Ewf [in CoqInCoq.ETypes]
expln [in CoqInCoq.Infer]
expr [in CoqInCoq.Expr]
expr_of_ast [in CoqInCoq.Machine]
expr_vars [in CoqInCoq.Expr]
F
first_item [in CoqInCoq.MyList]free_db [in CoqInCoq.Termes]
I
ik_eq [in CoqInCoq.Int_typ]In [in CoqInCoq.MyList]
inf_error [in CoqInCoq.Infer]
insert [in CoqInCoq.MyList]
ins_in_env [in CoqInCoq.Types]
int_var_sound [in CoqInCoq.Int_stab]
Int_K [in CoqInCoq.Int_typ]
item [in CoqInCoq.MyList]
L
loose_eqc [in CoqInCoq.Class]M
mem_sort [in CoqInCoq.Termes]mem_sort2 [in CoqInCoq.Ered]
message [in CoqInCoq.Machine]
N
NF_Econv [in CoqInCoq.Equiv]O
ord_insert [in CoqInCoq.Names]P
par_red1 [in CoqInCoq.Termes]perror [in CoqInCoq.Machine]
pmessage [in CoqInCoq.Machine]
ptype_error [in CoqInCoq.Machine]
R
red [in CoqInCoq.Termes]red1 [in CoqInCoq.Termes]
red1_in_env [in CoqInCoq.Types]
S
skel [in CoqInCoq.Class]sort [in CoqInCoq.Termes]
subterm [in CoqInCoq.Termes]
subt_nobind [in CoqInCoq.Termes]
subt_bind [in CoqInCoq.Termes]
sub_in_env [in CoqInCoq.Types]
synthesis_trans [in CoqInCoq.Machine]
synth_error [in CoqInCoq.Machine]
T
term [in CoqInCoq.Termes]term_expr_equiv [in CoqInCoq.Expr]
Tfor_all2 [in CoqInCoq.ListType]
Tfor_all_fold [in CoqInCoq.ListType]
Tfor_all [in CoqInCoq.ListType]
TIns [in CoqInCoq.ListType]
TList [in CoqInCoq.ListType]
top_error [in CoqInCoq.Machine]
top_trans [in CoqInCoq.Machine]
transition [in CoqInCoq.Machine]
transl_err [in CoqInCoq.Machine]
transl_type_error [in CoqInCoq.Machine]
transl_msg [in CoqInCoq.Machine]
transl_name [in CoqInCoq.Expr]
trm_in_int [in CoqInCoq.Strong_Norm]
trunc [in CoqInCoq.MyList]
TTrunc [in CoqInCoq.ListType]
typ [in CoqInCoq.Types]
type_error [in CoqInCoq.Infer]
typ_cls [in CoqInCoq.Class]
W
wf [in CoqInCoq.Types]Projection Index
A
adapt_class_equal [in CoqInCoq.Strong_Norm]adapt_trm_in_int [in CoqInCoq.Strong_Norm]
C
clos_exp [in CoqInCoq.Can]clos_red [in CoqInCoq.Can]
cons_names [in CoqInCoq.Machine]
cons_env [in CoqInCoq.Machine]
G
glob_unique [in CoqInCoq.Machine]glob_length [in CoqInCoq.Machine]
glob_wf_ctx [in CoqInCoq.Machine]
glob_names [in CoqInCoq.Machine]
glob_ctx [in CoqInCoq.Machine]
I
incl_sn [in CoqInCoq.Can]int_can_adapt [in CoqInCoq.Strong_Norm]
Section Index
B
Beta_Reduction [in CoqInCoq.Termes]C
Church_Rosser [in CoqInCoq.Conv]D
Decidabilite_typage [in CoqInCoq.Infer]L
Listes [in CoqInCoq.MyList]N
Normalisation_Forte [in CoqInCoq.Termes]T
Termes [in CoqInCoq.Termes]TListes [in CoqInCoq.ListType]
Typage [in CoqInCoq.ETypes]
Typage [in CoqInCoq.Types]
TypeChecker [in CoqInCoq.Infer]
Definition Index
A
absurd_prop [in CoqInCoq.Consistency]add_typ [in CoqInCoq.Infer]
answer [in CoqInCoq.Machine]
applist [in CoqInCoq.Consistency]
C
Can [in CoqInCoq.Can]can_adapt [in CoqInCoq.Int_stab]
check_typ [in CoqInCoq.Infer]
class_env [in CoqInCoq.Class]
class_of_ik [in CoqInCoq.Int_typ]
cls [in CoqInCoq.Class]
cls_of_int [in CoqInCoq.Int_typ]
cl_term [in CoqInCoq.Class]
coerce_CR [in CoqInCoq.Int_typ]
compute_nf [in CoqInCoq.Conv_Dec]
com_answer [in CoqInCoq.Machine]
cv_skel [in CoqInCoq.Class]
D
default_can [in CoqInCoq.Can]def_cons [in CoqInCoq.Int_typ]
def_intt [in CoqInCoq.Strong_Norm]
def_intp [in CoqInCoq.Strong_Norm]
E
empty_state [in CoqInCoq.Machine]Enormal [in CoqInCoq.Ered]
env [in CoqInCoq.Types]
Epar_red [in CoqInCoq.Ered]
eqterm [in CoqInCoq.Conv_Dec]
eq_can [in CoqInCoq.Can]
eq_cand [in CoqInCoq.Can]
exec_delete [in CoqInCoq.Machine]
exec_axiom [in CoqInCoq.Machine]
exec_check [in CoqInCoq.Machine]
exec_infer [in CoqInCoq.Machine]
expr_of_term [in CoqInCoq.Expr]
ext_ik [in CoqInCoq.Int_typ]
F
find_free_var [in CoqInCoq.Names]find_free [in CoqInCoq.Names]
H
hnf_proofs [in CoqInCoq.Consistency]I
incl [in CoqInCoq.MyList]infer [in CoqInCoq.Infer]
interp_ast [in CoqInCoq.Machine]
interp_command [in CoqInCoq.Machine]
intP [in CoqInCoq.Int_typ]
intt [in CoqInCoq.Int_term]
int_term [in CoqInCoq.Int_term]
int_typ [in CoqInCoq.Int_typ]
int_inv [in CoqInCoq.Int_typ]
int_eq_can [in CoqInCoq.Int_typ]
int_cons [in CoqInCoq.Int_typ]
int_of_nat [in CoqInCoq.MlTypes]
inv_Etype [in CoqInCoq.ETypes]
inv_type [in CoqInCoq.Types]
is_conv [in CoqInCoq.Conv_Dec]
is_prop [in CoqInCoq.Termes]
is_can [in CoqInCoq.Can]
is_free_var [in CoqInCoq.Expr]
is_atom [in CoqInCoq.Consistency]
is_lam [in CoqInCoq.Equiv]
item_lift [in CoqInCoq.Types]
L
lift [in CoqInCoq.Termes]lift_rec [in CoqInCoq.Termes]
list_index [in CoqInCoq.MyList]
list_disjoint [in CoqInCoq.MyList]
list_item [in CoqInCoq.MyList]
N
name [in CoqInCoq.Names]name_unique [in CoqInCoq.Names]
name_dec [in CoqInCoq.Names]
neutral [in CoqInCoq.Can]
normal [in CoqInCoq.Termes]
norm_body [in CoqInCoq.Conv_Dec]
nth_def [in CoqInCoq.MyList]
O
ord_norm [in CoqInCoq.Conv_Dec]ord_norm1 [in CoqInCoq.Conv_Dec]
P
par_red [in CoqInCoq.Termes]Pi [in CoqInCoq.Can]
prt_names [in CoqInCoq.Names]
R
red_to_prod [in CoqInCoq.Infer]red_to_sort [in CoqInCoq.Infer]
rmv [in CoqInCoq.Names]
S
shift_intt [in CoqInCoq.Int_term]skel_int [in CoqInCoq.Int_typ]
sn [in CoqInCoq.Termes]
str_confluent [in CoqInCoq.Conv]
subst [in CoqInCoq.Termes]
subst_rec [in CoqInCoq.Termes]
synthesis [in CoqInCoq.Machine]
synth_answer [in CoqInCoq.Machine]
T
term_of_expr [in CoqInCoq.Expr]TList_iter [in CoqInCoq.ListType]
Tmap [in CoqInCoq.ListType]
Tnth_def [in CoqInCoq.ListType]
transl_error [in CoqInCoq.Machine]
transl_ty_error [in CoqInCoq.Machine]
transl_message [in CoqInCoq.Machine]
TSmap [in CoqInCoq.ListType]
typ_skel [in CoqInCoq.Class]
U
undef_vars [in CoqInCoq.Expr]V
var_of_nat [in CoqInCoq.Names]Record Index
I
int_adapt [in CoqInCoq.Strong_Norm]is_cand [in CoqInCoq.Can]
S
state [in CoqInCoq.Machine]state_ext [in CoqInCoq.Machine]
| 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 | (830 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4 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 | (21 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 | (312 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 | (285 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 | (11 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (74 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 | (13 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (10 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 | (96 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) |