Global Index

(230 entries)

Axiom Index

(12 entries)

Lemma Index

(127 entries)

Constructor Index

(16 entries)

Inductive Index

(13 entries)

Definition Index

(56 entries)

Library Index

(6 entries)

Global Index

A

abs_app1 [lemma, in tip_slc]
appT [constructor, in tip_slc]
App1 [definition, in tip_mm]
app1T [definition, in tip_slc]
app1_abs [lemma, in tip_slc]
App1_Lam [lemma, in tip_mm]
app1_subst [lemma, in tip_slc]
app_as_app1 [lemma, in tip_slc]
arr [constructor, in tip_slc]

B

Beta [inductive, in tip_slc]
beta_fonct [lemma, in tip_slc]
beta_intro [constructor, in tip_slc]
beta_intro2 [lemma, in tip_slc]
beta_subst [lemma, in tip_slc]
bind_congr [lemma, in tip_mm]
bind_map [lemma, in tip_mm]

C

class [axiom, in Quot_T]
classT [definition, in tip_lc]
class_eq [axiom, in Quot_T]
class_rel [axiom, in Quot_T]
class_surj [axiom, in Quot_T]

D

def [definition, in tip_slc]
default [definition, in Misc]
default [definition, in tip_slc]
default_none [lemma, in tip_slc]
default_some [lemma, in tip_slc]
def_fonct [lemma, in tip_slc]
def_none [lemma, in tip_slc]
def_R [definition, in tip_thm]
def_R_none [lemma, in tip_thm]
def_R_some [lemma, in tip_thm]
def_some [lemma, in tip_slc]
def_some_func [lemma, in tip_slc]

E

Eqv [inductive, in Quot_T]
eq_eqv [lemma, in Quot_T]
Eta [inductive, in tip_slc]
eta_fonct [lemma, in tip_slc]
eta_intro [constructor, in tip_slc]
eta_subst [lemma, in tip_slc]
extens [lemma, in Misc]
extens_dep [axiom, in Misc]

F

factor [axiom, in Quot_T]
factorize [axiom, in Quot_T]
factorize1 [lemma, in Quot_T]
factorize2 [lemma, in Quot_T]
factorize_W [lemma, in tip_thm]
factor1 [definition, in Quot_T]
factor1_extens [lemma, in Quot_T]
factor2 [definition, in Quot_T]
factor2_extens [lemma, in Quot_T]
factor_extens [lemma, in Quot_T]
factor_W [definition, in tip_thm]
foc_int_fonct [definition, in tip_mm]
fonct_as_subst [lemma, in tip_slc]
fonct_rich_f [lemma, in tip_slc]
fonct_shift [lemma, in tip_slc]
fonct_subst [lemma, in tip_slc]
functional_choice [axiom, in Misc]
functional_choice_2 [axiom, in tip_lc]

I

iota [definition, in tip_thm]
iota_app1 [lemma, in tip_thm]
iota_factorize [lemma, in tip_thm]
iota_lam [lemma, in tip_thm]
Iota_Monad_Exp_Mor [definition, in tip_thm]
Iota_Monad_Mor [definition, in tip_thm]
iota_subst [lemma, in tip_thm]
iota_unique [lemma, in tip_thm]
iota_var [lemma, in tip_thm]
iso1 [definition, in tip_mm]
iso1_subst [lemma, in tip_mm]
iso2 [definition, in tip_mm]
iso2_subst [lemma, in tip_mm]

L

Lam [definition, in tip_mm]
lamT [constructor, in tip_slc]
Lam_App1 [lemma, in tip_mm]
LCT [definition, in tip_mm]
LCT_bind [lemma, in tip_mm]
LCT_Exp [definition, in tip_mm]
LCT_fonct [lemma, in tip_mm]
LCT_Modul [definition, in tip_mm]
LCT_Modul_Der [definition, in tip_mm]
LCT_Modul_Int [definition, in tip_mm]
LCT_unit [lemma, in tip_mm]
lift [definition, in tip_mm]
lift_fun [lemma, in Quot_T]

M

