| 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 | _ | (363 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 | _ | (5 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 | _ | (155 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 | _ | (97 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 | _ | (31 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 | _ | (70 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 | _ | (5 entries) |
Global Index
A
AApp [constructor, in TranslValid]AApp_n [definition, in TranslValid]
ACoerce [constructor, in TranslValid]
AConst [constructor, in TranslValid]
AFun [constructor, in TranslValid]
ALet [constructor, in TranslValid]
ALetrec [constructor, in TranslValid]
align [definition, in Coqlib]
align_le [lemma, in Coqlib]
arity [inductive, in Firstorder]
arity_env [definition, in Firstorder]
aterm [inductive, in TranslValid]
aterm_size [definition, in TranslValid]
AVar [constructor, in TranslValid]
B
beq_type [definition, in TranslValid]beq_typelist [definition, in TranslValid]
beq_type_correct [lemma, in TranslValid]
bind [definition, in ErrorMonad]
bind2 [definition, in ErrorMonad]
build_app [definition, in TranslValid]
build_app_correct [lemma, in TranslValid]
C
can_coerce [inductive, in TranslValid]can_coerce_cons [constructor, in TranslValid]
can_coerce_curry [lemma, in TranslValid]
can_coerce_curry_inv [lemma, in TranslValid]
can_coerce_list [inductive, in TranslValid]
can_coerce_nil [constructor, in TranslValid]
can_coerce_NM [constructor, in TranslValid]
can_coerce_NM' [lemma, in TranslValid]
can_coerce_NN [constructor, in TranslValid]
can_coerce_N1 [constructor, in TranslValid]
can_coerce_refl [lemma, in TranslValid]
can_coerce_sub [constructor, in TranslValid]
can_coerce_subtype_mix [lemma, in TranslValid]
can_coerce_subtype_trans [lemma, in TranslValid]
can_coerce_T [constructor, in TranslValid]
can_coerce_trans [lemma, in TranslValid]
can_coerce_1N [constructor, in TranslValid]
can_mult_apply [inductive, in Uncurry]
can_mult_apply_cons [constructor, in Uncurry]
can_mult_apply_nil [constructor, in Uncurry]
can_subtype_coerce_trans [lemma, in TranslValid]
coerce [inductive, in Uncurry]
coerce_can_coerce [lemma, in TranslValid]
coerce_cons [constructor, in Uncurry]
coerce_curry [constructor, in Uncurry]
coerce_fun [constructor, in Uncurry]
coerce_list [inductive, in Uncurry]
coerce_nil [constructor, in Uncurry]
coerce_rcomp [lemma, in Uncurry]
coerce_rcomp_var [lemma, in Uncurry]
coerce_sub [constructor, in Uncurry]
coerce_trans [constructor, in Uncurry]
coerce_uncurry [constructor, in Uncurry]
const [axiom, in Uncurry]
Coqlib [library]
curry [definition, in Uncurry]
curry_type [definition, in Uncurry]
D
decomp_F [constructor, in Uncurry]decomp_T [constructor, in Uncurry]
decomp_unary_fun [inductive, in Uncurry]
dec_eq_false [lemma, in Coqlib]
dec_eq_sym [lemma, in Coqlib]
dec_eq_true [lemma, in Coqlib]
do_coerce [definition, in TranslValid]
do_coerce_args [definition, in TranslValid]
do_coerce_complete [lemma, in TranslValid]
do_coerce_correct [lemma, in TranslValid]
do_coerce_rec [definition, in TranslValid]
do_coerce_rec_complete [lemma, in TranslValid]
do_coerce_rec_correct [lemma, in TranslValid]
do_transl [definition, in TranslValid]
do_transl_args [definition, in TranslValid]
do_transl_args_correct [lemma, in TranslValid]
do_transl_complete [lemma, in TranslValid]
do_transl_correct [lemma, in TranslValid]
E
eq_type [definition, in TranslValid]erasure [definition, in TranslValid]
ErrorMonad [library]
extensionality [axiom, in Coqlib]
F
F [constructor, in Uncurry]Firstorder [library]
fun_extensionality [axiom, in Uncurry]
F1 [definition, in TranslValid]
I
incl_app_inv_l [lemma, in Coqlib]incl_app_inv_r [lemma, in Coqlib]
incl_cons_inv [lemma, in Coqlib]
incl_same_head [lemma, in Coqlib]
in_app [lemma, in Coqlib]
in_cns [lemma, in Coqlib]
is_subtype [definition, in TranslValid]
is_subtype_complete [lemma, in TranslValid]
is_subtype_correct [lemma, in TranslValid]
is_subtype_decision_procedure [lemma, in TranslValid]
is_subtype_rec [definition, in TranslValid]
is_subtype_rec_complete [lemma, in TranslValid]
is_subtype_rec_correct [lemma, in TranslValid]
is_tail [inductive, in Coqlib]
is_tail_cons [constructor, in Coqlib]
is_tail_cons_left [lemma, in Coqlib]
is_tail_in [lemma, in Coqlib]
is_tail_incl [lemma, in Coqlib]
is_tail_refl [constructor, in Coqlib]
is_tail_trans [lemma, in Coqlib]
K
Known [constructor, in Firstorder]L
list_append_map [lemma, in Coqlib]list_disjoint [definition, in Coqlib]
list_disjoint_cons_left [lemma, in Coqlib]
list_disjoint_cons_right [lemma, in Coqlib]
list_disjoint_dec [lemma, in Coqlib]
list_disjoint_notin [lemma, in Coqlib]
list_disjoint_sym [lemma, in Coqlib]
list_drop1 [definition, in Coqlib]
list_drop1_incl [lemma, in Coqlib]
list_drop1_norepet [lemma, in Coqlib]
list_drop2 [definition, in Coqlib]
list_drop2_incl [lemma, in Coqlib]
list_drop2_norepet [lemma, in Coqlib]
list_forall2 [inductive, in Coqlib]
list_forall2_cons [constructor, in Coqlib]
list_forall2_imply [lemma, in Coqlib]
list_forall2_length [lemma, in Coqlib]
list_forall2_nil [constructor, in Coqlib]
list_forall3 [inductive, in Coqlib]
list_forall3_cons [constructor, in Coqlib]
list_forall3_nil [constructor, in Coqlib]
list_forall4 [inductive, in Coqlib]
list_forall4_cons [constructor, in Coqlib]
list_forall4_nil [constructor, in Coqlib]
list_in_insert [lemma, in Coqlib]
list_in_map_inv [lemma, in Coqlib]
list_length_map [lemma, in Coqlib]
list_map_compose [lemma, in Coqlib]
list_map_drop1 [lemma, in Coqlib]
list_map_drop2 [lemma, in Coqlib]
list_map_exten [lemma, in Coqlib]
list_map_identity [lemma, in Coqlib]
list_map_norepet [lemma, in Coqlib]
list_map_nth [lemma, in Coqlib]
list_norepet [inductive, in Coqlib]
list_norepet_app [lemma, in Coqlib]
list_norepet_append [lemma, in Coqlib]
list_norepet_append_left [lemma, in Coqlib]
list_norepet_append_right [lemma, in Coqlib]
list_norepet_cons [constructor, in Coqlib]
list_norepet_dec [lemma, in Coqlib]
list_norepet_nil [constructor, in Coqlib]
list_vars [definition, in Uncurry]
lt_rel_comp [lemma, in Uncurry]
M
match_app [definition, in TranslValid]mmap [definition, in ErrorMonad]
modusponens [lemma, in Coqlib]
N
NApp [constructor, in Uncurry]NApp_n [definition, in Uncurry]
NC [constructor, in Uncurry]
NClos [constructor, in Uncurry]
nclos_rec [definition, in Uncurry]
NConst [constructor, in Uncurry]
nenv [definition, in Uncurry]
neval [inductive, in Uncurry]
neval_app [constructor, in Uncurry]
neval_const [constructor, in Uncurry]
neval_fun [constructor, in Uncurry]
neval_list_def [lemma, in Uncurry]
neval_multapp [inductive, in Uncurry]
neval_multapp_cons [constructor, in Uncurry]
neval_multapp_nil [constructor, in Uncurry]
neval_NApp_n [lemma, in Uncurry]
neval_var [constructor, in Uncurry]
neval_var' [lemma, in Uncurry]
NFun [constructor, in Uncurry]
NFun_n [definition, in Uncurry]
NLet [constructor, in Uncurry]
NLetrec [constructor, in Uncurry]
nterm [inductive, in Uncurry]
nterms_of [definition, in TranslValid]
nth_error_app [lemma, in Coqlib]
nth_error_in [lemma, in Coqlib]
nth_error_nil [lemma, in Coqlib]
nvalue [inductive, in Uncurry]
NVar [constructor, in Uncurry]
O
option_map [definition, in Coqlib]P
peq [definition, in Coqlib]peq_false [lemma, in Coqlib]
peq_true [lemma, in Coqlib]
Ple [definition, in Coqlib]
Ple_refl [lemma, in Coqlib]
Ple_succ [lemma, in Coqlib]
Ple_trans [lemma, in Coqlib]
plt [definition, in Coqlib]
Plt [definition, in Coqlib]
Plt_ne [lemma, in Coqlib]
Plt_Ple [lemma, in Coqlib]
Plt_Ple_trans [lemma, in Coqlib]
Plt_strict [lemma, in Coqlib]
Plt_succ [lemma, in Coqlib]
Plt_succ_inv [lemma, in Coqlib]
Plt_trans [lemma, in Coqlib]
Plt_trans_succ [lemma, in Coqlib]
Plt_wf [lemma, in Coqlib]
positive_Peano_ind [lemma, in Coqlib]
positive_rec [definition, in Coqlib]
positive_rec_base [lemma, in Coqlib]
positive_rec_succ [lemma, in Coqlib]
Ppred_Plt [lemma, in Coqlib]
proj_sumbool [definition, in Coqlib]
proj_sumbool_true [lemma, in Coqlib]
proof_irrelevance [axiom, in Coqlib]
prop_extensionality [axiom, in Uncurry]
R
rcomp [definition, in Uncurry]rcompval [definition, in Uncurry]
rcompval_fun [lemma, in Uncurry]
rcomp_appN [lemma, in Uncurry]
rcomp_appT [lemma, in Uncurry]
rcomp_const [lemma, in Uncurry]
rcomp_curried_app [lemma, in Uncurry]
rcomp_curry [lemma, in Uncurry]
rcomp_fun_rval [lemma, in Uncurry]
rcomp_list [definition, in Uncurry]
rcomp_recursive_coerce [lemma, in Uncurry]
rcomp_recursive_coerce_can_mult_apply [lemma, in Uncurry]
rcomp_recursive_coerce_rval_args [lemma, in Uncurry]
rcomp_subtype [lemma, in Uncurry]
rcomp_uncurry [lemma, in Uncurry]
rcomp_var [lemma, in Uncurry]
rel_comp [definition, in Uncurry]
rel_comp_val [definition, in Uncurry]
rel_val [definition, in Uncurry]
renv [inductive, in Uncurry]
renv_cons [constructor, in Uncurry]
renv_decr [lemma, in Uncurry]
renv_lookup [lemma, in Uncurry]
renv_nil [constructor, in Uncurry]
replicate [definition, in Coqlib]
replicate_app [lemma, in Coqlib]
replicate_length [lemma, in Coqlib]
replicate_map [lemma, in Coqlib]
replicate_rev [lemma, in Coqlib]
rval [definition, in Uncurry]
rval_args [inductive, in Uncurry]
rval_args_cons [constructor, in Uncurry]
rval_args_nil [constructor, in Uncurry]
rval_cases [inductive, in Uncurry]
rval_closN [constructor, in Uncurry]
rval_clos1 [constructor, in Uncurry]
rval_const [constructor, in Uncurry]
rval_curry_type [lemma, in Uncurry]
rval_decr [lemma, in Uncurry]
rval_def [lemma, in Uncurry]
rval_fun [lemma, in Uncurry]
rval_fun_charact [lemma, in Uncurry]
rval_fun_charact_2 [lemma, in Uncurry]
rval_fun_charact_3 [lemma, in Uncurry]
rval_fun_rec [lemma, in Uncurry]
rval_fun_shape [lemma, in Uncurry]
rval_subtype [lemma, in Uncurry]
rval_uncurry_type [lemma, in Uncurry]
S
sd_subtype [inductive, in TranslValid]sd_subtype_complete [lemma, in TranslValid]
sd_subtype_cons [constructor, in TranslValid]
sd_subtype_correct [lemma, in TranslValid]
sd_subtype_curry [lemma, in TranslValid]
sd_subtype_curry_inv [lemma, in TranslValid]
sd_subtype_fun [constructor, in TranslValid]
sd_subtype_inj [constructor, in TranslValid]
sd_subtype_list [inductive, in TranslValid]
sd_subtype_list_can_coerce_list [lemma, in TranslValid]
sd_subtype_nil [constructor, in TranslValid]
sd_subtype_refl [lemma, in TranslValid]
sd_subtype_top [constructor, in TranslValid]
sd_subtype_trans [lemma, in TranslValid]
sem_coerce_comp [definition, in Uncurry]
sem_coerce_comp_eval [lemma, in Uncurry]
sem_subtype_comp [definition, in Uncurry]
sem_subtype_val [definition, in Uncurry]
size_type [definition, in TranslValid]
size_typelist [definition, in TranslValid]
subtype [inductive, in Uncurry]
subtype_cons [constructor, in Uncurry]
subtype_fun [constructor, in Uncurry]
subtype_inj [constructor, in Uncurry]
subtype_list [inductive, in Uncurry]
subtype_nil [constructor, in Uncurry]
subtype_refl [constructor, in Uncurry]
subtype_trans [constructor, in Uncurry]
sum_left_map [definition, in Coqlib]
sz_curry_type [lemma, in TranslValid]
sz_list_2 [definition, in TranslValid]
sz_type [definition, in TranslValid]
sz_typelist [definition, in TranslValid]
sz_2 [definition, in TranslValid]
T
T [constructor, in Uncurry]transl [inductive, in Uncurry]
TranslValid [library]
transl_const [constructor, in Uncurry]
transl_correct [lemma, in Uncurry]
transl_fun [constructor, in Uncurry]
transl_list_split [lemma, in TranslValid]
transl_rcomp [lemma, in Uncurry]
transl_var [constructor, in Uncurry]
two_power_nat_O [lemma, in Coqlib]
two_power_nat_pos [lemma, in Coqlib]
type [inductive, in Uncurry]
typenv [definition, in Uncurry]
typenv_of_arityenv [definition, in Firstorder]
types_of [definition, in TranslValid]
type_ind2 [definition, in TranslValid]
type_of_arity [definition, in Firstorder]
U
UApp [constructor, in Uncurry]UApp_n [definition, in Uncurry]
UC [constructor, in Uncurry]
UClos [constructor, in Uncurry]
uclos_rec [definition, in Uncurry]
UConst [constructor, in Uncurry]
uenv [definition, in Uncurry]
ueval [inductive, in Uncurry]
ueval_app [constructor, in Uncurry]
ueval_const [constructor, in Uncurry]
ueval_curried_app [inductive, in Uncurry]
ueval_curried_app_base [constructor, in Uncurry]
ueval_curried_app_cons [constructor, in Uncurry]
ueval_fun [constructor, in Uncurry]
ueval_let [constructor, in Uncurry]
ueval_letrec [constructor, in Uncurry]
ueval_UApp_n_inv [lemma, in Uncurry]
ueval_var [constructor, in Uncurry]
UFun [constructor, in Uncurry]
UFun_n [definition, in Uncurry]
ULet [constructor, in Uncurry]
ULetrec [constructor, in Uncurry]
uncurry [definition, in Uncurry]
Uncurry [library]
Unknown [constructor, in Firstorder]
unroll_positive_rec [lemma, in Coqlib]
uterm [inductive, in Uncurry]
uvalue [inductive, in Uncurry]
UVar [constructor, in Uncurry]
Z
Zdiv_small [lemma, in Coqlib]Zdiv_unique [lemma, in Coqlib]
zeq [definition, in Coqlib]
zeq_false [lemma, in Coqlib]
zeq_true [lemma, in Coqlib]
zle [definition, in Coqlib]
zle_false [lemma, in Coqlib]
zle_true [lemma, in Coqlib]
zlt [definition, in Coqlib]
zlt_false [lemma, in Coqlib]
zlt_true [lemma, in Coqlib]
Zmax_bound_l [lemma, in Coqlib]
Zmax_bound_r [lemma, in Coqlib]
Zmax_spec [lemma, in Coqlib]
Zmin_spec [lemma, in Coqlib]
Zmod_small [lemma, in Coqlib]
Zmod_unique [lemma, in Coqlib]
ztransl [inductive, in Firstorder]
ztransl_app [constructor, in Firstorder]
ztransl_app_known [constructor, in Firstorder]
ztransl_const [constructor, in Firstorder]
ztransl_correct [lemma, in Firstorder]
ztransl_fun [constructor, in Firstorder]
ztransl_transl [lemma, in Firstorder]
ztransl_var_1 [constructor, in Firstorder]
ztransl_var_2 [constructor, in Firstorder]
Axiom Index
C
const [in Uncurry]E
extensionality [in Coqlib]F
fun_extensionality [in Uncurry]P
proof_irrelevance [in Coqlib]prop_extensionality [in Uncurry]
Lemma Index
A
align_le [in Coqlib]B
beq_type_correct [in TranslValid]build_app_correct [in TranslValid]
C
can_coerce_curry [in TranslValid]can_coerce_curry_inv [in TranslValid]
can_coerce_NM' [in TranslValid]
can_coerce_refl [in TranslValid]
can_coerce_subtype_mix [in TranslValid]
can_coerce_subtype_trans [in TranslValid]
can_coerce_trans [in TranslValid]
can_subtype_coerce_trans [in TranslValid]
coerce_can_coerce [in TranslValid]
coerce_rcomp [in Uncurry]
coerce_rcomp_var [in Uncurry]
D
dec_eq_false [in Coqlib]dec_eq_sym [in Coqlib]
dec_eq_true [in Coqlib]
do_coerce_complete [in TranslValid]
do_coerce_correct [in TranslValid]
do_coerce_rec_complete [in TranslValid]
do_coerce_rec_correct [in TranslValid]
do_transl_args_correct [in TranslValid]
do_transl_complete [in TranslValid]
do_transl_correct [in TranslValid]
I
incl_app_inv_l [in Coqlib]incl_app_inv_r [in Coqlib]
incl_cons_inv [in Coqlib]
incl_same_head [in Coqlib]
in_app [in Coqlib]
in_cns [in Coqlib]
is_subtype_complete [in TranslValid]
is_subtype_correct [in TranslValid]
is_subtype_decision_procedure [in TranslValid]
is_subtype_rec_complete [in TranslValid]
is_subtype_rec_correct [in TranslValid]
is_tail_cons_left [in Coqlib]
is_tail_in [in Coqlib]
is_tail_incl [in Coqlib]
is_tail_trans [in Coqlib]
L
list_append_map [in Coqlib]list_disjoint_cons_left [in Coqlib]
list_disjoint_cons_right [in Coqlib]
list_disjoint_dec [in Coqlib]
list_disjoint_notin [in Coqlib]
list_disjoint_sym [in Coqlib]
list_drop1_incl [in Coqlib]
list_drop1_norepet [in Coqlib]
list_drop2_incl [in Coqlib]
list_drop2_norepet [in Coqlib]
list_forall2_imply [in Coqlib]
list_forall2_length [in Coqlib]
list_in_insert [in Coqlib]
list_in_map_inv [in Coqlib]
list_length_map [in Coqlib]
list_map_compose [in Coqlib]
list_map_drop1 [in Coqlib]
list_map_drop2 [in Coqlib]
list_map_exten [in Coqlib]
list_map_identity [in Coqlib]
list_map_norepet [in Coqlib]
list_map_nth [in Coqlib]
list_norepet_app [in Coqlib]
list_norepet_append [in Coqlib]
list_norepet_append_left [in Coqlib]
list_norepet_append_right [in Coqlib]
list_norepet_dec [in Coqlib]
lt_rel_comp [in Uncurry]
M
modusponens [in Coqlib]N
neval_list_def [in Uncurry]neval_NApp_n [in Uncurry]
neval_var' [in Uncurry]
nth_error_app [in Coqlib]
nth_error_in [in Coqlib]
nth_error_nil [in Coqlib]
P
peq_false [in Coqlib]peq_true [in Coqlib]
Ple_refl [in Coqlib]
Ple_succ [in Coqlib]
Ple_trans [in Coqlib]
Plt_ne [in Coqlib]
Plt_Ple [in Coqlib]
Plt_Ple_trans [in Coqlib]
Plt_strict [in Coqlib]
Plt_succ [in Coqlib]
Plt_succ_inv [in Coqlib]
Plt_trans [in Coqlib]
Plt_trans_succ [in Coqlib]
Plt_wf [in Coqlib]
positive_Peano_ind [in Coqlib]
positive_rec_base [in Coqlib]
positive_rec_succ [in Coqlib]
Ppred_Plt [in Coqlib]
proj_sumbool_true [in Coqlib]
R
rcompval_fun [in Uncurry]rcomp_appN [in Uncurry]
rcomp_appT [in Uncurry]
rcomp_const [in Uncurry]
rcomp_curried_app [in Uncurry]
rcomp_curry [in Uncurry]
rcomp_fun_rval [in Uncurry]
rcomp_recursive_coerce [in Uncurry]
rcomp_recursive_coerce_can_mult_apply [in Uncurry]
rcomp_recursive_coerce_rval_args [in Uncurry]
rcomp_subtype [in Uncurry]
rcomp_uncurry [in Uncurry]
rcomp_var [in Uncurry]
renv_decr [in Uncurry]
renv_lookup [in Uncurry]
replicate_app [in Coqlib]
replicate_length [in Coqlib]
replicate_map [in Coqlib]
replicate_rev [in Coqlib]
rval_curry_type [in Uncurry]
rval_decr [in Uncurry]
rval_def [in Uncurry]
rval_fun [in Uncurry]
rval_fun_charact [in Uncurry]
rval_fun_charact_2 [in Uncurry]
rval_fun_charact_3 [in Uncurry]
rval_fun_rec [in Uncurry]
rval_fun_shape [in Uncurry]
rval_subtype [in Uncurry]
rval_uncurry_type [in Uncurry]
S
sd_subtype_complete [in TranslValid]sd_subtype_correct [in TranslValid]
sd_subtype_curry [in TranslValid]
sd_subtype_curry_inv [in TranslValid]
sd_subtype_list_can_coerce_list [in TranslValid]
sd_subtype_refl [in TranslValid]
sd_subtype_trans [in TranslValid]
sem_coerce_comp_eval [in Uncurry]
sz_curry_type [in TranslValid]
T
transl_correct [in Uncurry]transl_list_split [in TranslValid]
transl_rcomp [in Uncurry]
two_power_nat_O [in Coqlib]
two_power_nat_pos [in Coqlib]
U
ueval_UApp_n_inv [in Uncurry]unroll_positive_rec [in Coqlib]
Z
Zdiv_small [in Coqlib]Zdiv_unique [in Coqlib]
zeq_false [in Coqlib]
zeq_true [in Coqlib]
zle_false [in Coqlib]
zle_true [in Coqlib]
zlt_false [in Coqlib]
zlt_true [in Coqlib]
Zmax_bound_l [in Coqlib]
Zmax_bound_r [in Coqlib]
Zmax_spec [in Coqlib]
Zmin_spec [in Coqlib]
Zmod_small [in Coqlib]
Zmod_unique [in Coqlib]
ztransl_correct [in Firstorder]
ztransl_transl [in Firstorder]
Constructor Index
A
AApp [in TranslValid]ACoerce [in TranslValid]
AConst [in TranslValid]
AFun [in TranslValid]
ALet [in TranslValid]
ALetrec [in TranslValid]
AVar [in TranslValid]
C
can_coerce_cons [in TranslValid]can_coerce_nil [in TranslValid]
can_coerce_NM [in TranslValid]
can_coerce_NN [in TranslValid]
can_coerce_N1 [in TranslValid]
can_coerce_sub [in TranslValid]
can_coerce_T [in TranslValid]
can_coerce_1N [in TranslValid]
can_mult_apply_cons [in Uncurry]
can_mult_apply_nil [in Uncurry]
coerce_cons [in Uncurry]
coerce_curry [in Uncurry]
coerce_fun [in Uncurry]
coerce_nil [in Uncurry]
coerce_sub [in Uncurry]
coerce_trans [in Uncurry]
coerce_uncurry [in Uncurry]
D
decomp_F [in Uncurry]decomp_T [in Uncurry]
F
F [in Uncurry]I
is_tail_cons [in Coqlib]is_tail_refl [in Coqlib]
K
Known [in Firstorder]L
list_forall2_cons [in Coqlib]list_forall2_nil [in Coqlib]
list_forall3_cons [in Coqlib]
list_forall3_nil [in Coqlib]
list_forall4_cons [in Coqlib]
list_forall4_nil [in Coqlib]
list_norepet_cons [in Coqlib]
list_norepet_nil [in Coqlib]
N
NApp [in Uncurry]NC [in Uncurry]
NClos [in Uncurry]
NConst [in Uncurry]
neval_app [in Uncurry]
neval_const [in Uncurry]
neval_fun [in Uncurry]
neval_multapp_cons [in Uncurry]
neval_multapp_nil [in Uncurry]
neval_var [in Uncurry]
NFun [in Uncurry]
NLet [in Uncurry]
NLetrec [in Uncurry]
NVar [in Uncurry]
R
renv_cons [in Uncurry]renv_nil [in Uncurry]
rval_args_cons [in Uncurry]
rval_args_nil [in Uncurry]
rval_closN [in Uncurry]
rval_clos1 [in Uncurry]
rval_const [in Uncurry]
S
sd_subtype_cons [in TranslValid]sd_subtype_fun [in TranslValid]
sd_subtype_inj [in TranslValid]
sd_subtype_nil [in TranslValid]
sd_subtype_top [in TranslValid]
subtype_cons [in Uncurry]
subtype_fun [in Uncurry]
subtype_inj [in Uncurry]
subtype_nil [in Uncurry]
subtype_refl [in Uncurry]
subtype_trans [in Uncurry]
T
T [in Uncurry]transl_const [in Uncurry]
transl_fun [in Uncurry]
transl_var [in Uncurry]
U
UApp [in Uncurry]UC [in Uncurry]
UClos [in Uncurry]
UConst [in Uncurry]
ueval_app [in Uncurry]
ueval_const [in Uncurry]
ueval_curried_app_base [in Uncurry]
ueval_curried_app_cons [in Uncurry]
ueval_fun [in Uncurry]
ueval_let [in Uncurry]
ueval_letrec [in Uncurry]
ueval_var [in Uncurry]
UFun [in Uncurry]
ULet [in Uncurry]
ULetrec [in Uncurry]
Unknown [in Firstorder]
UVar [in Uncurry]
Z
ztransl_app [in Firstorder]ztransl_app_known [in Firstorder]
ztransl_const [in Firstorder]
ztransl_fun [in Firstorder]
ztransl_var_1 [in Firstorder]
ztransl_var_2 [in Firstorder]
Inductive Index
A
arity [in Firstorder]aterm [in TranslValid]
C
can_coerce [in TranslValid]can_coerce_list [in TranslValid]
can_mult_apply [in Uncurry]
coerce [in Uncurry]
coerce_list [in Uncurry]
D
decomp_unary_fun [in Uncurry]I
is_tail [in Coqlib]L
list_forall2 [in Coqlib]list_forall3 [in Coqlib]
list_forall4 [in Coqlib]
list_norepet [in Coqlib]
N
neval [in Uncurry]neval_multapp [in Uncurry]
nterm [in Uncurry]
nvalue [in Uncurry]
R
renv [in Uncurry]rval_args [in Uncurry]
rval_cases [in Uncurry]
S
sd_subtype [in TranslValid]sd_subtype_list [in TranslValid]
subtype [in Uncurry]
subtype_list [in Uncurry]
T
transl [in Uncurry]type [in Uncurry]
U
ueval [in Uncurry]ueval_curried_app [in Uncurry]
uterm [in Uncurry]
uvalue [in Uncurry]
Z
ztransl [in Firstorder]Definition Index
A
AApp_n [in TranslValid]align [in Coqlib]
arity_env [in Firstorder]
aterm_size [in TranslValid]
B
beq_type [in TranslValid]beq_typelist [in TranslValid]
bind [in ErrorMonad]
bind2 [in ErrorMonad]
build_app [in TranslValid]
C
curry [in Uncurry]curry_type [in Uncurry]
D
do_coerce [in TranslValid]do_coerce_args [in TranslValid]
do_coerce_rec [in TranslValid]
do_transl [in TranslValid]
do_transl_args [in TranslValid]
E
eq_type [in TranslValid]erasure [in TranslValid]
F
F1 [in TranslValid]I
is_subtype [in TranslValid]is_subtype_rec [in TranslValid]
L
list_disjoint [in Coqlib]list_drop1 [in Coqlib]
list_drop2 [in Coqlib]
list_vars [in Uncurry]
M
match_app [in TranslValid]mmap [in ErrorMonad]
N
NApp_n [in Uncurry]nclos_rec [in Uncurry]
nenv [in Uncurry]
NFun_n [in Uncurry]
nterms_of [in TranslValid]
O
option_map [in Coqlib]P
peq [in Coqlib]Ple [in Coqlib]
plt [in Coqlib]
Plt [in Coqlib]
positive_rec [in Coqlib]
proj_sumbool [in Coqlib]
R
rcomp [in Uncurry]rcompval [in Uncurry]
rcomp_list [in Uncurry]
rel_comp [in Uncurry]
rel_comp_val [in Uncurry]
rel_val [in Uncurry]
replicate [in Coqlib]
rval [in Uncurry]
S
sem_coerce_comp [in Uncurry]sem_subtype_comp [in Uncurry]
sem_subtype_val [in Uncurry]
size_type [in TranslValid]
size_typelist [in TranslValid]
sum_left_map [in Coqlib]
sz_list_2 [in TranslValid]
sz_type [in TranslValid]
sz_typelist [in TranslValid]
sz_2 [in TranslValid]
T
typenv [in Uncurry]typenv_of_arityenv [in Firstorder]
types_of [in TranslValid]
type_ind2 [in TranslValid]
type_of_arity [in Firstorder]
U
UApp_n [in Uncurry]uclos_rec [in Uncurry]
uenv [in Uncurry]
UFun_n [in Uncurry]
uncurry [in Uncurry]
Z
zeq [in Coqlib]zle [in Coqlib]
zlt [in Coqlib]
Library Index
C
CoqlibE
ErrorMonadF
FirstorderT
TranslValidU
Uncurry| 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 | _ | (363 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 | _ | (5 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 | _ | (155 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 | _ | (97 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 | _ | (31 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 | _ | (70 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 | _ | (5 entries) |
This page has been generated by coqdoc