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 _ (438 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 _ (6 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 _ (2 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 _ (253 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 _ (9 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 _ (70 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 _ (21 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 _ (57 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 _ (2 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 _ (18 entries)

Global Index

A

Abs [constructor, in Termes]
absurd_prop [definition, in Consistency]
abs_par_red [constructor, in Termes]
abs_red_l [constructor, in Termes]
abs_red_r [constructor, in Termes]
Abs_sound [lemma, in Can]
adapt_class_equal [projection, in Strong_Norm]
adapt_int_eq_can [lemma, in Int_typ]
adapt_trm_in_int [projection, in Strong_Norm]
add_typ [lemma, in Infer]
add_typ [lemma, in Infer]
adj_cls [inductive, in Class]
adj_T [constructor, in Class]
adj_t [constructor, in Class]
App [constructor, in Termes]
applist [definition, in Consistency]
applist_assoc [lemma, in Consistency]
app_par_red [constructor, in Termes]
app_red_l [constructor, in Termes]
app_red_r [constructor, in Termes]
atom_inhabitants [lemma, in Consistency]
atom_reduction [lemma, in Consistency]


B

beta [constructor, in Termes]
Beta_Reduction [section, in Termes]


C

Can [definition, in Can]
Can [library]
cand_sat [lemma, in Can]
cand_sn [lemma, in Can]
can_adapt [definition, in Int_typ]
can_interp [inductive, in Int_typ]
ca_K [constructor, in Int_typ]
ca_T [constructor, in Int_typ]
check_typ [lemma, in Infer]
check_typ [lemma, in Infer]
church_rosser [lemma, in Conv]
Church_Rosser [section, in Conv]
class [inductive, in Class]
Class [library]
class_env [definition, in Class]
class_knd [lemma, in Class]
class_lift [lemma, in Class]
class_of_ik [definition, in Int_typ]
class_red [lemma, in Class]
class_sound [lemma, in Class]
class_subst [lemma, in Class]
class_term [lemma, in Class]
class_trm [lemma, in Class]
class_typ [lemma, in Class]
class_type [lemma, in Class]
clos_exp [projection, in Can]
clos_red [projection, in Can]
cls [definition, in Class]
cls_of_int [definition, in Int_typ]
cl_term [definition, in Class]
cl_term_conv [lemma, in Class]
cl_term_ext [lemma, in Class]
cl_term_red [lemma, in Class]
cl_term_red1 [lemma, in Class]
cl_term_sound [lemma, in Class]
cl_term_subst [lemma, in Class]
cl_term_subst0 [lemma, in Class]
coc_consistency [lemma, in Consistency]
coc_consistency_nf [lemma, in Consistency]
coerce_CR [definition, in Int_typ]
coerce_refl [lemma, in Int_typ]
commut_case [lemma, in Class]
commut_lift_subst [lemma, in Termes]
commut_lift_subst_rec [lemma, in Termes]
commut_red1_subterm [lemma, in Termes]
compute_nf [lemma, in Conv_Dec]
confluence_par_red [lemma, in Conv]
confluence_red [lemma, in Conv]
Consistency [library]
cons_can_adapt [lemma, in Int_typ]
cons_int_eq_can [lemma, in Int_typ]
cons_map [definition, in IntMap]
cons_map_ext [lemma, in IntMap]
conv [inductive, in Termes]
Conv [library]
conv_conv_lift [lemma, in Termes]
conv_conv_prod [lemma, in Termes]
conv_conv_subst [lemma, in Termes]
Conv_Dec [library]
conv_int_typ [lemma, in Int_stab]
conv_kind_prop [lemma, in Conv]
conv_prod_atom [lemma, in Consistency]
conv_sort [lemma, in Conv]
conv_sort_atom [lemma, in Consistency]
conv_sort_prod [lemma, in Conv]


D

Decidabilite_typage [section, in Infer]
Decidabilite_typage [section, in Infer]
decide_typ [lemma, in Infer]
decide_typ [lemma, in Infer]
decide_wf [lemma, in Infer]
decide_wf [lemma, in Infer]
default_can [definition, in Can]
def_adapt [lemma, in Strong_Norm]
def_can_is_can [lemma, in Can]
def_ik [definition, in Int_typ]
def_ik_can [lemma, in Int_typ]
def_intp [definition, in Strong_Norm]
def_intp_can [lemma, in Strong_Norm]
def_intt [definition, in Strong_Norm]
def_intt_id [lemma, in Strong_Norm]
del_cons_map [lemma, in IntMap]
del_cons_map2 [lemma, in IntMap]
del_int_eq_can [lemma, in Int_typ]
del_map [definition, in IntMap]
distr_lift_subst [lemma, in Termes]
distr_lift_subst_rec [lemma, in Termes]
distr_subst [lemma, in Termes]
distr_subst_rec [lemma, in Termes]


E

eqic_K [constructor, in Int_typ]
eqic_T [constructor, in Int_typ]
eqterm [lemma, in Conv_Dec]
eq_can [definition, in Can]
eq_cand [definition, in Can]
eq_cand_incl [lemma, in Can]
eq_can_coerce [lemma, in Int_typ]
eq_can_left [lemma, in Can]
eq_can_Pi [lemma, in Can]
eq_can_prod [lemma, in Can]
eq_can_prod_elim [lemma, in Can]
eq_can_right [lemma, in Can]
eq_can_sym [lemma, in Can]
eq_can_trans [lemma, in Can]
eq_map [definition, in IntMap]
EQ_skel [lemma, in Can]
Extract [library]


F

fun_item [lemma, in MyList]


H

hnf_proofs [definition, in Consistency]
hnf_proofs_sound [lemma, in Consistency]


I

id_int_term [lemma, in Strong_Norm]
iK [constructor, in Int_typ]
ik_app [definition, in Int_typ]
ik_app_can [lemma, in Int_typ]
ik_app_ext [lemma, in Int_typ]
ik_beta_redex [lemma, in Int_typ]
ik_eq_can [inductive, in Int_typ]
ik_eq_can_sym [lemma, in Int_typ]
ik_eq_can_trans [lemma, in Int_typ]
ik_eq_fun [definition, in Int_typ]
ik_lam [definition, in Int_typ]
ik_lam_can [lemma, in Int_typ]
ik_lam_ext [lemma, in Int_typ]
ik_pi [definition, in Int_typ]
ik_pi_can [lemma, in Int_typ]
ik_pi_elim [lemma, in Int_typ]
ik_pi_ext [lemma, in Int_typ]
ik_pi_intro [lemma, in Int_typ]
ik_proj_right [lemma, in Int_typ]
incl_sn [projection, in Can]
infer [lemma, in Infer]
infer [lemma, in Infer]
Infer [library]
Infer [library]
insert [inductive, in MyList]
insert_hd [constructor, in MyList]
insert_tl [constructor, in MyList]
ins_cons_map [lemma, in IntMap]
ins_eq [lemma, in MyList]
ins_gt [lemma, in MyList]
ins_int_eq_can [lemma, in Int_typ]
ins_int_eq_can_inv [lemma, in Int_typ]
ins_item_ge_inv [lemma, in Strengthen]
ins_item_lt_inv [lemma, in Strengthen]
ins_le [lemma, in MyList]
ins_map [definition, in IntMap]
interp_is_sound [lemma, in Strong_Norm]
IntMap [library]
intP [definition, in Int_typ]
intt [definition, in Int_term]
int_adapt [record, in Strong_Norm]
int_adapt_cons [lemma, in Strong_Norm]
int_can_adapt [projection, in Strong_Norm]
int_equiv_int_typ [lemma, in Int_stab]
int_eq_can [definition, in Int_typ]
int_eq_can_class [lemma, in Int_typ]
int_eq_can_cons_class [lemma, in Int_typ]
int_eq_can_cons_del [lemma, in Int_typ]
int_eq_can_cons_ins [lemma, in Int_typ]
int_eq_can_right [lemma, in Int_typ]
Int_K [inductive, in Int_typ]
Int_stab [library]
int_term [definition, in Int_term]
Int_term [library]
int_term_rec [definition, in Int_term]
int_term_subst [lemma, in Int_term]
int_typ [definition, in Int_typ]
Int_typ [library]
int_typ_class [lemma, in Int_stab]
int_typ_class_eq [lemma, in Int_stab]
int_typ_is_can [lemma, in Int_stab]
int_typ_red1 [lemma, in Int_stab]
int_var_sound [lemma, in Strong_Norm]
inv_conv_prod_l [lemma, in Conv]
inv_conv_prod_r [lemma, in Conv]
inv_lift_sort [lemma, in Termes]
inv_nth_cs [lemma, in MyList]
inv_nth_nl [lemma, in MyList]
inv_par_red_abs [lemma, in Termes]
inv_subst_sort [lemma, in Termes]
inv_type [definition, in Types]
inv_type_conv [lemma, in Types]
inv_typ_abs [lemma, in Types]
inv_typ_app [lemma, in Types]
inv_typ_applist_head [lemma, in Consistency]
inv_typ_conv_kind [lemma, in Types]
inv_typ_kind [lemma, in Types]
inv_typ_prod [lemma, in Types]
inv_typ_prop [lemma, in Types]
inv_typ_ref [lemma, in Types]
is_atom [definition, in Consistency]
is_atom_app [lemma, in Consistency]
is_can [definition, in Can]
is_cand [record, in Can]
is_can_coerce [lemma, in Int_typ]
is_can_invariant [lemma, in Can]
is_can_Pi [lemma, in Can]
is_can_prod_elim [lemma, in Can]
is_can_prop [lemma, in Can]
is_conv [lemma, in Conv_Dec]
is_prod [lemma, in Infer]
is_prod [lemma, in Infer]
is_sort [lemma, in Infer]
is_sort [lemma, in Infer]
iT [constructor, in Int_typ]
item [inductive, in MyList]
item_hd [constructor, in MyList]
item_tl [constructor, in MyList]
item_trunc [lemma, in MyList]


K

kind [constructor, in Termes]
Knd [constructor, in Class]
Knd_1 [definition, in Class]


L

leqc_ord [constructor, in Class]
leqc_trm [constructor, in Class]
leqc_typ [constructor, in Class]
Library [library]
lift [definition, in Termes]
lift0 [lemma, in Termes]
lift_abs_inv [lemma, in Strengthen]
lift_app_inv [lemma, in Strengthen]
lift_inj [lemma, in Strengthen]
lift_int_typ [lemma, in Int_stab]
lift_prod_inv [lemma, in Strengthen]
lift_rec [definition, in Termes]
lift_rec0 [lemma, in Termes]
lift_ref_ge [lemma, in Termes]
lift_ref_inv [lemma, in Strengthen]
lift_ref_lt [lemma, in Termes]
lift_srt_inv [lemma, in Strengthen]
List [definition, in MyList]
Listes [section, in MyList]
Listes.A [variable, in MyList]
list_item [lemma, in MyList]
loose_eqc [inductive, in Class]
loose_eqc_stable [lemma, in Class]
loose_eqc_trans [lemma, in Class]


M

Map [section, in IntMap]
map [definition, in MyList]
Map.A [variable, in IntMap]
mem_abs_l [constructor, in Termes]
mem_abs_r [constructor, in Termes]
mem_app_l [constructor, in Termes]
mem_app_r [constructor, in Termes]
mem_eq [constructor, in Termes]
mem_prod_l [constructor, in Termes]
mem_prod_r [constructor, in Termes]
mem_sort [inductive, in Termes]
mem_sort_lift [lemma, in Termes]
mem_sort_subst [lemma, in Termes]
MyList [library]


N

neutral [definition, in Can]
nf_uniqueness [lemma, in Conv]
nil_cls [definition, in Class]
nil_intP [definition, in Int_typ]
normal [definition, in Termes]
Normalisation_Forte [section, in Termes]
norm_body [definition, in Conv_Dec]
nth_class_env [lemma, in Class]
nth_class_env' [lemma, in Class]
nth_def [definition, in MyList]
nth_sound [lemma, in MyList]


O

one_step_conv_exp [lemma, in Termes]
one_step_red [lemma, in Termes]
ord_norm [definition, in Conv_Dec]
ord_norm1 [definition, in Conv_Dec]


P

par_beta [constructor, in Termes]
par_red [definition, in Termes]
par_red1 [inductive, in Termes]
par_red1_lift [lemma, in Termes]
par_red1_subst [lemma, in Termes]
par_red_red [lemma, in Termes]
permute_lift [lemma, in Termes]
permute_lift_rec [lemma, in Termes]
Pi [definition, in Can]
pre_strength [lemma, in Strengthen]
PROD [constructor, in Can]
Prod [constructor, in Termes]
prod_inhabitants [lemma, in Consistency]
prod_not_atom [lemma, in Consistency]
prod_par_red [constructor, in Termes]
prod_red_l [constructor, in Termes]
prod_red_r [constructor, in Termes]
proj_fw [definition, in Int_typ]
prop [constructor, in Termes]
PROP [constructor, in Can]


R

red [inductive, in Termes]
red1 [inductive, in Termes]
red1_lift [lemma, in Termes]
red1_par_red1 [lemma, in Termes]
red1_red1_lift_ex [lemma, in Strengthen]
red1_red_ind [lemma, in Termes]
red1_subst_l [lemma, in Termes]
red1_subst_r [lemma, in Termes]
red_conv [lemma, in Termes]
red_int_typ [lemma, in Int_stab]
red_lift_lift_inv [lemma, in Strengthen]
red_normal [lemma, in Termes]
red_par_red [lemma, in Termes]
red_prod_prod [lemma, in Termes]
red_red1_ord_norm [lemma, in Conv_Dec]
red_red_abs [lemma, in Termes]
red_red_app [lemma, in Termes]
red_red_lift [lemma, in Strengthen]
red_red_lift_ex [lemma, in Strengthen]
red_red_prod [lemma, in Termes]
red_red_subst [lemma, in Strengthen]
red_sort_mem [lemma, in Termes]
red_sort_sort [lemma, in Termes]
red_to_prod [lemma, in Infer]
red_to_prod [lemma, in Infer]
red_to_sort [lemma, in Infer]
red_to_sort [lemma, in Infer]
Ref [constructor, in Termes]
refl_conv [constructor, in Termes]
refl_eq_map [lemma, in IntMap]
refl_loose_eqc [lemma, in Class]
refl_par_red1 [lemma, in Termes]
refl_red [constructor, in Termes]
ref_par_red [constructor, in Termes]


S

sbtrm_abs_l [constructor, in Termes]
sbtrm_abs_r [constructor, in Termes]
sbtrm_app_l [constructor, in Termes]
sbtrm_app_r [constructor, in Termes]
sbtrm_prod_l [constructor, in Termes]
sbtrm_prod_r [constructor, in Termes]
sem_typ [definition, in Strong_Norm]
simpl_lift [lemma, in Termes]
simpl_lift_rec [lemma, in Termes]
simpl_subst [lemma, in Termes]
simpl_subst_rec [lemma, in Termes]
skel [inductive, in Can]
skel_sound [lemma, in Class]
sn [definition, in Termes]
sn_prod [lemma, in Termes]
sn_red_sn [lemma, in Termes]
sn_subst [lemma, in Termes]
sort [inductive, in Termes]
sort_not_atom [lemma, in Consistency]
sort_par_red [constructor, in Termes]
Srt [constructor, in Termes]
Strengthen [library]
strengthening [lemma, in Strengthen]
strengthening0 [lemma, in Strengthen]
strengthening_env [lemma, in Strengthen]
strip_lemma [lemma, in Conv]
strong_norm [lemma, in Strong_Norm]
Strong_Norm [library]
str_confluence_par_red1 [lemma, in Conv]
str_confluent [definition, in Conv]
subject_reduction [lemma, in Types]
subj_red [lemma, in Types]
subst [definition, in Termes]
substitution [lemma, in Types]
subst_int_typ [lemma, in Int_stab]
subst_int_typ0 [lemma, in Int_stab]
subst_rec [definition, in Termes]
subst_ref_eq [lemma, in Termes]
subst_ref_gt [lemma, in Termes]
subst_ref_lt [lemma, in Termes]
subterm [inductive, in Termes]
subterm_ord_norm [lemma, in Conv_Dec]
subterm_sn [lemma, in Termes]
sym_conv [lemma, in Termes]
sym_eq_map [lemma, in IntMap]


T

tail_int_eq_can [lemma, in Int_typ]
tc_T [constructor, in Class]
tc_t [constructor, in Class]
term [inductive, in Termes]
Termes [section, in Termes]
Termes [library]
thinning [lemma, in Types]
thinning_n [lemma, in Types]
trans_conv_conv [lemma, in Termes]
trans_conv_exp [constructor, in Termes]
trans_conv_red [constructor, in Termes]
trans_eq_map [lemma, in IntMap]
trans_red [constructor, in Termes]
trans_red_red [lemma, in Termes]
Trm [constructor, in Class]
trm_in_int [definition, in Strong_Norm]
trunc [inductive, in MyList]
trunc_O [constructor, in MyList]
trunc_S [constructor, in MyList]
typ [inductive, in Types]
Typ [constructor, in Class]
Typage [section, in Types]
Types [library]
type_abs [constructor, in Types]
type_app [constructor, in Types]
type_case [lemma, in Types]
type_conv [constructor, in Types]
type_kind_not_conv [lemma, in Types]
type_prod [constructor, in Types]
type_prop [constructor, in Types]
type_reduction [lemma, in Types]
type_sn [lemma, in Strong_Norm]
type_var [constructor, in Types]
typ_cls [inductive, in Class]
typ_conv_conv [lemma, in Types]
typ_inversion [lemma, in Types]
typ_mem_kind [lemma, in Types]
typ_red_env [lemma, in Types]
typ_sub_weak [lemma, in Types]
typ_unique [lemma, in Types]
typ_weak_weak [lemma, in Types]
typ_wf [lemma, in Types]
Typ_1 [definition, in Class]


V

var_in_cand [lemma, in Can]


W

wf [inductive, in Types]
wf_nil [constructor, in Types]
wf_ord_norm [lemma, in Conv_Dec]
wf_ord_norm1 [lemma, in Conv_Dec]
wf_sort [lemma, in Types]
wf_sort_lift [lemma, in Types]
wf_subterm [lemma, in Conv_Dec]
wf_var [constructor, in Types]



Projection Index

A

adapt_class_equal [in Strong_Norm]
adapt_trm_in_int [in Strong_Norm]


C

clos_exp [in Can]
clos_red [in Can]


I

incl_sn [in Can]
int_can_adapt [in Strong_Norm]



Record Index

I

int_adapt [in Strong_Norm]
is_cand [in Can]



Lemma Index

A

Abs_sound [in Can]
adapt_int_eq_can [in Int_typ]
add_typ [in Infer]
add_typ [in Infer]
applist_assoc [in Consistency]
atom_inhabitants [in Consistency]
atom_reduction [in Consistency]


C

cand_sat [in Can]
cand_sn [in Can]
check_typ [in Infer]
check_typ [in Infer]
church_rosser [in Conv]
class_knd [in Class]
class_lift [in Class]
class_red [in Class]
class_sound [in Class]
class_subst [in Class]
class_term [in Class]
class_trm [in Class]
class_typ [in Class]
class_type [in Class]
cl_term_conv [in Class]
cl_term_ext [in Class]
cl_term_red [in Class]
cl_term_red1 [in Class]
cl_term_sound [in Class]
cl_term_subst [in Class]
cl_term_subst0 [in Class]
coc_consistency [in Consistency]
coc_consistency_nf [in Consistency]
coerce_refl [in Int_typ]
commut_case [in Class]
commut_lift_subst [in Termes]
commut_lift_subst_rec [in Termes]
commut_red1_subterm [in Termes]
compute_nf [in Conv_Dec]
confluence_par_red [in Conv]
confluence_red [in Conv]
cons_can_adapt [in Int_typ]
cons_int_eq_can [in Int_typ]
cons_map_ext [in IntMap]
conv_conv_lift [in Termes]
conv_conv_prod [in Termes]
conv_conv_subst [in Termes]
conv_int_typ [in Int_stab]
conv_kind_prop [in Conv]
conv_prod_atom [in Consistency]
conv_sort [in Conv]
conv_sort_atom [in Consistency]
conv_sort_prod [in Conv]


D

decide_typ [in Infer]
decide_typ [in Infer]
decide_wf [in Infer]
decide_wf [in Infer]
def_adapt [in Strong_Norm]
def_can_is_can [in Can]
def_ik_can [in Int_typ]
def_intp_can [in Strong_Norm]
def_intt_id [in Strong_Norm]
del_cons_map [in IntMap]
del_cons_map2 [in IntMap]
del_int_eq_can [in Int_typ]
distr_lift_subst [in Termes]
distr_lift_subst_rec [in Termes]
distr_subst [in Termes]
distr_subst_rec [in Termes]


E

eqterm [in Conv_Dec]
eq_cand_incl [in Can]
eq_can_coerce [in Int_typ]
eq_can_left [in Can]
eq_can_Pi [in Can]
eq_can_prod [in Can]
eq_can_prod_elim [in Can]
eq_can_right [in Can]
eq_can_sym [in Can]
eq_can_trans [in Can]
EQ_skel [in Can]


F

fun_item [in MyList]


H

hnf_proofs_sound [in Consistency]


I

id_int_term [in Strong_Norm]
ik_app_can [in Int_typ]
ik_app_ext [in Int_typ]
ik_beta_redex [in Int_typ]
ik_eq_can_sym [in Int_typ]
ik_eq_can_trans [in Int_typ]
ik_lam_can [in Int_typ]
ik_lam_ext [in Int_typ]
ik_pi_can [in Int_typ]
ik_pi_elim [in Int_typ]
ik_pi_ext [in Int_typ]
ik_pi_intro [in Int_typ]
ik_proj_right [in Int_typ]
infer [in Infer]
infer [in Infer]
ins_cons_map [in IntMap]
ins_eq [in MyList]
ins_gt [in MyList]
ins_int_eq_can [in Int_typ]
ins_int_eq_can_inv [in Int_typ]
ins_item_ge_inv [in Strengthen]
ins_item_lt_inv [in Strengthen]
ins_le [in MyList]
interp_is_sound [in Strong_Norm]
int_adapt_cons [in Strong_Norm]
int_equiv_int_typ [in Int_stab]
int_eq_can_class [in Int_typ]
int_eq_can_cons_class [in Int_typ]
int_eq_can_cons_del [in Int_typ]
int_eq_can_cons_ins [in Int_typ]
int_eq_can_right [in Int_typ]
int_term_subst [in Int_term]
int_typ_class [in Int_stab]
int_typ_class_eq [in Int_stab]
int_typ_is_can [in Int_stab]
int_typ_red1 [in Int_stab]
int_var_sound [in Strong_Norm]
inv_conv_prod_l [in Conv]
inv_conv_prod_r [in Conv]
inv_lift_sort [in Termes]
inv_nth_cs [in MyList]
inv_nth_nl [in MyList]
inv_par_red_abs [in Termes]
inv_subst_sort [in Termes]
inv_type_conv [in Types]
inv_typ_abs [in Types]
inv_typ_app [in Types]
inv_typ_applist_head [in Consistency]
inv_typ_conv_kind [in Types]
inv_typ_kind [in Types]
inv_typ_prod [in Types]
inv_typ_prop [in Types]
inv_typ_ref [in Types]
is_atom_app [in Consistency]
is_can_coerce [in Int_typ]
is_can_invariant [in Can]
is_can_Pi [in Can]
is_can_prod_elim [in Can]
is_can_prop [in Can]
is_conv [in Conv_Dec]
is_prod [in Infer]
is_prod [in Infer]
is_sort [in Infer]
is_sort [in Infer]
item_trunc [in MyList]


L

lift0 [in Termes]
lift_abs_inv [in Strengthen]
lift_app_inv [in Strengthen]
lift_inj [in Strengthen]
lift_int_typ [in Int_stab]
lift_prod_inv [in Strengthen]
lift_rec0 [in Termes]
lift_ref_ge [in Termes]
lift_ref_inv [in Strengthen]
lift_ref_lt [in Termes]
lift_srt_inv [in Strengthen]
list_item [in MyList]
loose_eqc_stable [in Class]
loose_eqc_trans [in Class]


M

mem_sort_lift [in Termes]
mem_sort_subst [in Termes]


N

nf_uniqueness [in Conv]
nth_class_env [in Class]
nth_class_env' [in Class]
nth_sound [in MyList]


O

one_step_conv_exp [in Termes]
one_step_red [in Termes]


P

par_red1_lift [in Termes]
par_red1_subst [in Termes]
par_red_red [in Termes]
permute_lift [in Termes]
permute_lift_rec [in Termes]
pre_strength [in Strengthen]
prod_inhabitants [in Consistency]
prod_not_atom [in Consistency]


R

red1_lift [in Termes]
red1_par_red1 [in Termes]
red1_red1_lift_ex [in Strengthen]
red1_red_ind [in Termes]
red1_subst_l [in Termes]
red1_subst_r [in Termes]
red_conv [in Termes]
red_int_typ [in Int_stab]
red_lift_lift_inv [in Strengthen]
red_normal [in Termes]
red_par_red [in Termes]
red_prod_prod [in Termes]
red_red1_ord_norm [in Conv_Dec]
red_red_abs [in Termes]
red_red_app [in Termes]
red_red_lift [in Strengthen]
red_red_lift_ex [in Strengthen]
red_red_prod [in Termes]
red_red_subst [in Strengthen]
red_sort_mem [in Termes]
red_sort_sort [in Termes]
red_to_prod [in Infer]
red_to_prod [in Infer]
red_to_sort [in Infer]
red_to_sort [in Infer]
refl_eq_map [in IntMap]
refl_loose_eqc [in Class]
refl_par_red1 [in Termes]


S

simpl_lift [in Termes]
simpl_lift_rec [in Termes]
simpl_subst [in Termes]
simpl_subst_rec [in Termes]
skel_sound [in Class]
sn_prod [in Termes]
sn_red_sn [in Termes]
sn_subst [in Termes]
sort_not_atom [in Consistency]
strengthening [in Strengthen]
strengthening0 [in Strengthen]
strengthening_env [in Strengthen]
strip_lemma [in Conv]
strong_norm [in Strong_Norm]
str_confluence_par_red1 [in Conv]
subject_reduction [in Types]
subj_red [in Types]
substitution [in Types]
subst_int_typ [in Int_stab]
subst_int_typ0 [in Int_stab]
subst_ref_eq [in Termes]
subst_ref_gt [in Termes]
subst_ref_lt [in Termes]
subterm_ord_norm [in Conv_Dec]
subterm_sn [in Termes]
sym_conv [in Termes]
sym_eq_map [in IntMap]


T

tail_int_eq_can [in Int_typ]
thinning [in Types]
thinning_n [in Types]
trans_conv_conv [in Termes]
trans_eq_map [in IntMap]
trans_red_red [in Termes]
type_case [in Types]
type_kind_not_conv [in Types]
type_reduction [in Types]
type_sn [in Strong_Norm]
typ_conv_conv [in Types]
typ_inversion [in Types]
typ_mem_kind [in Types]
typ_red_env [in Types]
typ_sub_weak [in Types]
typ_unique [in Types]
typ_weak_weak [in Types]
typ_wf [in Types]


V

var_in_cand [in Can]


W

wf_ord_norm [in Conv_Dec]
wf_ord_norm1 [in Conv_Dec]
wf_sort [in Types]
wf_sort_lift [in Types]
wf_subterm [in Conv_Dec]



Section Index

B

Beta_Reduction [in Termes]


C

Church_Rosser [in Conv]


D

Decidabilite_typage [in Infer]
Decidabilite_typage [in Infer]


L

Listes [in MyList]


M

Map [in IntMap]


N

Normalisation_Forte [in Termes]


T

Termes [in Termes]
Typage [in Types]



Constructor Index

A

Abs [in Termes]
abs_par_red [in Termes]
abs_red_l [in Termes]
abs_red_r [in Termes]
adj_T [in Class]
adj_t [in Class]
App [in Termes]
app_par_red [in Termes]
app_red_l [in Termes]
app_red_r [in Termes]


B

beta [in Termes]


C

ca_K [in Int_typ]
ca_T [in Int_typ]


E

eqic_K [in Int_typ]
eqic_T [in Int_typ]


I

iK [in Int_typ]
insert_hd [in MyList]
insert_tl [in MyList]
iT [in Int_typ]
item_hd [in MyList]
item_tl [in MyList]


K

kind [in Termes]
Knd [in Class]


L

leqc_ord [in Class]
leqc_trm [in Class]
leqc_typ [in Class]


M

mem_abs_l [in Termes]
mem_abs_r [in Termes]
mem_app_l [in Termes]
mem_app_r [in Termes]
mem_eq [in Termes]
mem_prod_l [in Termes]
mem_prod_r [in Termes]


P

par_beta [in Termes]
PROD [in Can]
Prod [in Termes]
prod_par_red [in Termes]
prod_red_l [in Termes]
prod_red_r [in Termes]
prop [in Termes]
PROP [in Can]


R

Ref [in Termes]
refl_conv [in Termes]
refl_red [in Termes]
ref_par_red [in Termes]


S

sbtrm_abs_l [in Termes]
sbtrm_abs_r [in Termes]
sbtrm_app_l [in Termes]
sbtrm_app_r [in Termes]
sbtrm_prod_l [in Termes]
sbtrm_prod_r [in Termes]
sort_par_red [in Termes]
Srt [in Termes]


T

tc_T [in Class]
tc_t [in Class]
trans_conv_exp [in Termes]
trans_conv_red [in Termes]
trans_red [in Termes]
Trm [in Class]
trunc_O [in MyList]
trunc_S [in MyList]
Typ [in Class]
type_abs [in Types]
type_app [in Types]
type_conv [in Types]
type_prod [in Types]
type_prop [in Types]
type_var [in Types]


W

wf_nil [in Types]
wf_var [in Types]



Inductive Index

A

adj_cls [in Class]


C

can_interp [in Int_typ]
class [in Class]
conv [in Termes]


I

ik_eq_can [in Int_typ]
insert [in MyList]
Int_K [in Int_typ]
item [in MyList]


L

loose_eqc [in Class]


M

mem_sort [in Termes]


P

par_red1 [in Termes]


R

red [in Termes]
red1 [in Termes]


S

skel [in Can]
sort [in Termes]
subterm [in Termes]


T

term [in Termes]
trunc [in MyList]
typ [in Types]
typ_cls [in Class]


W

wf [in Types]



Definition Index

A

absurd_prop [in Consistency]
applist [in Consistency]


C

Can [in Can]
can_adapt [in Int_typ]
class_env [in Class]
class_of_ik [in Int_typ]
cls [in Class]
cls_of_int [in Int_typ]
cl_term [in Class]
coerce_CR [in Int_typ]
cons_map [in IntMap]


D

default_can [in Can]
def_ik [in Int_typ]
def_intp [in Strong_Norm]
def_intt [in Strong_Norm]
del_map [in IntMap]


E

eq_can [in Can]
eq_cand [in Can]
eq_map [in IntMap]


H

hnf_proofs [in Consistency]


I

ik_app [in Int_typ]
ik_eq_fun [in Int_typ]
ik_lam [in Int_typ]
ik_pi [in Int_typ]
ins_map [in IntMap]
intP [in Int_typ]
intt [in Int_term]
int_eq_can [in Int_typ]
int_term [in Int_term]
int_term_rec [in Int_term]
int_typ [in Int_typ]
inv_type [in Types]
is_atom [in Consistency]
is_can [in Can]


K

Knd_1 [in Class]


L

lift [in Termes]
lift_rec [in Termes]
List [in MyList]


M

map [in MyList]


N

neutral [in Can]
nil_cls [in Class]
nil_intP [in Int_typ]
normal [in Termes]
norm_body [in Conv_Dec]
nth_def [in MyList]


O

ord_norm [in Conv_Dec]
ord_norm1 [in Conv_Dec]


P

par_red [in Termes]
Pi [in Can]
proj_fw [in Int_typ]


S

sem_typ [in Strong_Norm]
sn [in Termes]
str_confluent [in Conv]
subst [in Termes]
subst_rec [in Termes]


T

trm_in_int [in Strong_Norm]
Typ_1 [in Class]



Variable Index

L

Listes.A [in MyList]


M

Map.A [in IntMap]



Library Index

C

Can
Class
Consistency
Conv
Conv_Dec


E

Extract


I

Infer
Infer
IntMap
Int_stab
Int_term
Int_typ


L

Library


M

MyList


S

Strengthen
Strong_Norm


T

Termes
Types



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 _ (438 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 _ (6 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 _ (2 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 _ (253 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 _ (9 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 _ (70 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 _ (21 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 _ (57 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 _ (2 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 _ (18 entries)

This page has been generated by coqdoc