map [definition, in tip_mm]
map_bind [lemma, in tip_mm]
map_congr [lemma, in tip_mm]
map_id [lemma, in tip_mm]
map_map [lemma, in tip_mm]
map_unit [lemma, in tip_mm]
mbind_der [definition, in tip_mm]
mbind_der_bind [lemma, in tip_mm]
mbind_int [definition, in tip_mm]
mbind_int_bind [lemma, in tip_mm]
Misc [library]
moc_der [definition, in tip_mm]
moc_fonct [axiom, in tip_mm]
moc_int [definition, in tip_mm]
Modul [inductive, in tip_mm]
Modul_Mor [inductive, in tip_mm]
Mod_Der [definition, in tip_mm]
Mod_Int [definition, in tip_mm]
Mod_Taut [definition, in tip_mm]
Monad [inductive, in tip_mm]
Monad_Exp [inductive, in tip_mm]
Monad_Exp_Mor [inductive, in tip_mm]
monad_exp_mor_extens [lemma, in tip_mm]
Monad_Mor [inductive, in tip_mm]
monad_mor_extens [lemma, in tip_mm]

N

None_T [constructor, in tip_slc]

O

optmap [definition, in tip_slc]
optmap [definition, in Misc]
optmap_none [lemma, in tip_slc]
optmap_optmap [lemma, in tip_slc]
optmap_some [lemma, in tip_slc]
opt_T [inductive, in tip_slc]

P

pre_rich_f_varT [lemma, in tip_slc]
pre_shift [definition, in tip_slc]
pre_tt_class_surj [lemma, in tip_lc]
proof_irrelevance [axiom, in Misc]

Q

quotient [axiom, in Quot_T]
Quot_T [library]

R

R [definition, in tip_lc]
rich_f [definition, in tip_slc]
rich_f_none [lemma, in tip_slc]
rich_f_optmap [lemma, in tip_slc]
rich_f_R [definition, in tip_mm]
rich_f_R_none [lemma, in tip_mm]
rich_f_R_some [lemma, in tip_mm]
rich_f_some [lemma, in tip_slc]
rich_f_varT [lemma, in tip_slc]

S

shift [definition, in tip_slc]
shift_R [definition, in tip_mm]
SLCT [definition, in tip_mm]
Some_T [constructor, in tip_slc]
star [constructor, in tip_slc]
subsT [definition, in tip_slc]
subst_expl_app [lemma, in tip_slc]
subst_expl_lam [lemma, in tip_slc]
subst_expl_var [lemma, in tip_slc]
subst_fonct [lemma, in tip_slc]
subst_help [lemma, in tip_slc]
subst_shift [lemma, in tip_slc]
subsT_subsT [lemma, in tip_slc]
subsT_varT [lemma, in tip_slc]

T

tip [inductive, in tip_slc]
tip_lc [library]
tip_mm [library]
tip_slc [library]
tip_thm [library]
tt [definition, in tip_lc]
TT [inductive, in tip_slc]
TTR [inductive, in tip_slc]
ttr_app [constructor, in tip_slc]
ttr_app1 [lemma, in tip_slc]
ttr_beta [constructor, in tip_slc]
ttr_eq [lemma, in tip_slc]
ttr_eta [constructor, in tip_slc]
ttr_fonct [lemma, in tip_slc]
ttr_lam [constructor, in tip_slc]
ttr_refl [lemma, in tip_slc]
ttr_subst [lemma, in tip_slc]
ttr_subst_arg [lemma, in tip_slc]
ttr_subst_fun [lemma, in tip_slc]
ttr_sym [constructor, in tip_slc]
ttr_trans [constructor, in tip_slc]
ttr_var [constructor, in tip_slc]
tt_app [definition, in tip_lc]
tt_app1 [definition, in tip_lc]
tt_app1_factorize [lemma, in tip_lc]
tt_app_factorize [lemma, in tip_lc]
tt_beta [lemma, in tip_lc]
tt_class [definition, in tip_lc]
tt_class_eq [lemma, in tip_lc]
tt_class_rel [lemma, in tip_lc]
tt_class_surj [lemma, in tip_lc]
tt_comm [definition, in tip_lc]
tt_comm_none [lemma, in tip_lc]
tt_comm_rich_f [lemma, in tip_lc]
tt_comm_some [lemma, in tip_lc]
tt_eta [lemma, in tip_lc]
tt_factor [definition, in tip_lc]
tt_factorize [lemma, in tip_lc]
tt_factorize1 [lemma, in tip_lc]
tt_factorize2 [lemma, in tip_lc]
tt_factor1 [definition, in tip_lc]
tt_factor2 [definition, in tip_lc]
tt_fct_as_subst [lemma, in tip_lc]
TT_fonct [definition, in tip_slc]
tt_fonct [definition, in tip_lc]
TT_fonct_app [lemma, in tip_slc]
tt_fonct_factorize [lemma, in tip_lc]
TT_fonct_fonct [lemma, in tip_slc]
TT_fonct_lam [lemma, in tip_slc]
TT_fonct_varT [lemma, in tip_slc]
tt_fun_lift [lemma, in tip_lc]
TT_iota [definition, in tip_thm]
TT_iota_app [lemma, in tip_thm]
TT_iota_app1 [lemma, in tip_thm]
TT_iota_beta [lemma, in tip_thm]
TT_iota_beta2 [lemma, in tip_thm]
TT_iota_eta [lemma, in tip_thm]
TT_iota_eta2 [lemma, in tip_thm]
TT_iota_fct [lemma, in tip_thm]
TT_iota_lam [lemma, in tip_thm]
TT_iota_subst [lemma, in tip_thm]
TT_iota_var [lemma, in tip_thm]
TT_iota_wd [lemma, in tip_thm]
tt_lam [definition, in tip_lc]
tt_lam_factorize [lemma, in tip_lc]
tt_subst [definition, in tip_lc]
tt_subst1 [definition, in tip_lc]
tt_subst1_app [lemma, in tip_lc]
tt_subst1_factorize [lemma, in tip_lc]
tt_subst1_lam [lemma, in tip_lc]
tt_subst1_var [lemma, in tip_lc]
tt_subst2 [lemma, in tip_lc]
tt_subst_app1 [lemma, in tip_lc]
tt_subst_factorize [lemma, in tip_lc]
tt_subst_lam [lemma, in tip_lc]
tt_subst_subst [lemma, in tip_lc]
tt_subst_var [lemma, in tip_lc]
tt_var [definition, in tip_lc]
tt_var_subst [lemma, in tip_lc]

