Global Index

G

J

K

Q

Y

Z

_

(332 entries)

Notation Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(12 entries)

Variable Index

C

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

X

Y

Z

_

other

(19 entries)

Library Index

A

G

H

J

K

L

O

P

Q

R

T

U

V

X

Y

Z

_

other

(19 entries)

Lemma Index

B

F

G

H

J

K

O

Q

X

Y

Z

_

other

(45 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

(19 entries)

Axiom Index

C

F

G

H

J

K

L

N

O

Q

R

T

U

V

X

Y

Z

_

other

(19 entries)

Inductive Index

B

C

D

E

F

G

H

I

J

K

L

N

O

Q

R

S

U

V

X

Y

Z

_

other

(5 entries)

Projection Index

B

D

E

G

H

I

J

K

M

N

O

P

Q

R

T

V

W

X

Y

Z

_

other

(25 entries)

Section Index

A

B

C

E

F

G

H

I

J

K

L

O

P

Q

S

U

V

X

Y

Z

_

other

(10 entries)

Instance Index

A

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Definition Index

G

J

K

Q

Y

Z

_

other

(142 entries)

Record Index

B

D

E

G

H

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(11 entries)

Global Index

A

A [axiom, in Containers.W_with_Conversion]
A [variable, in Containers.W_From_Nat]
Addr [definition, in Containers.W_From_Nat]
Addr [inductive, in Containers.Decorate_M]
Addr_rect [definition, in Containers.W_From_Nat]
Addr' [definition, in Containers.W_From_Nat]
Algebra [record, in Containers.Initial_Algebra]
Algebra_Morphism [record, in Containers.Initial_Algebra]
alg_morphism_id [definition, in Containers.Initial_Algebra]
alg_morphism_compose [definition, in Containers.Initial_Algebra]
alg_morph_path [projection, in Containers.Initial_Algebra]
alg_morph_fun [projection, in Containers.Initial_Algebra]
alg_fun [projection, in Containers.Initial_Algebra]
alg_carrier [projection, in Containers.Initial_Algebra]
apply_on_chain [definition, in Containers.Chain]
ap_precompose_inverse_apD10 [lemma, in Containers.W]
ap10_ap_precompose [definition, in Containers.W]
arg [projection, in Containers.W_From_Nat]
arg [definition, in Containers.Decorate_M]
arg_recursor [definition, in Containers.W_From_Nat]

B

B [axiom, in Containers.W_with_Conversion]
B [variable, in Containers.W_From_Nat]
Basic_Types [library]
Basic_Containers [library]
Bool [definition, in Containers.Basic_Types]
Bool_elim [definition, in Containers.Basic_Types]

C

Chain [record, in Containers.Chain]
chain [definition, in Containers.M]
Chain [library]
ch_funs [projection, in Containers.Chain]
ch_types [projection, in Containers.Chain]
Coalgebra [record, in Containers.Final_Coalgebra]
Coalgebra_Hom [record, in Containers.Final_Coalgebra]
Coalgebra_equiv_sigma [lemma, in Containers.Final_Coalgebra]
coalg_hom_path [projection, in Containers.Final_Coalgebra]
coalg_hom_fun [projection, in Containers.Final_Coalgebra]
coalg_fun [projection, in Containers.Final_Coalgebra]
coalg_carrier [projection, in Containers.Final_Coalgebra]
Cochain [record, in Containers.Cochain]
Cochain [library]
cochain_limit [definition, in Containers.Cochain]
coch_funs [projection, in Containers.Cochain]
coch_types [projection, in Containers.Cochain]
code [definition, in Containers.W]
Cone [definition, in Containers.Chain]
Cone0 [definition, in Containers.Chain]
Cone0' [definition, in Containers.Chain]
Cone1 [definition, in Containers.Chain]
Cone1' [definition, in Containers.Chain]
const_container_correct [lemma, in Containers.Basic_Containers]
const_container [definition, in Containers.Basic_Containers]
Container [record, in Containers.Container]
Container [library]
container_implements_pe [lemma, in Containers.Strictly_Positive_Types]
container_functor_is_container_fun [lemma, in Containers.Container]
container_functor [definition, in Containers.Container]
container_extension [definition, in Containers.Container]
contr_recursor [instance, in Containers.W_From_Nat]
contr_local_recursor [instance, in Containers.W_From_Nat]
contr_hom_to_M_coalg [instance, in Containers.M]
corec [definition, in Containers.Decorate_M]
c_Positions [projection, in Containers.Container]
c_Shape [projection, in Containers.Container]

D

dec [definition, in Containers.Decorate_M]
decorate [definition, in Containers.W]
decorate_undecorate [lemma, in Containers.W]
_ =W _ [notation, in Containers.W]
Decorate_W [section, in Containers.W]
Decorate_M.B [variable, in Containers.Decorate_M]
Decorate_M.A2 [variable, in Containers.Decorate_M]
Decorate_M.A1 [variable, in Containers.Decorate_M]
_ =M _ [notation, in Containers.Decorate_M]
Decorate_M.funext [variable, in Containers.Decorate_M]
Decorate_M [section, in Containers.Decorate_M]
Decorate_M [library]
dec_undec [definition, in Containers.Decorate_M]
dec_step_arg [definition, in Containers.Decorate_M]
dec_step_label [definition, in Containers.Decorate_M]
destruct_eta [axiom, in Containers.Decorate_M]

E

Empty [definition, in Containers.Basic_Types]
Empty_elim [definition, in Containers.Basic_Types]
Equivalences [library]
equiv_decorate [lemma, in Containers.W]
equiv_decode [definition, in Containers.W]
equiv_decode_step [definition, in Containers.W]
equiv_arg_recursor [lemma, in Containers.W_From_Nat]
equiv_addr_match [lemma, in Containers.W_From_Nat]
equiv_propresize [axiom, in Containers.W_From_Nat]
equiv_option_ind [lemma, in Containers.Equivalences]
equiv_shift_sequence_contr_base [lemma, in Containers.Equivalences]
equiv_nat_match [lemma, in Containers.Equivalences]
equiv_intensional_choice_finite [lemma, in Containers.Equivalences]
equiv_cochain_limit_base [lemma, in Containers.Cochain]
equiv_cochain_limit_base_simpl [lemma, in Containers.Cochain]
equiv_decorate_M [lemma, in Containers.Decorate_M]
equiv_path_m [definition, in Containers.Decorate_M]
equiv_path_m' [definition, in Containers.Decorate_M]
eta [axiom, in Containers.Decorate_M]
expo_container_correct [lemma, in Containers.Basic_Containers]
expo_container [definition, in Containers.Basic_Containers]
extend_addr [definition, in Containers.W_From_Nat]

F

false [definition, in Containers.Basic_Types]
Fin [definition, in Containers.Basic_Types]
final_coalg_final [projection, in Containers.Final_Coalgebra]
final_coalg_coalgebra [projection, in Containers.Final_Coalgebra]
Final_Coalgebra [record, in Containers.Final_Coalgebra]
Final_Coalgebra [library]
Functor [record, in Containers.Functor]
Functor [library]
f_map_path_composition [projection, in Containers.Functor]
f_map_path_id [projection, in Containers.Functor]
f_map [projection, in Containers.Functor]
f_fun [projection, in Containers.Functor]

H

H [definition, in Containers.M]

I

initial_algebra_unique [lemma, in Containers.Initial_Algebra]
Initial_Algebra [library]
inl [definition, in Containers.Basic_Types]
inr [definition, in Containers.Basic_Types]
in_ [definition, in Containers.M]
ishprop_propresize [axiom, in Containers.W_From_Nat]
issig_Coalgebra_Hom [lemma, in Containers.Final_Coalgebra]
is_final [definition, in Containers.Final_Coalgebra]
is_tree_type_W [instance, in Containers.W_From_Nat]
is_wf_m_arg [definition, in Containers.W_From_Nat]
is_wf [definition, in Containers.W_From_Nat]
is_tree_type_M [instance, in Containers.W_From_Nat]
is_tree_type [record, in Containers.W_From_Nat]
is_final_M' [axiom, in Containers.M_with_Conversion]
is_initial' [definition, in Containers.Initial_Algebra]
is_inductive [definition, in Containers.Initial_Algebra]
is_initial [definition, in Containers.Initial_Algebra]
is_final_m [axiom, in Containers.Decorate_M]
is_equiv_out [instance, in Containers.Decorate_M]
is_final_M [lemma, in Containers.M]

L

label [projection, in Containers.W_From_Nat]
label [definition, in Containers.Decorate_M]
label_at [definition, in Containers.W_From_Nat]
label' [definition, in Containers.W_with_Conversion]
less [definition, in Containers.Basic_Types]
lift [definition, in Containers.W_From_Nat]
limit [definition, in Containers.Chain]
limit_universal [lemma, in Containers.Chain]
local_recursor [definition, in Containers.W_From_Nat]
Local_Recursor [definition, in Containers.W_From_Nat]

M

M [axiom, in Containers.W_From_Nat]
M [axiom, in Containers.M_with_Conversion]
M [inductive, in Containers.Decorate_M]
M [definition, in Containers.M]
M [section, in Containers.M]
M [library]
map [definition, in Containers.Functor]
merely [definition, in Containers.Basic_Types]
merely_elim [definition, in Containers.Basic_Types]
mu_container_correct [lemma, in Containers.Mu_Container]
mu_W [definition, in Containers.Mu_Container]
mu_B [definition, in Containers.Mu_Container]
mu_A [definition, in Containers.Mu_Container]
mu_container [definition, in Containers.Mu_Container]
mu_positions [definition, in Containers.Mu_Container]
mu_shape [definition, in Containers.Mu_Container]
Mu_Container.funext [variable, in Containers.Mu_Container]
Mu_Container [section, in Containers.Mu_Container]
Mu_Container [library]
m_arg_sup [lemma, in Containers.W_From_Nat]
m_label_sup [lemma, in Containers.W_From_Nat]
m_arg [definition, in Containers.W_From_Nat]
m_label [definition, in Containers.W_From_Nat]
m_sup [definition, in Containers.W_From_Nat]
m_out [axiom, in Containers.W_From_Nat]
M_coalg' [definition, in Containers.M_with_Conversion]
m_arg' [definition, in Containers.M_with_Conversion]
m_label' [definition, in Containers.M_with_Conversion]
m_out' [definition, in Containers.M_with_Conversion]
m_out_p' [definition, in Containers.M_with_Conversion]
m_corec' [definition, in Containers.M_with_Conversion]
M_with_Conversion.m_eta_id [variable, in Containers.M_with_Conversion]
m_beta_arg [axiom, in Containers.M_with_Conversion]
m_beta_label [axiom, in Containers.M_with_Conversion]
m_arg [definition, in Containers.M_with_Conversion]
m_label [definition, in Containers.M_with_Conversion]
m_corec [axiom, in Containers.M_with_Conversion]
M_with_Conversion.B [variable, in Containers.M_with_Conversion]
M_with_Conversion.A [variable, in Containers.M_with_Conversion]
M_with_Conversion [section, in Containers.M_with_Conversion]
m_path_arg [definition, in Containers.Decorate_M]
m_path_label [definition, in Containers.Decorate_M]
m_path [definition, in Containers.Decorate_M]
m_coalg [definition, in Containers.Decorate_M]
m_eta [lemma, in Containers.M]
m_beta_arg [definition, in Containers.M]
m_beta_label [definition, in Containers.M]
m_corec [definition, in Containers.M]
m_arg [definition, in Containers.M]
m_label [definition, in Containers.M]
M_coalg [definition, in Containers.M]
m_out [definition, in Containers.M]
M_with_Conversion [library]
M' [definition, in Containers.M_with_Conversion]
M'_equiv_M [lemma, in Containers.M_with_Conversion]
M.A [variable, in Containers.M]
M.B [variable, in Containers.M]
M.Corecursion [section, in Containers.M]
M.Corecursion.step [variable, in Containers.M]

N

nu_container_correct [lemma, in Containers.Nu_Container]
nu_M [definition, in Containers.Nu_Container]
nu_B [definition, in Containers.Nu_Container]
nu_A [definition, in Containers.Nu_Container]
nu_container [definition, in Containers.Nu_Container]
nu_positions [definition, in Containers.Nu_Container]
nu_shape [definition, in Containers.Nu_Container]
Nu_Container.funext [variable, in Containers.Nu_Container]
Nu_Container [section, in Containers.Nu_Container]
Nu_Container [library]

O

out [definition, in Containers.Decorate_M]

P

path_Algebra_Morphism [lemma, in Containers.Initial_Algebra]
PE [inductive, in Containers.Strictly_Positive_Types]
pe_to_container [definition, in Containers.Strictly_Positive_Types]
pe_nu [constructor, in Containers.Strictly_Positive_Types]
pe_mu [constructor, in Containers.Strictly_Positive_Types]
pe_expo [constructor, in Containers.Strictly_Positive_Types]
pe_prod [constructor, in Containers.Strictly_Positive_Types]
pe_sum [constructor, in Containers.Strictly_Positive_Types]
pe_const [constructor, in Containers.Strictly_Positive_Types]
pe_var [constructor, in Containers.Strictly_Positive_Types]
pi [definition, in Containers.M]
polynomial_functors_commute_with_limit [definition, in Containers.Chain]
product_container_correct [lemma, in Containers.Basic_Containers]
product_container [definition, in Containers.Basic_Containers]
propresize [axiom, in Containers.W_From_Nat]

R

recursor [definition, in Containers.W_From_Nat]
Recursor [definition, in Containers.W_From_Nat]
Recursor [section, in Containers.W_From_Nat]
Recursor.C [variable, in Containers.W_From_Nat]
restrict [definition, in Containers.W_From_Nat]
restrict_is_sect [lemma, in Containers.W_From_Nat]
root_addr [constructor, in Containers.W]
root_addr [definition, in Containers.W_From_Nat]
root_addr [constructor, in Containers.Decorate_M]

S

shift_preserves_limit [definition, in Containers.Chain]
shift_chain [definition, in Containers.Chain]
step [definition, in Containers.W_From_Nat]
Strictly_Positive_Types [library]
Substitution [library]
subst_container_correct [lemma, in Containers.Substitution]
subst_container [definition, in Containers.Substitution]
subst_functor [definition, in Containers.Substitution]
subtree_addr [constructor, in Containers.W]
subtree_at_extend_addr [lemma, in Containers.W_From_Nat]
subtree_at [definition, in Containers.W_From_Nat]
subtree_addr [definition, in Containers.W_From_Nat]
subtree_addr [constructor, in Containers.Decorate_M]
sum [definition, in Containers.Basic_Types]
sum_container_correct [lemma, in Containers.Basic_Containers]
sum_container [definition, in Containers.Basic_Containers]
sum_elim [definition, in Containers.Basic_Types]
sup [axiom, in Containers.W_with_Conversion]
sup [projection, in Containers.W_From_Nat]
sup [constructor, in Containers.Decorate_M]
sup' [definition, in Containers.W_with_Conversion]

T

tipe_nu [constructor, in Containers.Strictly_Positive_Types]
tipe_mu [constructor, in Containers.Strictly_Positive_Types]
tipe_expo [constructor, in Containers.Strictly_Positive_Types]
tipe_prod [constructor, in Containers.Strictly_Positive_Types]
tipe_sum [constructor, in Containers.Strictly_Positive_Types]
tipe_const [constructor, in Containers.Strictly_Positive_Types]
tipe_var [constructor, in Containers.Strictly_Positive_Types]
tr [definition, in Containers.Basic_Types]
transport_addr_correct [lemma, in Containers.W]
transport_addr [definition, in Containers.W]
transport_addr_undec1_dec_correct [lemma, in Containers.Decorate_M]
transport_addr_undec1_dec [definition, in Containers.Decorate_M]
transport_addr_correct [lemma, in Containers.Decorate_M]
transport_addr [definition, in Containers.Decorate_M]
Tree_Type [section, in Containers.W_From_Nat]
true [definition, in Containers.Basic_Types]
tt [definition, in Containers.Basic_Types]
type_implements_pe [inductive, in Containers.Strictly_Positive_Types]

U

uc_Positions [projection, in Containers.Container]
uc_Shape [projection, in Containers.Container]
unary_container_functor [definition, in Containers.Container]
Unary_Container [record, in Containers.Container]
undec [definition, in Containers.Decorate_M]
undecorate1 [definition, in Containers.W]
undecorate1_decorate [lemma, in Containers.W]
undecorate1_decorate' [lemma, in Containers.W]
undecorate2 [definition, in Containers.W]
undecorate2_decorate [lemma, in Containers.W]
undec_dec [lemma, in Containers.Decorate_M]
undec1 [definition, in Containers.Decorate_M]
undec1_dec [definition, in Containers.Decorate_M]
undec1_step_arg [definition, in Containers.Decorate_M]
undec1_step_label [definition, in Containers.Decorate_M]
undec2 [definition, in Containers.Decorate_M]
undec2_dec [lemma, in Containers.Decorate_M]
Unit [definition, in Containers.Basic_Types]
Unit_elim [definition, in Containers.Basic_Types]

V

var_container_correct [lemma, in Containers.Basic_Containers]
var_container [definition, in Containers.Basic_Containers]

W

W [section, in Containers.W]
W [axiom, in Containers.W_with_Conversion]
W [definition, in Containers.W_From_Nat]
W [definition, in Containers.M]
W [library]
W_Address [inductive, in Containers.W]
W_initial [lemma, in Containers.W]
W_alg [definition, in Containers.W]
W_rect' [definition, in Containers.W_with_Conversion]
W_rect_β [axiom, in Containers.W_with_Conversion]
W_rect [axiom, in Containers.W_with_Conversion]
w_arg [definition, in Containers.W_From_Nat]
w_label [definition, in Containers.W_From_Nat]
w_sup [definition, in Containers.W_From_Nat]
W_with_Conversion [library]
W_From_Nat [library]
W' [definition, in Containers.W_with_Conversion]
W'_is_W [lemma, in Containers.W_with_Conversion]
W'_equiv_W [lemma, in Containers.W_with_Conversion]
W.A [variable, in Containers.W]
W.B [variable, in Containers.W]
W.in_ [variable, in Containers.W]
W.W [variable, in Containers.W]

X

X [definition, in Containers.W_From_Nat]

other

_ -> _ (container_scope) [notation, in Containers.Basic_Containers]
_ * _ (container_scope) [notation, in Containers.Basic_Containers]
_ + _ (container_scope) [notation, in Containers.Basic_Containers]
_ |- _ ~> _ [notation, in Containers.Strictly_Positive_Types]
_ ;; _ [notation, in Containers.Container]
_ |> _ [notation, in Containers.Container]
_ ||> _ [notation, in Containers.Container]
_ oH _ [notation, in Containers.Initial_Algebra]
(| _ |) [notation, in Containers.Container]
[[ _ ]] [notation, in Containers.Container]

Notation Index

D

_ =W _ [in Containers.W]
_ =M _ [in Containers.Decorate_M]

other

_ -> _ (container_scope) [in Containers.Basic_Containers]
_ * _ (container_scope) [in Containers.Basic_Containers]
_ + _ (container_scope) [in Containers.Basic_Containers]
_ |- _ ~> _ [in Containers.Strictly_Positive_Types]
_ ;; _ [in Containers.Container]
_ |> _ [in Containers.Container]
_ ||> _ [in Containers.Container]
_ oH _ [in Containers.Initial_Algebra]
(| _ |) [in Containers.Container]
[[ _ ]] [in Containers.Container]

Variable Index

A

A [in Containers.W_From_Nat]

B

B [in Containers.W_From_Nat]

D

Decorate_M.B [in Containers.Decorate_M]
Decorate_M.A2 [in Containers.Decorate_M]
Decorate_M.A1 [in Containers.Decorate_M]
Decorate_M.funext [in Containers.Decorate_M]

M

Mu_Container.funext [in Containers.Mu_Container]
M_with_Conversion.m_eta_id [in Containers.M_with_Conversion]
M_with_Conversion.B [in Containers.M_with_Conversion]
M_with_Conversion.A [in Containers.M_with_Conversion]
M.A [in Containers.M]
M.B [in Containers.M]
M.Corecursion.step [in Containers.M]

N

Nu_Container.funext [in Containers.Nu_Container]

R

Recursor.C [in Containers.W_From_Nat]

W

W.A [in Containers.W]
W.B [in Containers.W]
W.in_ [in Containers.W]
W.W [in Containers.W]

Library Index

B

Basic_Types
Basic_Containers

C

Chain
Cochain
Container

D

E

F

Final_Coalgebra
Functor

I

Initial_Algebra

M

M
Mu_Container
M_with_Conversion

N

S

Strictly_Positive_Types
Substitution

W

W
W_with_Conversion
W_From_Nat

Lemma Index

A

ap_precompose_inverse_apD10 [in Containers.W]

C

Coalgebra_equiv_sigma [in Containers.Final_Coalgebra]
const_container_correct [in Containers.Basic_Containers]
container_implements_pe [in Containers.Strictly_Positive_Types]
container_functor_is_container_fun [in Containers.Container]

D

decorate_undecorate [in Containers.W]

E

equiv_decorate [in Containers.W]
equiv_arg_recursor [in Containers.W_From_Nat]
equiv_addr_match [in Containers.W_From_Nat]
equiv_option_ind [in Containers.Equivalences]
equiv_shift_sequence_contr_base [in Containers.Equivalences]
equiv_nat_match [in Containers.Equivalences]
equiv_intensional_choice_finite [in Containers.Equivalences]
equiv_cochain_limit_base [in Containers.Cochain]
equiv_cochain_limit_base_simpl [in Containers.Cochain]
equiv_decorate_M [in Containers.Decorate_M]
expo_container_correct [in Containers.Basic_Containers]

I

initial_algebra_unique [in Containers.Initial_Algebra]
issig_Coalgebra_Hom [in Containers.Final_Coalgebra]
is_final_M [in Containers.M]

L

limit_universal [in Containers.Chain]

M

mu_container_correct [in Containers.Mu_Container]
m_arg_sup [in Containers.W_From_Nat]
m_label_sup [in Containers.W_From_Nat]
m_eta [in Containers.M]
M'_equiv_M [in Containers.M_with_Conversion]

N

nu_container_correct [in Containers.Nu_Container]

P

path_Algebra_Morphism [in Containers.Initial_Algebra]
product_container_correct [in Containers.Basic_Containers]

R

restrict_is_sect [in Containers.W_From_Nat]

S

subst_container_correct [in Containers.Substitution]
subtree_at_extend_addr [in Containers.W_From_Nat]
sum_container_correct [in Containers.Basic_Containers]

T

transport_addr_correct [in Containers.W]
transport_addr_undec1_dec_correct [in Containers.Decorate_M]
transport_addr_correct [in Containers.Decorate_M]

U

undecorate1_decorate [in Containers.W]
undecorate1_decorate' [in Containers.W]
undecorate2_decorate [in Containers.W]
undec_dec [in Containers.Decorate_M]
undec2_dec [in Containers.Decorate_M]

V

var_container_correct [in Containers.Basic_Containers]

W

W_initial [in Containers.W]
W'_is_W [in Containers.W_with_Conversion]
W'_equiv_W [in Containers.W_with_Conversion]

Constructor Index

P

pe_nu [in Containers.Strictly_Positive_Types]
pe_mu [in Containers.Strictly_Positive_Types]
pe_expo [in Containers.Strictly_Positive_Types]
pe_prod [in Containers.Strictly_Positive_Types]
pe_sum [in Containers.Strictly_Positive_Types]
pe_const [in Containers.Strictly_Positive_Types]
pe_var [in Containers.Strictly_Positive_Types]

R

root_addr [in Containers.W]
root_addr [in Containers.Decorate_M]

S

subtree_addr [in Containers.W]
subtree_addr [in Containers.Decorate_M]
sup [in Containers.Decorate_M]

T

tipe_nu [in Containers.Strictly_Positive_Types]
tipe_mu [in Containers.Strictly_Positive_Types]
tipe_expo [in Containers.Strictly_Positive_Types]
tipe_prod [in Containers.Strictly_Positive_Types]
tipe_sum [in Containers.Strictly_Positive_Types]
tipe_const [in Containers.Strictly_Positive_Types]
tipe_var [in Containers.Strictly_Positive_Types]

Axiom Index

A

A [in Containers.W_with_Conversion]

B

B [in Containers.W_with_Conversion]

D

destruct_eta [in Containers.Decorate_M]

E

equiv_propresize [in Containers.W_From_Nat]
eta [in Containers.Decorate_M]

I

ishprop_propresize [in Containers.W_From_Nat]
is_final_M' [in Containers.M_with_Conversion]
is_final_m [in Containers.Decorate_M]

M

M [in Containers.W_From_Nat]
M [in Containers.M_with_Conversion]
m_out [in Containers.W_From_Nat]
m_beta_arg [in Containers.M_with_Conversion]
m_beta_label [in Containers.M_with_Conversion]
m_corec [in Containers.M_with_Conversion]

P

propresize [in Containers.W_From_Nat]

S

sup [in Containers.W_with_Conversion]

W

W [in Containers.W_with_Conversion]
W_rect_β [in Containers.W_with_Conversion]
W_rect [in Containers.W_with_Conversion]

Inductive Index

A

Addr [in Containers.Decorate_M]

M

M [in Containers.Decorate_M]

P

PE [in Containers.Strictly_Positive_Types]

T

type_implements_pe [in Containers.Strictly_Positive_Types]

W

W_Address [in Containers.W]

Projection Index

A

alg_morph_path [in Containers.Initial_Algebra]
alg_morph_fun [in Containers.Initial_Algebra]
alg_fun [in Containers.Initial_Algebra]
alg_carrier [in Containers.Initial_Algebra]
arg [in Containers.W_From_Nat]

C

ch_funs [in Containers.Chain]
ch_types [in Containers.Chain]
coalg_hom_path [in Containers.Final_Coalgebra]
coalg_hom_fun [in Containers.Final_Coalgebra]
coalg_fun [in Containers.Final_Coalgebra]
coalg_carrier [in Containers.Final_Coalgebra]
coch_funs [in Containers.Cochain]
coch_types [in Containers.Cochain]
c_Positions [in Containers.Container]
c_Shape [in Containers.Container]

F

final_coalg_final [in Containers.Final_Coalgebra]
final_coalg_coalgebra [in Containers.Final_Coalgebra]
f_map_path_composition [in Containers.Functor]
f_map_path_id [in Containers.Functor]
f_map [in Containers.Functor]
f_fun [in Containers.Functor]

L

label [in Containers.W_From_Nat]

S

sup [in Containers.W_From_Nat]

U

uc_Positions [in Containers.Container]
uc_Shape [in Containers.Container]

Section Index

D

Decorate_W [in Containers.W]
Decorate_M [in Containers.Decorate_M]

M

M [in Containers.M]
Mu_Container [in Containers.Mu_Container]
M_with_Conversion [in Containers.M_with_Conversion]
M.Corecursion [in Containers.M]

N

Nu_Container [in Containers.Nu_Container]

R

Recursor [in Containers.W_From_Nat]

T

Tree_Type [in Containers.W_From_Nat]

W

W [in Containers.W]

Instance Index

C

contr_recursor [in Containers.W_From_Nat]
contr_local_recursor [in Containers.W_From_Nat]
contr_hom_to_M_coalg [in Containers.M]

I

is_tree_type_W [in Containers.W_From_Nat]
is_tree_type_M [in Containers.W_From_Nat]
is_equiv_out [in Containers.Decorate_M]

Definition Index

A

Addr [in Containers.W_From_Nat]
Addr_rect [in Containers.W_From_Nat]
Addr' [in Containers.W_From_Nat]
alg_morphism_id [in Containers.Initial_Algebra]
alg_morphism_compose [in Containers.Initial_Algebra]
apply_on_chain [in Containers.Chain]
ap10_ap_precompose [in Containers.W]
arg [in Containers.Decorate_M]
arg_recursor [in Containers.W_From_Nat]

B

Bool [in Containers.Basic_Types]
Bool_elim [in Containers.Basic_Types]

C

chain [in Containers.M]
cochain_limit [in Containers.Cochain]
code [in Containers.W]
Cone [in Containers.Chain]
Cone0 [in Containers.Chain]
Cone0' [in Containers.Chain]
Cone1 [in Containers.Chain]
Cone1' [in Containers.Chain]
const_container [in Containers.Basic_Containers]
container_functor [in Containers.Container]
container_extension [in Containers.Container]
corec [in Containers.Decorate_M]

D

dec [in Containers.Decorate_M]
decorate [in Containers.W]
dec_undec [in Containers.Decorate_M]
dec_step_arg [in Containers.Decorate_M]
dec_step_label [in Containers.Decorate_M]

E

Empty [in Containers.Basic_Types]
Empty_elim [in Containers.Basic_Types]
equiv_decode [in Containers.W]
equiv_decode_step [in Containers.W]
equiv_path_m [in Containers.Decorate_M]
equiv_path_m' [in Containers.Decorate_M]
expo_container [in Containers.Basic_Containers]
extend_addr [in Containers.W_From_Nat]

F

false [in Containers.Basic_Types]
Fin [in Containers.Basic_Types]

H

H [in Containers.M]

I

inl [in Containers.Basic_Types]
inr [in Containers.Basic_Types]
in_ [in Containers.M]
is_final [in Containers.Final_Coalgebra]
is_wf_m_arg [in Containers.W_From_Nat]
is_wf [in Containers.W_From_Nat]
is_initial' [in Containers.Initial_Algebra]
is_inductive [in Containers.Initial_Algebra]
is_initial [in Containers.Initial_Algebra]

L

label [in Containers.Decorate_M]
label_at [in Containers.W_From_Nat]
label' [in Containers.W_with_Conversion]
less [in Containers.Basic_Types]
lift [in Containers.W_From_Nat]
limit [in Containers.Chain]
local_recursor [in Containers.W_From_Nat]
Local_Recursor [in Containers.W_From_Nat]

M

M [in Containers.M]
map [in Containers.Functor]
merely [in Containers.Basic_Types]
merely_elim [in Containers.Basic_Types]
mu_W [in Containers.Mu_Container]
mu_B [in Containers.Mu_Container]
mu_A [in Containers.Mu_Container]
mu_container [in Containers.Mu_Container]
mu_positions [in Containers.Mu_Container]
mu_shape [in Containers.Mu_Container]
m_arg [in Containers.W_From_Nat]
m_label [in Containers.W_From_Nat]
m_sup [in Containers.W_From_Nat]
M_coalg' [in Containers.M_with_Conversion]
m_arg' [in Containers.M_with_Conversion]
m_label' [in Containers.M_with_Conversion]
m_out' [in Containers.M_with_Conversion]
m_out_p' [in Containers.M_with_Conversion]
m_corec' [in Containers.M_with_Conversion]
m_arg [in Containers.M_with_Conversion]
m_label [in Containers.M_with_Conversion]
m_path_arg [in Containers.Decorate_M]
m_path_label [in Containers.Decorate_M]
m_path [in Containers.Decorate_M]
m_coalg [in Containers.Decorate_M]
m_beta_arg [in Containers.M]
m_beta_label [in Containers.M]
m_corec [in Containers.M]
m_arg [in Containers.M]
m_label [in Containers.M]
M_coalg [in Containers.M]
m_out [in Containers.M]
M' [in Containers.M_with_Conversion]

N

nu_M [in Containers.Nu_Container]
nu_B [in Containers.Nu_Container]
nu_A [in Containers.Nu_Container]
nu_container [in Containers.Nu_Container]
nu_positions [in Containers.Nu_Container]
nu_shape [in Containers.Nu_Container]

O

out [in Containers.Decorate_M]

P

pe_to_container [in Containers.Strictly_Positive_Types]
pi [in Containers.M]
polynomial_functors_commute_with_limit [in Containers.Chain]
product_container [in Containers.Basic_Containers]

R

recursor [in Containers.W_From_Nat]
Recursor [in Containers.W_From_Nat]
restrict [in Containers.W_From_Nat]
root_addr [in Containers.W_From_Nat]

S

shift_preserves_limit [in Containers.Chain]
shift_chain [in Containers.Chain]
step [in Containers.W_From_Nat]
subst_container [in Containers.Substitution]
subst_functor [in Containers.Substitution]
subtree_at [in Containers.W_From_Nat]
subtree_addr [in Containers.W_From_Nat]
sum [in Containers.Basic_Types]
sum_container [in Containers.Basic_Containers]
sum_elim [in Containers.Basic_Types]
sup' [in Containers.W_with_Conversion]

T

tr [in Containers.Basic_Types]
transport_addr [in Containers.W]
transport_addr_undec1_dec [in Containers.Decorate_M]
transport_addr [in Containers.Decorate_M]
true [in Containers.Basic_Types]
tt [in Containers.Basic_Types]

U

unary_container_functor [in Containers.Container]
undec [in Containers.Decorate_M]
undecorate1 [in Containers.W]
undecorate2 [in Containers.W]
undec1 [in Containers.Decorate_M]
undec1_dec [in Containers.Decorate_M]
undec1_step_arg [in Containers.Decorate_M]
undec1_step_label [in Containers.Decorate_M]
undec2 [in Containers.Decorate_M]
Unit [in Containers.Basic_Types]
Unit_elim [in Containers.Basic_Types]

V

var_container [in Containers.Basic_Containers]

W

W [in Containers.W_From_Nat]
W [in Containers.M]
W_alg [in Containers.W]
W_rect' [in Containers.W_with_Conversion]
w_arg [in Containers.W_From_Nat]
w_label [in Containers.W_From_Nat]
w_sup [in Containers.W_From_Nat]
W' [in Containers.W_with_Conversion]

X

X [in Containers.W_From_Nat]

Record Index

A

Algebra [in Containers.Initial_Algebra]
Algebra_Morphism [in Containers.Initial_Algebra]

C

Chain [in Containers.Chain]
Coalgebra [in Containers.Final_Coalgebra]
Coalgebra_Hom [in Containers.Final_Coalgebra]
Cochain [in Containers.Cochain]
Container [in Containers.Container]

F

Final_Coalgebra [in Containers.Final_Coalgebra]
Functor [in Containers.Functor]

I

is_tree_type [in Containers.W_From_Nat]

U

Unary_Container [in Containers.Container]

Global Index

G

J

K

Q

Y

Z

_

(332 entries)

Notation Index

A

B

C

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(12 entries)

Variable Index

C

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

X

Y

Z

_

other

(19 entries)

Library Index

A

G

H

J

K

L

O

P

Q

R

T

U

V

X

Y

Z

_

other

(19 entries)

Lemma Index

B

F

G

H

J

K

O

Q

X

Y

Z

_

other

(45 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

Q

U

V

W

X

Y

Z

_

other

(19 entries)

Axiom Index

C

F

G

H

J

K

L

N

O

Q

R

T

U

V

X

Y

Z

_

other

(19 entries)

Inductive Index

B

C

D

E

F

G

H

I

J

K

L

N

O

Q

R

S

U

V

X

Y

Z

_

other

(5 entries)

Projection Index

B

D

E

G

H

I

J

K

M

N

O

P

Q

R

T

V

W

X

Y

Z

_

other

(25 entries)

Section Index

A

B

C

E

F

G

H

I

J

K

L

O

P

Q

S

U

V

X

Y

Z

_

other

(10 entries)

Instance Index

A

B

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Definition Index

G

J

K

Q

Y

Z

_

other

(142 entries)

Record Index

B

D

E

G

H

J

K

L

M

N

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(11 entries)

This page has been generated by coqdoc