U

unit_bind_match [lemma, in tip_mm]

V

var [lemma, in tip_slc]
varT [constructor, in tip_slc]
varT_subsT [lemma, in tip_slc]
var_subst_match [lemma, in tip_slc]

Axiom Index

C

class [in Quot_T]
class_eq [in Quot_T]
class_rel [in Quot_T]
class_surj [in Quot_T]

E

extens_dep [in Misc]

F

factor [in Quot_T]
factorize [in Quot_T]
functional_choice [in Misc]
functional_choice_2 [in tip_lc]

M

moc_fonct [in tip_mm]

P

proof_irrelevance [in Misc]

Q

quotient [in Quot_T]

Lemma Index

A

abs_app1 [in tip_slc]
app1_abs [in tip_slc]
App1_Lam [in tip_mm]
app1_subst [in tip_slc]
app_as_app1 [in tip_slc]

B

beta_fonct [in tip_slc]
beta_intro2 [in tip_slc]
beta_subst [in tip_slc]
bind_congr [in tip_mm]
bind_map [in tip_mm]

D

default_none [in tip_slc]
default_some [in tip_slc]
def_fonct [in tip_slc]
def_none [in tip_slc]
def_R_none [in tip_thm]
def_R_some [in tip_thm]
def_some [in tip_slc]
def_some_func [in tip_slc]

E

eq_eqv [in Quot_T]
eta_fonct [in tip_slc]
eta_subst [in tip_slc]
extens [in Misc]

F

factorize1 [in Quot_T]
factorize2 [in Quot_T]
factorize_W [in tip_thm]
factor1_extens [in Quot_T]
factor2_extens [in Quot_T]
factor_extens [in Quot_T]
fonct_as_subst [in tip_slc]
fonct_rich_f [in tip_slc]
fonct_shift [in tip_slc]
fonct_subst [in tip_slc]

I

iota_app1 [in tip_thm]
iota_factorize [in tip_thm]
iota_lam [in tip_thm]
iota_subst [in tip_thm]
iota_unique [in tip_thm]
iota_var [in tip_thm]
iso1_subst [in tip_mm]
iso2_subst [in tip_mm]

L

Lam_App1 [in tip_mm]
LCT_bind [in tip_mm]
LCT_fonct [in tip_mm]
LCT_unit [in tip_mm]
lift_fun [in Quot_T]

M

map_bind [in tip_mm]
map_congr [in tip_mm]
map_id [in tip_mm]
map_map [in tip_mm]
map_unit [in tip_mm]
mbind_der_bind [in tip_mm]
mbind_int_bind [in tip_mm]
monad_exp_mor_extens [in tip_mm]
monad_mor_extens [in tip_mm]

O

optmap_none [in tip_slc]
optmap_optmap [in tip_slc]
optmap_some [in tip_slc]

P

pre_rich_f_varT [in tip_slc]
pre_tt_class_surj [in tip_lc]

R

rich_f_none [in tip_slc]
rich_f_optmap [in tip_slc]
rich_f_R_none [in tip_mm]
rich_f_R_some [in tip_mm]
rich_f_some [in tip_slc]
rich_f_varT [in tip_slc]

S

subst_expl_app [in tip_slc]
subst_expl_lam [in tip_slc]
subst_expl_var [in tip_slc]
subst_fonct [in tip_slc]
subst_help [in tip_slc]
subst_shift [in tip_slc]
subsT_subsT [in tip_slc]
subsT_varT [in tip_slc]

T

U

unit_bind_match [in tip_mm]

V

var [in tip_slc]
varT_subsT [in tip_slc]
var_subst_match [in tip_slc]

Constructor Index

A

appT [in tip_slc]
arr [in tip_slc]

B

beta_intro [in tip_slc]

E

eta_intro [in tip_slc]

L

lamT [in tip_slc]

N

None_T [in tip_slc]

S

Some_T [in tip_slc]
star [in tip_slc]

T

ttr_app [in tip_slc]
ttr_beta [in tip_slc]
ttr_eta [in tip_slc]
ttr_lam [in tip_slc]
ttr_sym [in tip_slc]
ttr_trans [in tip_slc]
ttr_var [in tip_slc]

V

varT [in tip_slc]

Inductive Index

B

Beta [in tip_slc]

E

Eqv [in Quot_T]
Eta [in tip_slc]

M

Modul [in tip_mm]
Modul_Mor [in tip_mm]
Monad [in tip_mm]
Monad_Exp [in tip_mm]
Monad_Exp_Mor [in tip_mm]
Monad_Mor [in tip_mm]

O

opt_T [in tip_slc]

T

tip [in tip_slc]
TT [in tip_slc]
TTR [in tip_slc]

Definition Index

A

App1 [in tip_mm]
app1T [in tip_slc]

C

classT [in tip_lc]

D

def [in tip_slc]
default [in Misc]
default [in tip_slc]
def_R [in tip_thm]

F

factor1 [in Quot_T]
factor2 [in Quot_T]
factor_W [in tip_thm]
foc_int_fonct [in tip_mm]

I

iota [in tip_thm]
Iota_Monad_Exp_Mor [in tip_thm]
Iota_Monad_Mor [in tip_thm]
iso1 [in tip_mm]
iso2 [in tip_mm]

L

Lam [in tip_mm]
LCT [in tip_mm]
LCT_Exp [in tip_mm]
LCT_Modul [in tip_mm]
LCT_Modul_Der [in tip_mm]
LCT_Modul_Int [in tip_mm]
lift [in tip_mm]

M

map [in tip_mm]
mbind_der [in tip_mm]
mbind_int [in tip_mm]
moc_der [in tip_mm]
moc_int [in tip_mm]
Mod_Der [in tip_mm]
Mod_Int [in tip_mm]
Mod_Taut [in tip_mm]

O

optmap [in tip_slc]
optmap [in Misc]

P

pre_shift [in tip_slc]

R

R [in tip_lc]
rich_f [in tip_slc]
rich_f_R [in tip_mm]

S

shift [in tip_slc]
shift_R [in tip_mm]
SLCT [in tip_mm]
subsT [in tip_slc]

T

tt [in tip_lc]
tt_app [in tip_lc]
tt_app1 [in tip_lc]
tt_class [in tip_lc]
tt_comm [in tip_lc]
tt_factor [in tip_lc]
tt_factor1 [in tip_lc]
tt_factor2 [in tip_lc]
TT_fonct [in tip_slc]
tt_fonct [in tip_lc]
TT_iota [in tip_thm]
tt_lam [in tip_lc]
tt_subst [in tip_lc]
tt_subst1 [in tip_lc]
tt_var [in tip_lc]

Library Index

M

Misc

Q

Quot_T

T

tip_lc
tip_mm
tip_slc
tip_thm

Global Index

(230 entries)

Axiom Index

(12 entries)

Lemma Index

(127 entries)

Constructor Index

(16 entries)

Inductive Index

(13 entries)

Definition Index

(56 entries)

Library Index

(6 entries)

This page has been generated by coqdoc