Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1260 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(31 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(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

_

other

(19 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(523 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(72 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(43 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(36 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(400 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7 entries)

Global Index

A

ABapprox [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABapprox_PtoT_pruning [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABapprox_pruning_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_choicefun [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP_size_inf [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_PtoT_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABchoicefun [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_PtoT_choice [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_choice_TtoP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABDownarborification [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonotonisation [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABDown_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABis_tree [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone_size [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABmonot_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size [inductive, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUpmono_size_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUpsize_monotone_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ABUp_Up_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
Additional_Lemmas.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
Additional_Lemmas [section, in Continuity.BredeHerbelin.brede_herbelin]
Add_induction_step [lemma, in Continuity.BI]
Add_cat [lemma, in Continuity.BI]
Add_rcons [lemma, in Continuity.BI]
agnostic [definition, in Continuity.Shared.partial]
all_strict_well_founded_neighborhood_are_brouwer_op_transfer [lemma, in Continuity.Partial.Neighborhood]
all_uniform [lemma, in Continuity.continuity_zoo_Prop]
approx [definition, in Continuity.Partial.Modulus]
approx [constructor, in Continuity.BredeHerbelin.brede_herbelin]
approx_sup [lemma, in Continuity.Partial.Modulus]
approx_monotonic_seq [lemma, in Continuity.Partial.Modulus]
arbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Ask [constructor, in Continuity.Partial.DialogueTree]
Ask [constructor, in Continuity.continuity_zoo_Prop]
ask [constructor, in Continuity.continuity_zoo_Prop]
associated_neighborhood_fun_to_associated_tree_fun [lemma, in Continuity.Partial.TreeFunction]
assume_part.impl [variable, in Continuity.Shared.partial]
assume_part [section, in Continuity.Shared.partial]

B

BarInduction [section, in Continuity.BI]
BarInduction.A [variable, in Continuity.BI]
BarInduction.dBI [variable, in Continuity.BI]
BarInduction.R [variable, in Continuity.BI]
barred [definition, in Continuity.extra_principles]
barred_ABbarred_PtoT_Up [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_barred_Upmon [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_ABbarred_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_TtoP_ABbarred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
barred_Bseq_cont [lemma, in Continuity.BI]
barred_Bseq_cont_aux [lemma, in Continuity.BI]
Bars [section, in Continuity.extra_principles]
bar_to_strict_well_founded_neighborhood [lemma, in Continuity.Partial.Neighborhood]
bar_to_neighborhood [lemma, in Continuity.Partial.Neighborhood]
bar_to_well_founded_neighborhood_fun [lemma, in Continuity.Partial.Neighborhood]
bar_to_neighborhood_fun [definition, in Continuity.Partial.Neighborhood]
Bbeta [definition, in Continuity.continuity_zoo_Prop]
BbetaP [lemma, in Continuity.continuity_zoo_Prop]
Bbeta_dep [constructor, in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont [definition, in Continuity.Brouwer_ext]
Bcoind_dial_cont_to_neigh_cont [lemma, in Continuity.kawai2018]
Bconst [constructor, in Continuity.kawai2018]
Bconst_at [constructor, in Continuity.kawai2018]
Beta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
beta [constructor, in Continuity.continuity_zoo_Prop]
Beta_dep [constructor, in Continuity.continuity_zoo_Prop]
beval [definition, in Continuity.continuity_zoo_Prop]
Beval_ext_tree_monotone [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_output_unique [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_constant [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_map_aux [lemma, in Continuity.Brouwer_ext]
Beval_ext_tree_trace [definition, in Continuity.Brouwer_ext]
Beval_ext_tree_trace_aux [definition, in Continuity.Brouwer_ext]
Beval_ext_tree [definition, in Continuity.Brouwer_ext]
Beval_ext_tree_aux [definition, in Continuity.Brouwer_ext]
beval_list_modulus_at [lemma, in Continuity.BI]
beval_list_barred [lemma, in Continuity.BI]
beval_list_barred_aux [lemma, in Continuity.BI]
beval_list_mon [lemma, in Continuity.BI]
beval_list [definition, in Continuity.BI]
beval_ext [lemma, in Continuity.BI]
beval_trace [definition, in Continuity.BI]
Bext_tree [definition, in Continuity.Brouwer_ext]
BI [library]
Bieval [definition, in Continuity.Brouwer_ext]
Bieval_output_unique [lemma, in Continuity.Brouwer_ext]
Bieval_monotone_plus [lemma, in Continuity.Brouwer_ext]
Bieval_monotone [lemma, in Continuity.Brouwer_ext]
Bieval_trace_inf [lemma, in Continuity.kawai2018]
Bieval_trace_Some [lemma, in Continuity.kawai2018]
Bieval_trace [definition, in Continuity.kawai2018]
Bieval_pred_trace [lemma, in Continuity.BI]
Bieval_trace_spec [lemma, in Continuity.BI]
Bieval_trace [definition, in Continuity.BI]
Bieval_pred_to_Bitree_spec [lemma, in Continuity.BI]
bind [projection, in Continuity.Shared.partial]
bind_hasvalue_given [lemma, in Continuity.Shared.partial]
bind_hasvalue [projection, in Continuity.Shared.partial]
bind_ter' [lemma, in Continuity.Partial.Common]
bind_ter [lemma, in Continuity.Partial.Common]
BIProp11Down [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Down_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12 [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13 [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Up_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BIProp13_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
BisimDelayF [constructor, in Continuity.Partial.Delay]
BisimNowF [constructor, in Continuity.Partial.Delay]
bite [constructor, in Continuity.continuity_zoo_Prop]
Bitree [inductive, in Continuity.Brouwer_ext]
Bitree_cont_to_itree_cont [lemma, in Continuity.Brouwer_ext]
Bitree_to_itreeP [lemma, in Continuity.Brouwer_ext]
Bitree_to_itreeP_aux [lemma, in Continuity.Brouwer_ext]
Bitree_to_itree [definition, in Continuity.Brouwer_ext]
Bitree_to_itree_aux [definition, in Continuity.Brouwer_ext]
Bitree_to_option_Bieval [lemma, in Continuity.Brouwer_ext]
Bitree_to_option [definition, in Continuity.Brouwer_ext]
BI_GBI_alt [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_alt [definition, in Continuity.BredeHerbelin.brede_herbelin]
BI_mon.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
BI_mon [section, in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI [lemma, in Continuity.BredeHerbelin.brede_herbelin]
BI_ind [definition, in Continuity.extra_principles]
Bneigh_cont_equiv_dialogue_cont_Brouwer [lemma, in Continuity.kawai2018]
Bneigh_continuous_neigh_continuous [lemma, in Continuity.kawai2018]
Bneigh_cont [definition, in Continuity.kawai2018]
BOp [constructor, in Continuity.Partial.Neighborhood]
brede_herbelin [library]
Bret [constructor, in Continuity.Brouwer_ext]
Brouwer [abbreviation, in Continuity.continuity_zoo_Prop]
Brouwer [section, in Continuity.continuity_zoo_Prop]
brouwer_op_to_neighborhood [lemma, in Continuity.Partial.Neighborhood]
brouwer_op_to_strict_well_founded_neighborhood [lemma, in Continuity.Partial.Neighborhood]
brouwer_operation_cont [definition, in Continuity.Partial.Neighborhood]
brouwer_op_for [definition, in Continuity.Partial.Neighborhood]
brouwer_op_ind' [definition, in Continuity.Partial.Neighborhood]
brouwer_op_sind [definition, in Continuity.Partial.Neighborhood]
brouwer_op_ind [definition, in Continuity.Partial.Neighborhood]
brouwer_op [inductive, in Continuity.Partial.Neighborhood]
Brouwer_interaction_trees.R [variable, in Continuity.Brouwer_ext]
Brouwer_interaction_trees.A [variable, in Continuity.Brouwer_ext]
Brouwer_interaction_trees [section, in Continuity.Brouwer_ext]
Brouwer_ext_tree.R [variable, in Continuity.Brouwer_ext]
Brouwer_ext_tree.A [variable, in Continuity.Brouwer_ext]
Brouwer_ext_tree [section, in Continuity.Brouwer_ext]
Brouwer_operation_at_Type_spec [lemma, in Continuity.kawai2018]
Brouwer_operation_at'_spec1 [lemma, in Continuity.kawai2018]
Brouwer_operation_at_Type_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_rec [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type_rect [definition, in Continuity.kawai2018]
Brouwer_operation_at_Type [inductive, in Continuity.kawai2018]
Brouwer_operation_at'_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at'_rec [definition, in Continuity.kawai2018]
Brouwer_operation_at'_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at'_rect [definition, in Continuity.kawai2018]
Brouwer_operation_at' [inductive, in Continuity.kawai2018]
Brouwer_operation_at_spec [lemma, in Continuity.kawai2018]
Brouwer_operation_at_sind [definition, in Continuity.kawai2018]
Brouwer_operation_at_ind [definition, in Continuity.kawai2018]
Brouwer_operation_at [inductive, in Continuity.kawai2018]
Brouwer_operation_sind [definition, in Continuity.kawai2018]
Brouwer_operation_ind [definition, in Continuity.kawai2018]
Brouwer_operation [inductive, in Continuity.kawai2018]
Brouwer_ext [library]
Brouwer.A [variable, in Continuity.continuity_zoo_Prop]
Brouwer.R [variable, in Continuity.continuity_zoo_Prop]
Bseq_cont_to_dialogue_cont_Brouwer [lemma, in Continuity.BI]
Bsup [constructor, in Continuity.kawai2018]
Bsup_at_Type [constructor, in Continuity.kawai2018]
Bsup_at' [constructor, in Continuity.kawai2018]
Bsup_at [constructor, in Continuity.kawai2018]
Btree [inductive, in Continuity.continuity_zoo_Prop]
Btree_fun_cont_valid [definition, in Continuity.Brouwer_ext]
Btree_fun_cont [definition, in Continuity.Brouwer_ext]
Btree_to_dialogueP [lemma, in Continuity.continuity_zoo_Prop]
Btree_to_dialogueP_aux [lemma, in Continuity.continuity_zoo_Prop]
Btree_to_dialogue [definition, in Continuity.continuity_zoo_Prop]
Btree_to_dialogue_aux [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_sind [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_rec [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_ind [definition, in Continuity.continuity_zoo_Prop]
Btree_dep_rect [definition, in Continuity.continuity_zoo_Prop]
Btree_dep [inductive, in Continuity.continuity_zoo_Prop]
Btree_sind [definition, in Continuity.continuity_zoo_Prop]
Btree_rec [definition, in Continuity.continuity_zoo_Prop]
Btree_ind [definition, in Continuity.continuity_zoo_Prop]
Btree_rect [definition, in Continuity.continuity_zoo_Prop]
Bvalid_every_list [lemma, in Continuity.Brouwer_ext]
Bvalid_plus [lemma, in Continuity.Brouwer_ext]
Bvalid_ext_tree [definition, in Continuity.Brouwer_ext]
Bvis [constructor, in Continuity.Brouwer_ext]

C

Cantor [section, in Continuity.continuity_zoo_Prop]
cantor [lemma, in Continuity.BredeHerbelin.cantor]
cantor [library]
Cantor_Prop [lemma, in Continuity.BredeHerbelin.cantor]
Cantor.A [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.a0 [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.E [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.R [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.A [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types.Q [variable, in Continuity.continuity_zoo_Prop]
Cantor.fix_types [section, in Continuity.continuity_zoo_Prop]
Cantor.L [variable, in Continuity.continuity_zoo_Prop]
Cantor.L_spec [variable, in Continuity.continuity_zoo_Prop]
Cantor.Q [variable, in Continuity.continuity_zoo_Prop]
Cantor.R [variable, in Continuity.continuity_zoo_Prop]
case_to_false [lemma, in Continuity.BredeHerbelin.cantor]
cBI_implies_CI_fail.cBI [variable, in Continuity.BI]
cBI_implies_CI_fail.R [variable, in Continuity.BI]
cBI_implies_CI_fail.A [variable, in Continuity.BI]
cBI_implies_CI_fail [section, in Continuity.BI]
choicefun [definition, in Continuity.BredeHerbelin.brede_herbelin]
choicefun_Downarbor_choicefun [lemma, in Continuity.BredeHerbelin.brede_herbelin]
choice_ABchoice_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
choice_TtoP_ABchoice [lemma, in Continuity.BredeHerbelin.brede_herbelin]
CI_imp_c_BI [lemma, in Continuity.BI]
Classical [library]
CoCI_BI [lemma, in Continuity.BI]
coind_dial_cont_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
coind_dial_cont [definition, in Continuity.continuity_zoo_Prop]
combine_app_same_length_r [lemma, in Continuity.Partial.DialogueTree]
Common [library]
comp_modulus_equiv [lemma, in Continuity.Partial.Modulus]
comp_modulus'_cont [definition, in Continuity.Partial.Modulus]
comp_modulus_cont [definition, in Continuity.Partial.Modulus]
comp_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
constructive_minimizer [lemma, in Continuity.Partial.DialogueTree]
cons_no_dup [lemma, in Continuity.Partial.DialogueTree]
Cont [definition, in Continuity.Classical]
continuity_principles.R [variable, in Continuity.continuity_zoo_Prop]
continuity_principles.A [variable, in Continuity.continuity_zoo_Prop]
continuity_principles.Q [variable, in Continuity.continuity_zoo_Prop]
continuity_principles [section, in Continuity.continuity_zoo_Prop]
continuity_zoo_Prop [library]
ContinuousBarInduction [section, in Continuity.BI]
ContinuousBarInduction.A [variable, in Continuity.BI]
ContinuousBarInduction.CI [variable, in Continuity.BI]
ContinuousBarInduction.R [variable, in Continuity.BI]
ContinuousInduction [section, in Continuity.BI]
ContinuousInduction.A [variable, in Continuity.BI]
ContinuousInduction.CI [variable, in Continuity.BI]
continuous_mod_weak_continuous' [definition, in Continuity.Partial.Modulus]
continuous_mod_to_continuous_mod_weak [lemma, in Continuity.Partial.Modulus]
continuous_mod_weak_continuous [definition, in Continuity.Partial.Modulus]
continuous_modulus_cont_to_have_modulus_fn [lemma, in Continuity.Partial.Modulus]
continuous_modulus_equiv [lemma, in Continuity.Partial.Modulus]
continuous_modulus'_cont [definition, in Continuity.Partial.Modulus]
continuous_modulus_cont [definition, in Continuity.Partial.Modulus]
continuous_via_interrogations_iff [lemma, in Continuity.continuity_zoo_Prop]
continuous_modulus_cont_nat [definition, in Continuity.continuity_zoo_Prop]
continuous_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
cpo_cont_to_monotonic_modulus_cont_nat [lemma, in Continuity.Partial.Modulus]
cpo_cont_to_monotonic [lemma, in Continuity.Partial.Modulus]
cpo_cont [definition, in Continuity.Partial.Modulus]
c_BI_imp_CI [lemma, in Continuity.BI]
c_BI [definition, in Continuity.BI]
c_bar [definition, in Continuity.BI]

D

DC [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp11 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp11_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13 [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym [definition, in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_rev [definition, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
DC_GDC_BI_GBI.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
DC_GDC_BI_GBI [section, in Continuity.BredeHerbelin.brede_herbelin]
decidable_iff [lemma, in Continuity.Util]
Delay [definition, in Continuity.Partial.Delay]
delay [record, in Continuity.Partial.Delay]
Delay [library]
DelayF [constructor, in Continuity.Partial.Delay]
delayF [inductive, in Continuity.Partial.Delay]
delayF_sind [definition, in Continuity.Partial.Delay]
delayF_rec [definition, in Continuity.Partial.Delay]
delayF_ind [definition, in Continuity.Partial.Delay]
delayF_rect [definition, in Continuity.Partial.Delay]
DelayPartialImplem [module, in Continuity.Partial.Delay]
DelayPartialImplem.Bind [module, in Continuity.Partial.Delay]
DelayPartialImplem.bind [definition, in Continuity.Partial.Delay]
DelayPartialImplem.bind_hasvalue [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Bind.bind_delay [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Bind.bind_now [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Bind.hasvalue_reciprocal [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Bind.hasvalue_direct [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.delay_monad [instance, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue [module, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue [inductive, in Continuity.Partial.Delay]
DelayPartialImplem.HasValueDelay [constructor, in Continuity.Partial.Delay]
DelayPartialImplem.HasValueNow [constructor, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_bisim [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_det [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect_delay [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect_now [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect [definition, in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_ind [definition, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux [inductive, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_correct [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_rect [definition, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_ind [definition, in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.HasValueAux [constructor, in Continuity.Partial.Delay]
DelayPartialImplem.mu [definition, in Continuity.Partial.Delay]
DelayPartialImplem.Mu [module, in Continuity.Partial.Delay]
DelayPartialImplem.mu_hasvalue [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux [definition, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_reciprocal [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_spec_reciprocal [definition, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_leq [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_some_false [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_some_true [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_direct [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_spec_direct [definition, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_now_true [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_now_false [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_delay [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_none [definition, in Continuity.Partial.Delay]
DelayPartialImplem.ret [definition, in Continuity.Partial.Delay]
DelayPartialImplem.ret_hasvalue [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Seval [module, in Continuity.Partial.Delay]
DelayPartialImplem.seval [definition, in Continuity.Partial.Delay]
DelayPartialImplem.seval_hasvalue [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.seval_mono [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Seval.delay_some [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Seval.hasvalue_reciprocal [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.Seval.hasvalue_direct [lemma, in Continuity.Partial.Delay]
DelayPartialImplem.undef [definition, in Continuity.Partial.Delay]
DelayPartialImplem.undef_hasvalue [lemma, in Continuity.Partial.Delay]
delay_eta [lemma, in Continuity.Partial.Delay]
delay_bisim_trans [definition, in Continuity.Partial.Delay]
delay_bisim_sym [definition, in Continuity.Partial.Delay]
delay_bisim_refl [definition, in Continuity.Partial.Delay]
delay_bisim_go [projection, in Continuity.Partial.Delay]
delay_bisim [record, in Continuity.Partial.Delay]
delay_bisimF_sind [definition, in Continuity.Partial.Delay]
delay_bisimF_ind [definition, in Continuity.Partial.Delay]
delay_bisimF [inductive, in Continuity.Partial.Delay]
delay_go [projection, in Continuity.Partial.Delay]
Delta0_choice [lemma, in Continuity.continuity_zoo_Prop]
deval [definition, in Continuity.continuity_zoo_Prop]
deval_list_to_dialogue_trace [definition, in Continuity.continuity_zoo_Prop]
dialogue [abbreviation, in Continuity.continuity_zoo_Prop]
dialogue [inductive, in Continuity.continuity_zoo_Prop]
DialogueTree [library]
dialogue_tree_for_at [definition, in Continuity.Partial.DialogueTree]
dialogue_tree_cont [definition, in Continuity.Partial.DialogueTree]
dialogue_tree_for [definition, in Continuity.Partial.DialogueTree]
dialogue_tree_rect_ask [lemma, in Continuity.Partial.DialogueTree]
dialogue_tree_rect_output [lemma, in Continuity.Partial.DialogueTree]
dialogue_tree_ind [definition, in Continuity.Partial.DialogueTree]
dialogue_tree_rect [definition, in Continuity.Partial.DialogueTree]
dialogue_tree [inductive, in Continuity.Partial.DialogueTree]
dialogue_is_uniform [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_list [definition, in Continuity.continuity_zoo_Prop]
dialogue_not_uniform [lemma, in Continuity.continuity_zoo_Prop]
dialogue_F [lemma, in Continuity.continuity_zoo_Prop]
Dialogue_not_uniform [section, in Continuity.continuity_zoo_Prop]
dialogue_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_for [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_wf [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
dialogue_to_btree_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_BtreeP [lemma, in Continuity.continuity_zoo_Prop]
dialogue_to_Btree [definition, in Continuity.continuity_zoo_Prop]
dialogue_to_Brouwer [definition, in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer_to_dialogue_cont [lemma, in Continuity.continuity_zoo_Prop]
dialogue_cont_to_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]
dialogue_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer [definition, in Continuity.continuity_zoo_Prop]
dialogue_cont [definition, in Continuity.continuity_zoo_Prop]
dialogue_sind [definition, in Continuity.continuity_zoo_Prop]
dialogue_rec [definition, in Continuity.continuity_zoo_Prop]
dialogue_ind [definition, in Continuity.continuity_zoo_Prop]
dialogue_rect [definition, in Continuity.continuity_zoo_Prop]
DNE [definition, in Continuity.Classical]
DNS [lemma, in Continuity.Classical]
double_modulus_at [lemma, in Continuity.Partial.Modulus]
DownABarbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [definition, in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [definition, in Continuity.BredeHerbelin.minimal_example]
Downmonotonisation [definition, in Continuity.BredeHerbelin.brede_herbelin]

E

embed [definition, in Continuity.Shared.embed_nat]
EmbedNatNotations [module, in Continuity.Shared.embed_nat]
fun! ⟨ _ , _ ⟩ => _ [notation, in Continuity.Shared.embed_nat]
⟨ _ , _ ⟩ [notation, in Continuity.Shared.embed_nat]
embedP [lemma, in Continuity.Shared.embed_nat]
embed_nat [library]
enumerable [definition, in Continuity.Partial.Neighborhood]
enumerable_to_strictify_neighborhood_cont [lemma, in Continuity.Partial.Neighborhood]
enumerable_list [lemma, in Continuity.Partial.Neighborhood]
enumerable_tuple [lemma, in Continuity.Partial.Neighborhood]
enumerate_tuple [definition, in Continuity.Partial.Neighborhood]
equiv [definition, in Continuity.Shared.partial]
equiv_bind_hasvalue [lemma, in Continuity.Partial.Common]
equiv_ret_bind [lemma, in Continuity.Partial.Common]
equiv_bind_ret [lemma, in Continuity.Partial.Common]
equiv_bind_mult [lemma, in Continuity.Partial.Common]
equiv_hasvalue [lemma, in Continuity.Partial.Common]
equiv_bind' [lemma, in Continuity.Partial.Common]
equiv_bind [lemma, in Continuity.Partial.Common]
eq_catr [lemma, in Continuity.continuity_zoo_Prop]
eq_catl [lemma, in Continuity.continuity_zoo_Prop]
eq_cat [lemma, in Continuity.continuity_zoo_Prop]
Eta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
eta [constructor, in Continuity.continuity_zoo_Prop]
eval [definition, in Continuity.Shared.partial]
eval_hasvalue [definition, in Continuity.Shared.partial]
eval_ext_tree_pref_monotone [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_pref_monotone_aux [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_trace_from_pref [lemma, in Continuity.Brouwer_ext]
eval_ext_tree_from_pref [lemma, in Continuity.Brouwer_ext]
eval_dialogue_tree_ask [lemma, in Continuity.Partial.DialogueTree]
eval_dialogue_tree_output [lemma, in Continuity.Partial.DialogueTree]
eval_dialogue_tree [definition, in Continuity.Partial.DialogueTree]
eval_ext_tree_aux_equiv_trace [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_prev_ask [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_ask_succ [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_succ [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ_result [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ_ter [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_det [lemma, in Continuity.Partial.TreeFunction]
eval_ext_tree [definition, in Continuity.Partial.TreeFunction]
eval_ext_tree_aux [definition, in Continuity.Partial.TreeFunction]
eval_list_map_In [lemma, in Continuity.BI]
eval_list_incl_none [lemma, in Continuity.BI]
eval_list_monotone [lemma, in Continuity.BI]
eval_list_notin_cat [lemma, in Continuity.BI]
eval_list_none_fun [lemma, in Continuity.BI]
eval_list_notin [lemma, in Continuity.BI]
eval_list_In_is_fun [lemma, in Continuity.BI]
eval_list_In [lemma, in Continuity.BI]
eval_list [definition, in Continuity.BI]
eval_modulus_to_ext [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_continuous [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_continuous [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_valid_eqtau [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_to_interrogation [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval_trace [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_monotone [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_monotone [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_map [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_map_aux [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_aux [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_output_unique [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_constant [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree_ext [lemma, in Continuity.continuity_zoo_Prop]
eval_ext_tree [definition, in Continuity.continuity_zoo_Prop]
eval_ext_tree_aux [definition, in Continuity.continuity_zoo_Prop]
eval' [definition, in Continuity.Shared.partial]
extend [definition, in Continuity.Partial.Common]
extend_app [lemma, in Continuity.Partial.Common]
extend_fold_part [lemma, in Continuity.Partial.Common]
extensional [definition, in Continuity.Partial.Modulus]
extra_principles [library]
extree_to_Bextree_noo_eq [lemma, in Continuity.Brouwer_ext]
extree_to_Bextree_noo [definition, in Continuity.Brouwer_ext]
extree_to_Bextree_spec [lemma, in Continuity.Brouwer_ext]
extree_to_Bextree [definition, in Continuity.Brouwer_ext]
extree_to_extree [definition, in Continuity.Brouwer_ext]
ext_but_not_mono [lemma, in Continuity.Partial.Modulus]
ext_tree_to_Bext_tree_valid [lemma, in Continuity.Brouwer_ext]
ext_tree [definition, in Continuity.Partial.TreeFunction]
ext_tree_valid_eqtau_ask [lemma, in Continuity.continuity_zoo_Prop]
ext_tree_valid_valid [lemma, in Continuity.continuity_zoo_Prop]
ext_tree_valid [definition, in Continuity.continuity_zoo_Prop]
ext_tree_valid_aux [definition, in Continuity.continuity_zoo_Prop]
ext_tree_to_int_tree [definition, in Continuity.continuity_zoo_Prop]
ext_tree_for [definition, in Continuity.continuity_zoo_Prop]
ext_tree [definition, in Continuity.continuity_zoo_Prop]
ex_self_mod_to_cpo_cont [lemma, in Continuity.Partial.Modulus]
ex_monotonic_mod_to_monotonic [lemma, in Continuity.Partial.Modulus]
ex_monotonic_mod_to_ex_mod [lemma, in Continuity.Partial.Modulus]
ex_strong_mod_to_ex_monotonic_mod [lemma, in Continuity.Partial.Modulus]
ex_monotonic_modulus [definition, in Continuity.Partial.Modulus]
ex_strong_modulus [definition, in Continuity.Partial.Modulus]
ex_mod_to_ex_mod_weak [lemma, in Continuity.Partial.Modulus]
ex_mod_continuous_weak [definition, in Continuity.Partial.Modulus]
ex_modulus_cont [definition, in Continuity.Partial.Modulus]
ex_modulus_modulus_fun [lemma, in Continuity.continuity_zoo_Prop]
ex_modulus_cont_nat [definition, in Continuity.continuity_zoo_Prop]
ex_modulus_cont [definition, in Continuity.continuity_zoo_Prop]

F

F [projection, in Continuity.Partial.Neighborhood]
F [projection, in Continuity.Partial.DialogueTree]
F [definition, in Continuity.continuity_zoo_Prop]
FinQuestion [section, in Continuity.continuity_zoo_Prop]
FinQuestion.A [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.L [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.L_spec [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.Q [variable, in Continuity.continuity_zoo_Prop]
FinQuestion.R [variable, in Continuity.continuity_zoo_Prop]
firstn_app_l [lemma, in Continuity.Partial.Common]
fixed_magic_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
fixed_magic_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]
fixed_magic [definition, in Continuity.BredeHerbelin.brede_herbelin]
fold_part_list_general_hasvalue [lemma, in Continuity.Partial.DialogueTree]
fold_part_list_general [definition, in Continuity.Partial.DialogueTree]
fold_tab_nth_undef [lemma, in Continuity.Partial.Common]
fold_part_list_ret [lemma, in Continuity.Partial.Common]
fold_part_list_ter [lemma, in Continuity.Partial.Common]
fold_part_list_app [lemma, in Continuity.Partial.Common]
fold_part_list_tabulate_length [lemma, in Continuity.Partial.Common]
fold_part_list_tabulate_add_length [lemma, in Continuity.Partial.Common]
fold_part_list_length [lemma, in Continuity.Partial.Common]
fold_part_list_cons [lemma, in Continuity.Partial.Common]
fold_part_list_aux_app' [lemma, in Continuity.Partial.Common]
fold_part_list_aux_app [lemma, in Continuity.Partial.Common]
fold_part_list [definition, in Continuity.Partial.Common]
fold_part_list_aux [definition, in Continuity.Partial.Common]
follow [definition, in Continuity.continuity_zoo_Prop]
followP [lemma, in Continuity.continuity_zoo_Prop]
Forall_app_r [lemma, in Continuity.Partial.Common]
Forall_app_l [lemma, in Continuity.Partial.Common]
Forall_app [lemma, in Continuity.Partial.Common]
Forall2_rev [lemma, in Continuity.Partial.Common]
Forall2_imp [lemma, in Continuity.Partial.Common]
Forall2_app_r [lemma, in Continuity.Partial.Common]
Forall2_app_l [lemma, in Continuity.Partial.Common]
Forall2_app [lemma, in Continuity.Partial.Common]
from_pref_finite_equal [lemma, in Continuity.Brouwer_ext]
from_pref_map_iota [lemma, in Continuity.Brouwer_ext]
from_pref [definition, in Continuity.continuity_zoo_Prop]
functional [definition, in Continuity.Shared.partial]
FunRel [record, in Continuity.Shared.partial]

G

G [inductive, in Continuity.Shared.mu_nat]
gamma [projection, in Continuity.Partial.Neighborhood]
GBI [definition, in Continuity.BredeHerbelin.brede_herbelin]
GBI_BI_alt [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_inconsistent [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_BI_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.Magic.X [variable, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.Magic [section, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺s _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec [section, in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GBI_GCI [lemma, in Continuity.BI]
GBI_GCI_Fail [lemma, in Continuity.BI]
GDC [definition, in Continuity.BredeHerbelin.brede_herbelin]
GDC_inconsistent [lemma, in Continuity.BredeHerbelin.brede_herbelin]
GDC_gen [section, in Continuity.BredeHerbelin.brede_herbelin]
GDC_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [notation, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.Q [variable, in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition [section, in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction [section, in Continuity.BI]
GeneralisedBarInduction.A [variable, in Continuity.BI]
GeneralisedBarInduction.HGBI [variable, in Continuity.BI]
GeneralisedBarInduction.Q [variable, in Continuity.BI]
GeneralisedBarInduction.R [variable, in Continuity.BI]
generalize_pBIT_iff_pBIT [lemma, in Continuity.Partial.DialogueTree]
GI [constructor, in Continuity.Shared.mu_nat]
GoodList [constructor, in Continuity.Partial.DialogueTree]
good_list_extend_after [lemma, in Continuity.Partial.DialogueTree]
good_list_extend_before [lemma, in Continuity.Partial.DialogueTree]
good_list_extract [lemma, in Continuity.Partial.DialogueTree]
good_list_ind [definition, in Continuity.Partial.DialogueTree]
good_list [inductive, in Continuity.Partial.DialogueTree]
G_zero [lemma, in Continuity.Shared.mu_nat]
G_sig [lemma, in Continuity.Shared.mu_nat]
G_sind [definition, in Continuity.Shared.mu_nat]
G_rec [definition, in Continuity.Shared.mu_nat]
G_ind [definition, in Continuity.Shared.mu_nat]
G_rect [definition, in Continuity.Shared.mu_nat]

H

hasvalue [projection, in Continuity.Shared.partial]
hasvalue_det [projection, in Continuity.Shared.partial]
hereditarily_pbarred_ind' [definition, in Continuity.Partial.Neighborhood]
hereditarily_pbarred_sind [definition, in Continuity.Partial.Neighborhood]
hereditarily_pbarred_ind [definition, in Continuity.Partial.Neighborhood]
hereditarily_pbarred [inductive, in Continuity.Partial.Neighborhood]
hereditarily_pbarred_rect [definition, in Continuity.Partial.DialogueTree]
hereditarily_pbarred_ind [definition, in Continuity.Partial.DialogueTree]
hereditarily_pbarred [inductive, in Continuity.Partial.DialogueTree]
hereditary [lemma, in Continuity.Partial.DialogueTree]
hereditary_closure_rect [lemma, in Continuity.extra_principles]
hereditary_closure_Acc [lemma, in Continuity.extra_principles]
hereditary_closure_sind [definition, in Continuity.extra_principles]
hereditary_closure_ind [definition, in Continuity.extra_principles]
hereditary_sons [constructor, in Continuity.extra_principles]
hereditary_self [constructor, in Continuity.extra_principles]
hereditary_closure [inductive, in Continuity.extra_principles]
hereditary_closure_sind [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rec [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_ind [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rect [definition, in Continuity.BredeHerbelin.minimal_example]
hereditary_sons [constructor, in Continuity.BredeHerbelin.minimal_example]
hereditary_self [constructor, in Continuity.BredeHerbelin.minimal_example]
hereditary_closure [inductive, in Continuity.BredeHerbelin.minimal_example]
hered_mon_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
hered_mon_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
hered_mon [inductive, in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Hgamma [projection, in Continuity.Partial.Neighborhood]
Hpbar [constructor, in Continuity.Partial.Neighborhood]
Hpbar [constructor, in Continuity.Partial.DialogueTree]
Hptree_path [projection, in Continuity.Partial.Neighborhood]
Hptree_branch [projection, in Continuity.Partial.Neighborhood]
Hptree_path [projection, in Continuity.Partial.DialogueTree]
Hptree_branch [projection, in Continuity.Partial.DialogueTree]
Htau [projection, in Continuity.Partial.DialogueTree]

I

ibeta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
ieta [constructor, in Continuity.BredeHerbelin.brede_herbelin]
ieval [definition, in Continuity.continuity_zoo_Prop]
ieval_finapp_one_step_fuel [lemma, in Continuity.BI]
ieval_finapp_trace [lemma, in Continuity.BI]
ieval_trace [definition, in Continuity.BI]
ieval_finapp_monotone_ask_list_nomorefuel [lemma, in Continuity.BI]
ieval_finapp_monotone_ask_fuel [lemma, in Continuity.BI]
ieval_finapp_monotone_ask_list [lemma, in Continuity.BI]
ieval_finapp_monotone_output_fuel [lemma, in Continuity.BI]
ieval_finapp_monotone_output_list [lemma, in Continuity.BI]
ieval_finapp [definition, in Continuity.BI]
ieval_output_unique [lemma, in Continuity.continuity_zoo_Prop]
implementation [module, in Continuity.Shared.partial]
implementation.Allfalse [constructor, in Continuity.Shared.partial]
implementation.bind [definition, in Continuity.Shared.partial]
implementation.bind_hasvalue_imp [lemma, in Continuity.Shared.partial]
implementation.Diverged [constructor, in Continuity.Shared.partial]
implementation.equiv [definition, in Continuity.Shared.partial]
implementation.hasvalue [definition, in Continuity.Shared.partial]
implementation.hasvalue_det [lemma, in Continuity.Shared.partial]
implementation.list_max_lookup [lemma, in Continuity.Shared.partial]
implementation.lookup_seq [lemma, in Continuity.Shared.partial]
implementation.lt_list' [lemma, in Continuity.Shared.partial]
implementation.lt_list [lemma, in Continuity.Shared.partial]
implementation.monotonic_functions [instance, in Continuity.Shared.partial]
implementation.mu [definition, in Continuity.Shared.partial]
implementation.mu_hasvalue_imp [lemma, in Continuity.Shared.partial]
implementation.mu_fun_spec [lemma, in Continuity.Shared.partial]
implementation.mu_fun [definition, in Continuity.Shared.partial]
implementation.part [record, in Continuity.Shared.partial]
implementation.res [inductive, in Continuity.Shared.partial]
implementation.res_sind [definition, in Continuity.Shared.partial]
implementation.res_rec [definition, in Continuity.Shared.partial]
implementation.res_ind [definition, in Continuity.Shared.partial]
implementation.res_rect [definition, in Continuity.Shared.partial]
implementation.ret [definition, in Continuity.Shared.partial]
implementation.ret_hasvalue [lemma, in Continuity.Shared.partial]
implementation.seval [definition, in Continuity.Shared.partial]
implementation.seval_hasvalue_imp [lemma, in Continuity.Shared.partial]
implementation.seval_mono [lemma, in Continuity.Shared.partial]
implementation.spec_fun [projection, in Continuity.Shared.partial]
implementation.ter [definition, in Continuity.Shared.partial]
implementation.the_fun [projection, in Continuity.Shared.partial]
implementation.Trueat [constructor, in Continuity.Shared.partial]
implementation.undef [definition, in Continuity.Shared.partial]
implementation.undef_hasvalue [lemma, in Continuity.Shared.partial]
inclP [lemma, in Continuity.Util]
included_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
incl_iota_max [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inconsistent [lemma, in Continuity.Classical]
indbarred [inductive, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_Down_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec [inductive, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
indbarred_fun_list_itree_indbarredP [lemma, in Continuity.BI]
indbarred_fun_list_itree_indbarredP_aux [lemma, in Continuity.BI]
inductively_barred_indbarred_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred_Down_dual [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred [definition, in Continuity.extra_principles]
InP [lemma, in Continuity.Util]
Intensional_Dialogue.funext [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.R [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.A [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.Q [variable, in Continuity.continuity_zoo_Prop]
Intensional_Dialogue [section, in Continuity.continuity_zoo_Prop]
interrogation [inductive, in Continuity.continuity_zoo_Prop]
interrogation_equiv_eval_ext_tree [lemma, in Continuity.continuity_zoo_Prop]
interrogation_app [lemma, in Continuity.continuity_zoo_Prop]
interrogation_ext [lemma, in Continuity.continuity_zoo_Prop]
interrogation_cons [lemma, in Continuity.continuity_zoo_Prop]
interrogation_plus [lemma, in Continuity.continuity_zoo_Prop]
interrogation_sind [definition, in Continuity.continuity_zoo_Prop]
interrogation_ind [definition, in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree_one_step [lemma, in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
int_dialogue_cont_to_dialogue_cont [lemma, in Continuity.continuity_zoo_Prop]
int_dialogue_cont [definition, in Continuity.continuity_zoo_Prop]
inverse [constructor, in Continuity.BredeHerbelin.cantor]
inversion_ask [lemma, in Continuity.continuity_zoo_Prop]
in_iota [lemma, in Continuity.BredeHerbelin.brede_herbelin]
in_map [lemma, in Continuity.BredeHerbelin.brede_herbelin]
In_eval_list [lemma, in Continuity.BI]
iota_rcons [lemma, in Continuity.Util]
is_tree [definition, in Continuity.BredeHerbelin.brede_herbelin]
is_fun_rcons_notin_dom [lemma, in Continuity.BI]
is_fun_cons_notin_dom [lemma, in Continuity.BI]
is_fun_cat_notin_dom [lemma, in Continuity.BI]
is_fun_list_incl [lemma, in Continuity.BI]
is_fun_map [lemma, in Continuity.BI]
is_fun_list [definition, in Continuity.BI]
is_dialogue_to_dialogue [lemma, in Continuity.continuity_zoo_Prop]
is_dialogue_to_dialogue_ext [lemma, in Continuity.continuity_zoo_Prop]
is_dialogue_sind [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_rec [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_ind [definition, in Continuity.continuity_zoo_Prop]
is_dialogue_rect [definition, in Continuity.continuity_zoo_Prop]
is_dialogue [inductive, in Continuity.continuity_zoo_Prop]
itree [abbreviation, in Continuity.Brouwer_ext]
Itree [abbreviation, in Continuity.BI]
Itree [inductive, in Continuity.continuity_zoo_Prop]
itree [inductive, in Continuity.continuity_zoo_Prop]
itree_to_Bitree_cont [lemma, in Continuity.Brouwer_ext]
itree_to_BitreeP [lemma, in Continuity.Brouwer_ext]
itree_to_Bitree_seq [lemma, in Continuity.Brouwer_ext]
itree_to_Bitree [definition, in Continuity.Brouwer_ext]
itree_indbarredP_change_fuel [lemma, in Continuity.BI]
itree_indbarredP_monotone [lemma, in Continuity.BI]
itree_indbarred_spec [lemma, in Continuity.BI]
itree_indbarredP_ind [lemma, in Continuity.BI]
itree_indbarredP_rect [definition, in Continuity.BI]
itree_in [constructor, in Continuity.BI]
itree_indbarredP [inductive, in Continuity.BI]
itree_indbarred_dialogue [lemma, in Continuity.BI]
itree_indbarred_dialogue_aux [lemma, in Continuity.BI]
itree_indbarred_sind [definition, in Continuity.BI]
itree_indbarred_rec [definition, in Continuity.BI]
itree_indbarred_ind [definition, in Continuity.BI]
itree_indbarred_rect [definition, in Continuity.BI]
itree_beta [constructor, in Continuity.BI]
itree_succ [constructor, in Continuity.BI]
itree_eta [constructor, in Continuity.BI]
itree_indbarred [inductive, in Continuity.BI]

K

Kawai [section, in Continuity.kawai2018]
Kawai.A [variable, in Continuity.kawai2018]
Kawai.R [variable, in Continuity.kawai2018]
kawai2018 [library]
K0K [lemma, in Continuity.kawai2018]
K0K_aux [lemma, in Continuity.kawai2018]

L

least [definition, in Continuity.Shared.mu_nat]
list_max_spec [lemma, in Continuity.Shared.partial]
list_to_dialogue_eq [lemma, in Continuity.continuity_zoo_Prop]
list_to_dialogue_deval_eq [lemma, in Continuity.continuity_zoo_Prop]
list_to_cantor_swap [lemma, in Continuity.continuity_zoo_Prop]
list_to_dialogue [definition, in Continuity.continuity_zoo_Prop]
list_to_cantor [definition, in Continuity.continuity_zoo_Prop]
lots_of_separation [lemma, in Continuity.Partial.Modulus]
lpo [definition, in Continuity.Partial.Modulus]
lpo_cpo_cont_is_monotonic_mod_cont_nat [lemma, in Continuity.Partial.Modulus]
lpo_cpo_cont_is_strong_mod_cont_nat [lemma, in Continuity.Partial.Modulus]
lpo_monotonic_mod_fn_is_strong_mod_fn [lemma, in Continuity.Partial.Modulus]
lpo_monotonic_mod_is_strong_mod [lemma, in Continuity.Partial.Modulus]

M

make_well_founded_is_well_founded [lemma, in Continuity.Partial.Neighborhood]
make_well_founded_is_monotonic [lemma, in Continuity.Partial.Neighborhood]
make_well_founded_preserves_neighborhood [lemma, in Continuity.Partial.Neighborhood]
make_well_founded [definition, in Continuity.Partial.Neighborhood]
map_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]
mem_fixed_magic [lemma, in Continuity.BredeHerbelin.brede_herbelin]
mem_snd_in [definition, in Continuity.Partial.DialogueTree]
mem_fst_dec [lemma, in Continuity.Partial.DialogueTree]
MinEx [section, in Continuity.BredeHerbelin.minimal_example]
MinEx.B [variable, in Continuity.BredeHerbelin.minimal_example]
minimal_example [library]
mkpart [definition, in Continuity.Shared.partial]
mkpart_hasvalue [lemma, in Continuity.Shared.partial]
mkpart_hasvalue2 [lemma, in Continuity.Shared.partial]
mkpart_hasvalue1 [lemma, in Continuity.Shared.partial]
mkproof_ter [lemma, in Continuity.Shared.partial]
modulus [definition, in Continuity.Partial.Modulus]
Modulus [section, in Continuity.continuity_zoo_Prop]
modulus [definition, in Continuity.continuity_zoo_Prop]
Modulus [library]
modulus_of_cpo_nat_is_modulus [lemma, in Continuity.Partial.Modulus]
modulus_of_cpo_nat [definition, in Continuity.Partial.Modulus]
modulus_cont_to_extensional [lemma, in Continuity.Partial.Modulus]
modulus_to_weak_modulus [lemma, in Continuity.Partial.Modulus]
modulus_fn_to_have_modulus [lemma, in Continuity.Partial.Modulus]
modulus_at [definition, in Continuity.Partial.Modulus]
modulus_to_ext_tree [definition, in Continuity.continuity_zoo_Prop]
modulus_at_nat_to_modulus_at [lemma, in Continuity.continuity_zoo_Prop]
modulus_at_to_modulus_at_nat [lemma, in Continuity.continuity_zoo_Prop]
modulus_ex_modulus [lemma, in Continuity.continuity_zoo_Prop]
modulus_nat [definition, in Continuity.continuity_zoo_Prop]
modulus_at_nat [definition, in Continuity.continuity_zoo_Prop]
modulus_at [definition, in Continuity.continuity_zoo_Prop]
modulus' [definition, in Continuity.Partial.Modulus]
Modulus.A [variable, in Continuity.continuity_zoo_Prop]
Modulus.Q [variable, in Continuity.continuity_zoo_Prop]
Modulus.R [variable, in Continuity.continuity_zoo_Prop]
mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
mon [constructor, in Continuity.BredeHerbelin.minimal_example]
monotone [definition, in Continuity.BredeHerbelin.brede_herbelin]
monotone_bar_extend_true [lemma, in Continuity.Partial.Neighborhood]
monotone_ABUp_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
monotonic [definition, in Continuity.Partial.Modulus]
monotonic [definition, in Continuity.Shared.partial]
monotonic_to_extensional [lemma, in Continuity.Partial.Modulus]
monotonic_seq [definition, in Continuity.Partial.Modulus]
monotonic_modulus_to_modulus [lemma, in Continuity.Partial.Modulus]
monotonic_self_modulus_cont [definition, in Continuity.Partial.Modulus]
monotonic_cont_modulus_cont [definition, in Continuity.Partial.Modulus]
monotonic_modulus_cont [definition, in Continuity.Partial.Modulus]
monotonic_modulus [definition, in Continuity.Partial.Modulus]
monotonic_agnostic [lemma, in Continuity.Shared.partial]
monot_barred [lemma, in Continuity.BredeHerbelin.brede_herbelin]
MP [lemma, in Continuity.Classical]
mu [projection, in Continuity.Shared.partial]
mu_nat_dep_irrel [lemma, in Continuity.Shared.mu_nat]
mu_nat_dep_min [lemma, in Continuity.Shared.mu_nat]
mu_nat_dep_least [definition, in Continuity.Shared.mu_nat]
mu_nat_dep [definition, in Continuity.Shared.mu_nat]
mu_nat' [lemma, in Continuity.Shared.mu_nat]
mu_nat [lemma, in Continuity.Shared.mu_nat]
mu_tot_ter [lemma, in Continuity.Shared.partial]
mu_tot_hasvalue [lemma, in Continuity.Shared.partial]
mu_tot [definition, in Continuity.Shared.partial]
mu_ter [lemma, in Continuity.Shared.partial]
mu_hasvalue [projection, in Continuity.Shared.partial]
mu_fold_spec [lemma, in Continuity.Partial.DialogueTree]
mu_fold [definition, in Continuity.Partial.DialogueTree]
mu_opt_hasvalue [lemma, in Continuity.Partial.Common]
mu_opt_ter [lemma, in Continuity.Partial.Common]
mu_opt [definition, in Continuity.Partial.Common]
mu_nat [library]

N

nat_queries.R [variable, in Continuity.continuity_zoo_Prop]
nat_queries.A [variable, in Continuity.continuity_zoo_Prop]
nat_queries [section, in Continuity.continuity_zoo_Prop]
Neighborhood [library]
neighborhoodfunction [definition, in Continuity.kawai2018]
neighborhood_to_brouwer_op_pbit [lemma, in Continuity.Partial.Neighborhood]
neighborhood_canonical_correct [lemma, in Continuity.Partial.Neighborhood]
neighborhood_canonical [definition, in Continuity.Partial.Neighborhood]
neighborhood_for_squash [lemma, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_wf [definition, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_strict [lemma, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_hasvalue_none [lemma, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_hasvalue_some [lemma, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_ter [lemma, in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify [definition, in Continuity.Partial.Neighborhood]
neighborhood_cont_is_well_founded_neighborhood_cont [lemma, in Continuity.Partial.Neighborhood]
neighborhood_cont [definition, in Continuity.Partial.Neighborhood]
neighborhood_for [definition, in Continuity.Partial.Neighborhood]
neighborhood_fun [definition, in Continuity.Partial.Neighborhood]
neighborhood_cont_to_tree_fun_cont [lemma, in Continuity.Partial.TreeFunction]
neighborhood_fun_to_tree_fun_spec [lemma, in Continuity.Partial.TreeFunction]
neighborhood_to_tree_trace [lemma, in Continuity.Partial.TreeFunction]
neighborhood_fun_to_tree_fun [definition, in Continuity.Partial.TreeFunction]
neighborhood_wf_valid_Bext_tree [lemma, in Continuity.kawai2018]
neigh_cont_iff_Bcoind_dial_cont [lemma, in Continuity.kawai2018]
neigh_cont_to_Bcoind_dial_cont [lemma, in Continuity.kawai2018]
neigh_to_Bitree [definition, in Continuity.kawai2018]
neigh_cont_Btree_fun_cont [lemma, in Continuity.kawai2018]
neigh_realises_Beval [lemma, in Continuity.kawai2018]
neigh_realises_Beval_aux [lemma, in Continuity.kawai2018]
neigh_cont [definition, in Continuity.kawai2018]
neigh_realises [definition, in Continuity.kawai2018]
NoDupP [lemma, in Continuity.Util]
NoQuestions [constructor, in Continuity.continuity_zoo_Prop]
normalized_good_list_nodup [lemma, in Continuity.Partial.DialogueTree]
normalized_strict_well_founded_tree_fun_cont [definition, in Continuity.Partial.DialogueTree]
normalized_strict_well_founded_tree_fun_for [definition, in Continuity.Partial.DialogueTree]
normalized_ext_tree [definition, in Continuity.Partial.DialogueTree]
normalize_is_normalized [lemma, in Continuity.Partial.DialogueTree]
normalize_ext_tree [definition, in Continuity.Partial.DialogueTree]
normask [constructor, in Continuity.continuity_zoo_Prop]
normret [constructor, in Continuity.continuity_zoo_Prop]
normsucccons [constructor, in Continuity.continuity_zoo_Prop]
normsuccnil [constructor, in Continuity.continuity_zoo_Prop]
normzerocons [constructor, in Continuity.continuity_zoo_Prop]
normzeronil [constructor, in Continuity.continuity_zoo_Prop]
norm1 [inductive, in Continuity.continuity_zoo_Prop]
norm1_sind [definition, in Continuity.continuity_zoo_Prop]
norm1_rec [definition, in Continuity.continuity_zoo_Prop]
norm1_ind [definition, in Continuity.continuity_zoo_Prop]
norm1_rect [definition, in Continuity.continuity_zoo_Prop]
norm2 [inductive, in Continuity.continuity_zoo_Prop]
norm2_sind [definition, in Continuity.continuity_zoo_Prop]
norm2_rec [definition, in Continuity.continuity_zoo_Prop]
norm2_ind [definition, in Continuity.continuity_zoo_Prop]
norm2_rect [definition, in Continuity.continuity_zoo_Prop]
Notallin [lemma, in Continuity.Util]
Now [definition, in Continuity.Partial.Delay]
NowF [constructor, in Continuity.Partial.Delay]
nth_error_split_lr [lemma, in Continuity.Partial.DialogueTree]
nth_undef_app_r [lemma, in Continuity.Partial.Common]
nth_undef [definition, in Continuity.Partial.Common]
nth_error_app [lemma, in Continuity.Partial.Common]
nth_nth' [lemma, in Continuity.BI]
nth' [definition, in Continuity.BI]
n_comp_n_plus [lemma, in Continuity.continuity_zoo_Prop]
n_comp [definition, in Continuity.continuity_zoo_Prop]

O

omega_cpo [definition, in Continuity.Partial.Modulus]
ord [definition, in Continuity.BredeHerbelin.brede_herbelin]
Ord [section, in Continuity.BredeHerbelin.brede_herbelin]
ordP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_iota_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_map_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size_aux [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_incl' [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_NoDup [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_in_2 [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_sizeu_notin [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_notin [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_incl [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_nth_in [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_in [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_nth [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_rcons [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_size [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_drop [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_take [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_cat [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_inj [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_map_snd [lemma, in Continuity.BredeHerbelin.brede_herbelin]
ord_aux [definition, in Continuity.BredeHerbelin.brede_herbelin]
Ord.A [variable, in Continuity.BredeHerbelin.brede_herbelin]
Output [constructor, in Continuity.Partial.DialogueTree]
output [constructor, in Continuity.continuity_zoo_Prop]

P

padded_prefix [definition, in Continuity.continuity_zoo_Prop]
padded_seq [definition, in Continuity.continuity_zoo_Prop]
par [definition, in Continuity.Shared.partial]
part [projection, in Continuity.Shared.partial]
partial [library]
partiality [record, in Continuity.Shared.partial]
PartialTactics [module, in Continuity.Shared.partial]
PartialZoo [section, in Continuity.Partial.Modulus]
PartialZoo [section, in Continuity.Partial.Neighborhood]
PartialZoo [section, in Continuity.Partial.TreeFunction]
PartialZoo [section, in Continuity.Partial.Common]
PartialZoo.Partiality [variable, in Continuity.Partial.Modulus]
PartialZoo.Partiality [variable, in Continuity.Partial.Neighborhood]
PartialZoo.Partiality [variable, in Continuity.Partial.TreeFunction]
PartialZoo.Partiality [variable, in Continuity.Partial.Common]
part_equiv_Equivalence [instance, in Continuity.Partial.Delay]
part_equiv_Equivalence [instance, in Continuity.Shared.partial]
part_fold_preserves [lemma, in Continuity.Partial.DialogueTree]
part_fold_ter [lemma, in Continuity.Partial.DialogueTree]
part_fold [definition, in Continuity.Partial.DialogueTree]
par_hasvalue3 [lemma, in Continuity.Shared.partial]
par_hasvalue2 [lemma, in Continuity.Shared.partial]
par_hasvalue1 [lemma, in Continuity.Shared.partial]
pbarred [definition, in Continuity.Partial.Neighborhood]
pbarred [definition, in Continuity.Partial.DialogueTree]
pBIT [definition, in Continuity.Partial.Neighborhood]
pBIT [definition, in Continuity.Partial.DialogueTree]
pbit_neighborhood_cont_to_brouwer_cont_nat [lemma, in Continuity.Partial.Neighborhood]
pbit_neighborhood_cont_to_brouwer_cont [lemma, in Continuity.Partial.Neighborhood]
pbit_neighborhood_to_brouwer_op [lemma, in Continuity.Partial.Neighborhood]
pBIT_ext_tree_to_dialogue_tree [lemma, in Continuity.Partial.DialogueTree]
pcomputes [definition, in Continuity.Shared.partial]
permutes_quantifier_strict_well_founded_brouwer_operation [lemma, in Continuity.Partial.Neighborhood]
por [definition, in Continuity.Partial.Modulus]
por_true [lemma, in Continuity.Partial.Modulus]
por_false [lemma, in Continuity.Partial.Modulus]
pred_to_fun [definition, in Continuity.BI]
pred_to_Bitree_aux [definition, in Continuity.BI]
pref [definition, in Continuity.continuity_zoo_Prop]
prefix [definition, in Continuity.extra_principles]
pref_a_Bieval [lemma, in Continuity.BI]
pref_a_beval [lemma, in Continuity.BI]
pref_a_alpha [lemma, in Continuity.BI]
pref_a_eq [lemma, in Continuity.BI]
pref_a [definition, in Continuity.BI]
pref_padded_prefix [lemma, in Continuity.continuity_zoo_Prop]
pref_le_eq [lemma, in Continuity.continuity_zoo_Prop]
proof_ter_spec [definition, in Continuity.Partial.Common]
proof_ter [definition, in Continuity.Partial.Common]
prune [constructor, in Continuity.BredeHerbelin.brede_herbelin]
prune [constructor, in Continuity.BredeHerbelin.minimal_example]
pruning [inductive, in Continuity.BredeHerbelin.brede_herbelin]
pruning [inductive, in Continuity.BredeHerbelin.minimal_example]
pruning_pruning_Downarbor [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_ABapprox_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_TtoP_ABapprox [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_cat [lemma, in Continuity.BredeHerbelin.brede_herbelin]
pruning_arbor [lemma, in Continuity.BredeHerbelin.minimal_example]
ptot [constructor, in Continuity.BredeHerbelin.brede_herbelin]
PtoT [inductive, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_ret [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_inv [lemma, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_dual [definition, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
PtoT_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
ptree_restrict [lemma, in Continuity.Partial.Neighborhood]
ptree_branch_extend [lemma, in Continuity.Partial.Neighborhood]
ptree_path [projection, in Continuity.Partial.Neighborhood]
ptree_branch [projection, in Continuity.Partial.Neighborhood]
ptree_path [projection, in Continuity.Partial.DialogueTree]
ptree_branch [projection, in Continuity.Partial.DialogueTree]
P_ABUp_PtoTB [lemma, in Continuity.BredeHerbelin.brede_herbelin]
P_ABDown_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]
P_Uparbor_PtoT [lemma, in Continuity.BredeHerbelin.brede_herbelin]

Q

Q [abbreviation, in Continuity.Brouwer_ext]
Q [abbreviation, in Continuity.Brouwer_ext]
Q [abbreviation, in Continuity.BI]
Q [abbreviation, in Continuity.BI]
Q [abbreviation, in Continuity.continuity_zoo_Prop]
Q [abbreviation, in Continuity.continuity_zoo_Prop]
Q [abbreviation, in Continuity.continuity_zoo_Prop]

R

R [abbreviation, in Continuity.BI]
rebuild_first_values_app [lemma, in Continuity.Partial.DialogueTree]
rebuild_first_values [definition, in Continuity.Partial.DialogueTree]
reflectspfn [definition, in Continuity.Partial.Common]
reflect1 [definition, in Continuity.continuity_zoo_Prop]
reflect2 [definition, in Continuity.continuity_zoo_Prop]
reify [lemma, in Continuity.continuity_zoo_Prop]
reify2 [lemma, in Continuity.continuity_zoo_Prop]
result [inductive, in Continuity.continuity_zoo_Prop]
result_sind [definition, in Continuity.continuity_zoo_Prop]
result_rec [definition, in Continuity.continuity_zoo_Prop]
result_ind [definition, in Continuity.continuity_zoo_Prop]
result_rect [definition, in Continuity.continuity_zoo_Prop]
ret [projection, in Continuity.Shared.partial]
ret [constructor, in Continuity.continuity_zoo_Prop]
Ret [constructor, in Continuity.continuity_zoo_Prop]
retraction_Lawvere [lemma, in Continuity.BredeHerbelin.cantor]
retract_of [definition, in Continuity.Classical]
ret_hasvalue_iff [lemma, in Continuity.Shared.partial]
ret_hasvalue' [lemma, in Continuity.Shared.partial]
ret_hasvalue_inv [lemma, in Continuity.Shared.partial]
ret_hasvalue [projection, in Continuity.Shared.partial]
rev_combine [lemma, in Continuity.Partial.DialogueTree]
rev_firstn_rev [lemma, in Continuity.Partial.Common]
right_invertible_sind [definition, in Continuity.BredeHerbelin.cantor]
right_invertible_ind [definition, in Continuity.BredeHerbelin.cantor]
right_invertible [inductive, in Continuity.BredeHerbelin.cantor]

S

sec [section, in Continuity.continuity_zoo_Prop]
sec.A [variable, in Continuity.continuity_zoo_Prop]
sec.R [variable, in Continuity.continuity_zoo_Prop]
sefl_mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
self_mod_weak_continuous' [definition, in Continuity.Partial.Modulus]
self_mod_to_self_mod_weak [lemma, in Continuity.Partial.Modulus]
self_mod_weak_continuous [definition, in Continuity.Partial.Modulus]
self_modulus_cont_to_continuous_modulus_cont [lemma, in Continuity.Partial.Modulus]
self_modulus_equiv [lemma, in Continuity.Partial.Modulus]
self_modulus'_cont [definition, in Continuity.Partial.Modulus]
self_modulus_cont [definition, in Continuity.Partial.Modulus]
self_mod_cont_not_tree_fun_cont [lemma, in Continuity.Partial.TreeFunction]
self_modulus_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
self_modulus_cont [definition, in Continuity.continuity_zoo_Prop]
seval [projection, in Continuity.Shared.partial]
seval_hasvalue [projection, in Continuity.Shared.partial]
seval_mono [projection, in Continuity.Shared.partial]
sigma1 [definition, in Continuity.Partial.Common]
sigma1pfn [lemma, in Continuity.Partial.Common]
sigma1_tree [record, in Continuity.Partial.Neighborhood]
sigma1_tree [record, in Continuity.Partial.DialogueTree]
size_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
sons_mon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
spit [constructor, in Continuity.continuity_zoo_Prop]
split_app [lemma, in Continuity.Partial.DialogueTree]
strictify_self_mod_weak [lemma, in Continuity.Partial.Modulus]
strictify_continuous_mod_weak [lemma, in Continuity.Partial.Modulus]
strictify_weak_modulus [lemma, in Continuity.Partial.Modulus]
strictify_modulus_at [lemma, in Continuity.Partial.Modulus]
strictify_modulus_ter' [lemma, in Continuity.Partial.Modulus]
strictify_modulus_hasvalue' [lemma, in Continuity.Partial.Modulus]
strictify_modulus_hasvalue [lemma, in Continuity.Partial.Modulus]
strictify_modulus_ter [lemma, in Continuity.Partial.Modulus]
strictify_modulus [definition, in Continuity.Partial.Modulus]
strictify_preserves_neighborhood [lemma, in Continuity.Partial.Neighborhood]
strict_modulus [lemma, in Continuity.Partial.Modulus]
strict_well_founded_neighborhood_for_squash [lemma, in Continuity.Partial.Neighborhood]
strict_well_founded_neighborhood_cont [definition, in Continuity.Partial.Neighborhood]
strict_well_founded_neighborhood_for [definition, in Continuity.Partial.Neighborhood]
strict_neighborhood [definition, in Continuity.Partial.Neighborhood]
strict_well_founded_tree_fun_for_squash [lemma, in Continuity.Partial.DialogueTree]
strict_well_founded_tree_fun_cont [definition, in Continuity.Partial.TreeFunction]
strict_well_founded_tree_fun_for [definition, in Continuity.Partial.TreeFunction]
strict_ext_tree [definition, in Continuity.Partial.TreeFunction]
strong_modulus_to_monotonic_modulus [lemma, in Continuity.Partial.Modulus]
strong_self_modulus_cont [definition, in Continuity.Partial.Modulus]
strong_cont_modulus_cont [definition, in Continuity.Partial.Modulus]
strong_modulus_cont [definition, in Continuity.Partial.Modulus]
strong_modulus [definition, in Continuity.Partial.Modulus]
sup [definition, in Continuity.Partial.Modulus]

T

tabulate [definition, in Continuity.Partial.Common]
tabulate_equiv [lemma, in Continuity.Partial.Common]
tabulate_map [lemma, in Continuity.Partial.Common]
tabulate_length [lemma, in Continuity.Partial.Common]
tabulate_add [lemma, in Continuity.Partial.Common]
tabulate_succ' [lemma, in Continuity.Partial.Common]
tabulate_succ [lemma, in Continuity.Partial.Common]
tabulate_same [lemma, in Continuity.Partial.Common]
tabulate_aux [definition, in Continuity.Partial.Common]
Tarbor [constructor, in Continuity.BredeHerbelin.brede_herbelin]
tau [projection, in Continuity.Partial.DialogueTree]
Tau [constructor, in Continuity.continuity_zoo_Prop]
tbeta [constructor, in Continuity.continuity_zoo_Prop]
Technical [section, in Continuity.BredeHerbelin.brede_herbelin]
ter [definition, in Continuity.Shared.partial]
termination_tree [definition, in Continuity.Partial.Neighborhood]
termination_tree [definition, in Continuity.Partial.DialogueTree]
test [lemma, in Continuity.BredeHerbelin.minimal_example]
teta [constructor, in Continuity.continuity_zoo_Prop]
Theorem5 [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Theorem5rev [lemma, in Continuity.BredeHerbelin.brede_herbelin]
the_func_proof [projection, in Continuity.Shared.partial]
the_rel [projection, in Continuity.Shared.partial]
Tmon [constructor, in Continuity.BredeHerbelin.brede_herbelin]
Tmon_size [constructor, in Continuity.BredeHerbelin.brede_herbelin]
top [definition, in Continuity.BredeHerbelin.brede_herbelin]
top_cons [lemma, in Continuity.BredeHerbelin.brede_herbelin]
total [definition, in Continuity.Shared.partial]
TreeFunction [section, in Continuity.continuity_zoo_Prop]
TreeFunction [library]
TreeFunction.A [variable, in Continuity.continuity_zoo_Prop]
TreeFunction.Q [variable, in Continuity.continuity_zoo_Prop]
TreeFunction.R [variable, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_Brouwer [lemma, in Continuity.Brouwer_ext]
tree_fun_cont_to_Brouwer_aux [lemma, in Continuity.Brouwer_ext]
tree_fun_for_squash [lemma, in Continuity.Partial.DialogueTree]
tree_fun_cont_to_strong_self_modulus_cont [lemma, in Continuity.Partial.TreeFunction]
tree_fun_for_good_def [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_strong_self_modulus [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_strong_modulus' [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_restrict [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_restrict' [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_equiv_trace [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_strong_modulus_fn' [definition, in Continuity.Partial.TreeFunction]
tree_fun_cont_not_neighborhood_cont [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_to_self_modulus_cont [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_self_modulus [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_modulus [lemma, in Continuity.Partial.TreeFunction]
tree_fun_cont_mod_fn [definition, in Continuity.Partial.TreeFunction]
tree_fun_trace_ter_fold [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_mod [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_mod [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_succ [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_succ [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_val [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_ter [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_det [lemma, in Continuity.Partial.TreeFunction]
tree_fun_trace [definition, in Continuity.Partial.TreeFunction]
tree_fun_trace_aux [definition, in Continuity.Partial.TreeFunction]
tree_fun_cont [definition, in Continuity.Partial.TreeFunction]
tree_fun_for [definition, in Continuity.Partial.TreeFunction]
tree_fun_cont_equiv_self_modulus_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_self_modulus_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_tree_fun_cont_valid [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_iff_coind_dial_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_coind_dial_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf_to_tree_fun_cont [lemma, in Continuity.continuity_zoo_Prop]
tree_fun_cont_valid [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont_via_interrogations [definition, in Continuity.continuity_zoo_Prop]
tree_fun_cont [definition, in Continuity.continuity_zoo_Prop]
TtoP [definition, in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_inv [lemma, in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_ret [definition, in Continuity.BredeHerbelin.brede_herbelin]
tuple [definition, in Continuity.Partial.Neighborhood]
tuple_to_list [definition, in Continuity.Partial.Neighborhood]
T14 [lemma, in Continuity.continuity_zoo_Prop]
T41 [lemma, in Continuity.continuity_zoo_Prop]

U

undef [projection, in Continuity.Shared.partial]
undef_hasvalue [projection, in Continuity.Shared.partial]
undef' [definition, in Continuity.Shared.partial]
undef'_hasvalue [lemma, in Continuity.Shared.partial]
unembed [definition, in Continuity.Shared.embed_nat]
unembedP [lemma, in Continuity.Shared.embed_nat]
uniform_is_dialogue [lemma, in Continuity.continuity_zoo_Prop]
uni_cont [definition, in Continuity.continuity_zoo_Prop]
Unnamed_thm [definition, in Continuity.Partial.Modulus]
unzip1_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
unzip2_ord [lemma, in Continuity.BredeHerbelin.brede_herbelin]
UpABarbor_is_tree [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Uparbor_PtoT_P [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation [inductive, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation [inductive, in Continuity.BredeHerbelin.minimal_example]
UpmonotonisationP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [definition, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_ind [definition, in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rec [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_ind [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rect [definition, in Continuity.BredeHerbelin.minimal_example]
Upmonot_monotone [lemma, in Continuity.BredeHerbelin.brede_herbelin]
Upmono_dec [lemma, in Continuity.BredeHerbelin.brede_herbelin]
upP [lemma, in Continuity.BredeHerbelin.brede_herbelin]
useless_hypothesis [lemma, in Continuity.kawai2018]
Util [library]

V

valid_cat [lemma, in Continuity.continuity_zoo_Prop]
valid_ext_tree [definition, in Continuity.continuity_zoo_Prop]
VectorEmbedding [module, in Continuity.Shared.embed_nat]
VectorEmbedding.nat_to_vec [definition, in Continuity.Shared.embed_nat]
VectorEmbedding.vec_nat_inv [lemma, in Continuity.Shared.embed_nat]
VectorEmbedding.vec_to_nat [definition, in Continuity.Shared.embed_nat]
vis [constructor, in Continuity.continuity_zoo_Prop]
Vis [constructor, in Continuity.continuity_zoo_Prop]

W

weak_modulus' [definition, in Continuity.Partial.Modulus]
weak_modulus [definition, in Continuity.Partial.Modulus]
well_founded_neighborhood_for_squash [lemma, in Continuity.Partial.Neighborhood]
well_founded_neighborhood_hasvalue [lemma, in Continuity.Partial.Neighborhood]
well_founded_neighborhood_cont [definition, in Continuity.Partial.Neighborhood]
well_founded_neighborhood_for [definition, in Continuity.Partial.Neighborhood]
well_founded_neighborhood [definition, in Continuity.Partial.Neighborhood]
well_founded_tree_fun_for_squash [lemma, in Continuity.Partial.DialogueTree]
well_founded_tree_fun_cont [definition, in Continuity.Partial.TreeFunction]
well_founded_tree_fun_for [definition, in Continuity.Partial.TreeFunction]
well_founded_ext_tree [definition, in Continuity.Partial.TreeFunction]
wf_Bext_tree [definition, in Continuity.Brouwer_ext]
wf_ext_tree [definition, in Continuity.continuity_zoo_Prop]
without_loss_of_generality_le_sym [lemma, in Continuity.Partial.DialogueTree]
WO [section, in Continuity.Shared.mu_nat]
WO.f [variable, in Continuity.Shared.mu_nat]

other

_ ↛ _ [notation, in Continuity.Shared.partial]
_ =! _ [notation, in Continuity.Shared.partial]

Notation Index

A

[ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]

D

[ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]

E

fun! ⟨ _ , _ ⟩ => _ [in Continuity.Shared.embed_nat]
⟨ _ , _ ⟩ [in Continuity.Shared.embed_nat]

G

⇑⁺s _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₑ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[ _ ]ₐ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
[| _ |] (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
↑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁺ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇓⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]
⇑⁻ _ (bh_scope) [in Continuity.BredeHerbelin.brede_herbelin]

other

_ ↛ _ [in Continuity.Shared.partial]
_ =! _ [in Continuity.Shared.partial]

Module Index

D

DelayPartialImplem [in Continuity.Partial.Delay]
DelayPartialImplem.Bind [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue [in Continuity.Partial.Delay]
DelayPartialImplem.Mu [in Continuity.Partial.Delay]
DelayPartialImplem.Seval [in Continuity.Partial.Delay]

E

EmbedNatNotations [in Continuity.Shared.embed_nat]

I

implementation [in Continuity.Shared.partial]

P

PartialTactics [in Continuity.Shared.partial]

V

VectorEmbedding [in Continuity.Shared.embed_nat]

Variable Index

A

Additional_Lemmas.A [in Continuity.BredeHerbelin.brede_herbelin]
assume_part.impl [in Continuity.Shared.partial]

B

BarInduction.A [in Continuity.BI]
BarInduction.dBI [in Continuity.BI]
BarInduction.R [in Continuity.BI]
BI_mon.A [in Continuity.BredeHerbelin.brede_herbelin]
Brouwer_interaction_trees.R [in Continuity.Brouwer_ext]
Brouwer_interaction_trees.A [in Continuity.Brouwer_ext]
Brouwer_ext_tree.R [in Continuity.Brouwer_ext]
Brouwer_ext_tree.A [in Continuity.Brouwer_ext]
Brouwer.A [in Continuity.continuity_zoo_Prop]
Brouwer.R [in Continuity.continuity_zoo_Prop]

C

Cantor.A [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.a0 [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.E [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.R [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.A [in Continuity.continuity_zoo_Prop]
Cantor.fix_types.Q [in Continuity.continuity_zoo_Prop]
Cantor.L [in Continuity.continuity_zoo_Prop]
Cantor.L_spec [in Continuity.continuity_zoo_Prop]
Cantor.Q [in Continuity.continuity_zoo_Prop]
Cantor.R [in Continuity.continuity_zoo_Prop]
cBI_implies_CI_fail.cBI [in Continuity.BI]
cBI_implies_CI_fail.R [in Continuity.BI]
cBI_implies_CI_fail.A [in Continuity.BI]
continuity_principles.R [in Continuity.continuity_zoo_Prop]
continuity_principles.A [in Continuity.continuity_zoo_Prop]
continuity_principles.Q [in Continuity.continuity_zoo_Prop]
ContinuousBarInduction.A [in Continuity.BI]
ContinuousBarInduction.CI [in Continuity.BI]
ContinuousBarInduction.R [in Continuity.BI]
ContinuousInduction.A [in Continuity.BI]
ContinuousInduction.CI [in Continuity.BI]

D

DC_GDC_BI_GBI.A [in Continuity.BredeHerbelin.brede_herbelin]

F

FinQuestion.A [in Continuity.continuity_zoo_Prop]
FinQuestion.L [in Continuity.continuity_zoo_Prop]
FinQuestion.L_spec [in Continuity.continuity_zoo_Prop]
FinQuestion.Q [in Continuity.continuity_zoo_Prop]
FinQuestion.R [in Continuity.continuity_zoo_Prop]

G

GBI_dec.Magic.X [in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec.A [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.A [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition.Q [in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction.A [in Continuity.BI]
GeneralisedBarInduction.HGBI [in Continuity.BI]
GeneralisedBarInduction.Q [in Continuity.BI]
GeneralisedBarInduction.R [in Continuity.BI]

I

Intensional_Dialogue.funext [in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.R [in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.A [in Continuity.continuity_zoo_Prop]
Intensional_Dialogue.Q [in Continuity.continuity_zoo_Prop]

K

Kawai.A [in Continuity.kawai2018]
Kawai.R [in Continuity.kawai2018]

M

MinEx.B [in Continuity.BredeHerbelin.minimal_example]
Modulus.A [in Continuity.continuity_zoo_Prop]
Modulus.Q [in Continuity.continuity_zoo_Prop]
Modulus.R [in Continuity.continuity_zoo_Prop]

N

nat_queries.R [in Continuity.continuity_zoo_Prop]
nat_queries.A [in Continuity.continuity_zoo_Prop]

O

Ord.A [in Continuity.BredeHerbelin.brede_herbelin]

P

PartialZoo.Partiality [in Continuity.Partial.Modulus]
PartialZoo.Partiality [in Continuity.Partial.Neighborhood]
PartialZoo.Partiality [in Continuity.Partial.TreeFunction]
PartialZoo.Partiality [in Continuity.Partial.Common]

S

sec.A [in Continuity.continuity_zoo_Prop]
sec.R [in Continuity.continuity_zoo_Prop]

T

TreeFunction.A [in Continuity.continuity_zoo_Prop]
TreeFunction.Q [in Continuity.continuity_zoo_Prop]
TreeFunction.R [in Continuity.continuity_zoo_Prop]

W

WO.f [in Continuity.Shared.mu_nat]

Library Index

B

BI
brede_herbelin
Brouwer_ext

C

cantor
Classical
Common
continuity_zoo_Prop

D

Delay
DialogueTree

E

embed_nat
extra_principles

K

kawai2018

M

minimal_example
Modulus
mu_nat

N

Neighborhood

P

partial

T

TreeFunction

U

Util

Lemma Index

A

ABapprox_PtoT_pruning [in Continuity.BredeHerbelin.brede_herbelin]
ABapprox_pruning_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_choicefun [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP_size_inf [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_PtoT_barred [in Continuity.BredeHerbelin.brede_herbelin]
ABbarred_barred_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_PtoT_choice [in Continuity.BredeHerbelin.brede_herbelin]
ABchoice_choice_TtoP [in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
ABDown_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
ABmonot_barred [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmono_size_dec [in Continuity.BredeHerbelin.brede_herbelin]
ABUpsize_monotone_size [in Continuity.BredeHerbelin.brede_herbelin]
ABUp_Up_dec [in Continuity.BredeHerbelin.brede_herbelin]
Add_induction_step [in Continuity.BI]
Add_cat [in Continuity.BI]
Add_rcons [in Continuity.BI]
all_strict_well_founded_neighborhood_are_brouwer_op_transfer [in Continuity.Partial.Neighborhood]
all_uniform [in Continuity.continuity_zoo_Prop]
approx_sup [in Continuity.Partial.Modulus]
approx_monotonic_seq [in Continuity.Partial.Modulus]
arbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]
associated_neighborhood_fun_to_associated_tree_fun [in Continuity.Partial.TreeFunction]

B

barred_ABbarred_PtoT_Up [in Continuity.BredeHerbelin.brede_herbelin]
barred_barred_Upmon [in Continuity.BredeHerbelin.brede_herbelin]
barred_ABbarred_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
barred_TtoP_ABbarred [in Continuity.BredeHerbelin.brede_herbelin]
barred_Bseq_cont [in Continuity.BI]
barred_Bseq_cont_aux [in Continuity.BI]
bar_to_strict_well_founded_neighborhood [in Continuity.Partial.Neighborhood]
bar_to_neighborhood [in Continuity.Partial.Neighborhood]
bar_to_well_founded_neighborhood_fun [in Continuity.Partial.Neighborhood]
BbetaP [in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont_to_neigh_cont [in Continuity.kawai2018]
Beval_ext_tree_monotone [in Continuity.Brouwer_ext]
Beval_ext_tree_output_unique [in Continuity.Brouwer_ext]
Beval_ext_tree_constant [in Continuity.Brouwer_ext]
Beval_ext_tree_map_aux [in Continuity.Brouwer_ext]
beval_list_modulus_at [in Continuity.BI]
beval_list_barred [in Continuity.BI]
beval_list_barred_aux [in Continuity.BI]
beval_list_mon [in Continuity.BI]
beval_ext [in Continuity.BI]
Bieval_output_unique [in Continuity.Brouwer_ext]
Bieval_monotone_plus [in Continuity.Brouwer_ext]
Bieval_monotone [in Continuity.Brouwer_ext]
Bieval_trace_inf [in Continuity.kawai2018]
Bieval_trace_Some [in Continuity.kawai2018]
Bieval_pred_trace [in Continuity.BI]
Bieval_trace_spec [in Continuity.BI]
Bieval_pred_to_Bitree_spec [in Continuity.BI]
bind_hasvalue_given [in Continuity.Shared.partial]
bind_ter' [in Continuity.Partial.Common]
bind_ter [in Continuity.Partial.Common]
Bitree_cont_to_itree_cont [in Continuity.Brouwer_ext]
Bitree_to_itreeP [in Continuity.Brouwer_ext]
Bitree_to_itreeP_aux [in Continuity.Brouwer_ext]
Bitree_to_option_Bieval [in Continuity.Brouwer_ext]
BI_GBI_alt [in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI_dec [in Continuity.BredeHerbelin.brede_herbelin]
BI_GBI [in Continuity.BredeHerbelin.brede_herbelin]
Bneigh_cont_equiv_dialogue_cont_Brouwer [in Continuity.kawai2018]
Bneigh_continuous_neigh_continuous [in Continuity.kawai2018]
brouwer_op_to_neighborhood [in Continuity.Partial.Neighborhood]
brouwer_op_to_strict_well_founded_neighborhood [in Continuity.Partial.Neighborhood]
Brouwer_operation_at_Type_spec [in Continuity.kawai2018]
Brouwer_operation_at'_spec1 [in Continuity.kawai2018]
Brouwer_operation_at_spec [in Continuity.kawai2018]
Bseq_cont_to_dialogue_cont_Brouwer [in Continuity.BI]
Btree_to_dialogueP [in Continuity.continuity_zoo_Prop]
Btree_to_dialogueP_aux [in Continuity.continuity_zoo_Prop]
Bvalid_every_list [in Continuity.Brouwer_ext]
Bvalid_plus [in Continuity.Brouwer_ext]

C

cantor [in Continuity.BredeHerbelin.cantor]
Cantor_Prop [in Continuity.BredeHerbelin.cantor]
case_to_false [in Continuity.BredeHerbelin.cantor]
choicefun_Downarbor_choicefun [in Continuity.BredeHerbelin.brede_herbelin]
choice_ABchoice_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
choice_TtoP_ABchoice [in Continuity.BredeHerbelin.brede_herbelin]
CI_imp_c_BI [in Continuity.BI]
CoCI_BI [in Continuity.BI]
coind_dial_cont_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
combine_app_same_length_r [in Continuity.Partial.DialogueTree]
comp_modulus_equiv [in Continuity.Partial.Modulus]
constructive_minimizer [in Continuity.Partial.DialogueTree]
cons_no_dup [in Continuity.Partial.DialogueTree]
continuous_mod_to_continuous_mod_weak [in Continuity.Partial.Modulus]
continuous_modulus_cont_to_have_modulus_fn [in Continuity.Partial.Modulus]
continuous_modulus_equiv [in Continuity.Partial.Modulus]
continuous_via_interrogations_iff [in Continuity.continuity_zoo_Prop]
cpo_cont_to_monotonic_modulus_cont_nat [in Continuity.Partial.Modulus]
cpo_cont_to_monotonic [in Continuity.Partial.Modulus]
c_BI_imp_CI [in Continuity.BI]

D

decidable_iff [in Continuity.Util]
DelayPartialImplem.bind_hasvalue [in Continuity.Partial.Delay]
DelayPartialImplem.Bind.bind_delay [in Continuity.Partial.Delay]
DelayPartialImplem.Bind.bind_now [in Continuity.Partial.Delay]
DelayPartialImplem.Bind.hasvalue_reciprocal [in Continuity.Partial.Delay]
DelayPartialImplem.Bind.hasvalue_direct [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_bisim [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_det [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect_delay [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect_now [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_correct [in Continuity.Partial.Delay]
DelayPartialImplem.mu_hasvalue [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_reciprocal [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_leq [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_some_false [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_some_true [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_hasvalue_direct [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_now_true [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_now_false [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_some_delay [in Continuity.Partial.Delay]
DelayPartialImplem.ret_hasvalue [in Continuity.Partial.Delay]
DelayPartialImplem.seval_hasvalue [in Continuity.Partial.Delay]
DelayPartialImplem.seval_mono [in Continuity.Partial.Delay]
DelayPartialImplem.Seval.delay_some [in Continuity.Partial.Delay]
DelayPartialImplem.Seval.hasvalue_reciprocal [in Continuity.Partial.Delay]
DelayPartialImplem.Seval.hasvalue_direct [in Continuity.Partial.Delay]
DelayPartialImplem.undef_hasvalue [in Continuity.Partial.Delay]
delay_eta [in Continuity.Partial.Delay]
Delta0_choice [in Continuity.continuity_zoo_Prop]
dialogue_tree_rect_ask [in Continuity.Partial.DialogueTree]
dialogue_tree_rect_output [in Continuity.Partial.DialogueTree]
dialogue_is_uniform [in Continuity.continuity_zoo_Prop]
dialogue_not_uniform [in Continuity.continuity_zoo_Prop]
dialogue_F [in Continuity.continuity_zoo_Prop]
dialogue_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_for [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree_wf [in Continuity.continuity_zoo_Prop]
dialogue_to_btree_cont [in Continuity.continuity_zoo_Prop]
dialogue_to_BtreeP [in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer_to_dialogue_cont [in Continuity.continuity_zoo_Prop]
dialogue_cont_to_is_dialogue [in Continuity.continuity_zoo_Prop]
dialogue_is_dialogue [in Continuity.continuity_zoo_Prop]
DNS [in Continuity.Classical]
double_modulus_at [in Continuity.Partial.Modulus]
DownABarbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]

E

embedP [in Continuity.Shared.embed_nat]
enumerable_to_strictify_neighborhood_cont [in Continuity.Partial.Neighborhood]
enumerable_list [in Continuity.Partial.Neighborhood]
enumerable_tuple [in Continuity.Partial.Neighborhood]
equiv_bind_hasvalue [in Continuity.Partial.Common]
equiv_ret_bind [in Continuity.Partial.Common]
equiv_bind_ret [in Continuity.Partial.Common]
equiv_bind_mult [in Continuity.Partial.Common]
equiv_hasvalue [in Continuity.Partial.Common]
equiv_bind' [in Continuity.Partial.Common]
equiv_bind [in Continuity.Partial.Common]
eq_catr [in Continuity.continuity_zoo_Prop]
eq_catl [in Continuity.continuity_zoo_Prop]
eq_cat [in Continuity.continuity_zoo_Prop]
eval_ext_tree_pref_monotone [in Continuity.Brouwer_ext]
eval_ext_tree_pref_monotone_aux [in Continuity.Brouwer_ext]
eval_ext_tree_trace_from_pref [in Continuity.Brouwer_ext]
eval_ext_tree_from_pref [in Continuity.Brouwer_ext]
eval_dialogue_tree_ask [in Continuity.Partial.DialogueTree]
eval_dialogue_tree_output [in Continuity.Partial.DialogueTree]
eval_ext_tree_aux_equiv_trace [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_prev_ask [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_ask_succ [in Continuity.Partial.TreeFunction]
eval_ext_tree_succ [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ_result [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_succ_ter [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux_det [in Continuity.Partial.TreeFunction]
eval_list_map_In [in Continuity.BI]
eval_list_incl_none [in Continuity.BI]
eval_list_monotone [in Continuity.BI]
eval_list_notin_cat [in Continuity.BI]
eval_list_none_fun [in Continuity.BI]
eval_list_notin [in Continuity.BI]
eval_list_In_is_fun [in Continuity.BI]
eval_list_In [in Continuity.BI]
eval_modulus_to_ext [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_continuous [in Continuity.continuity_zoo_Prop]
eval_ext_tree_continuous [in Continuity.continuity_zoo_Prop]
eval_ext_tree_valid_eqtau [in Continuity.continuity_zoo_Prop]
eval_ext_tree_to_interrogation [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval_trace [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_size_eval [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_monotone [in Continuity.continuity_zoo_Prop]
eval_ext_tree_monotone [in Continuity.continuity_zoo_Prop]
eval_ext_tree_map [in Continuity.continuity_zoo_Prop]
eval_ext_tree_map_aux [in Continuity.continuity_zoo_Prop]
eval_ext_tree_output_unique [in Continuity.continuity_zoo_Prop]
eval_ext_tree_constant [in Continuity.continuity_zoo_Prop]
eval_ext_tree_ext [in Continuity.continuity_zoo_Prop]
extend_app [in Continuity.Partial.Common]
extend_fold_part [in Continuity.Partial.Common]
extree_to_Bextree_noo_eq [in Continuity.Brouwer_ext]
extree_to_Bextree_spec [in Continuity.Brouwer_ext]
ext_but_not_mono [in Continuity.Partial.Modulus]
ext_tree_to_Bext_tree_valid [in Continuity.Brouwer_ext]
ext_tree_valid_eqtau_ask [in Continuity.continuity_zoo_Prop]
ext_tree_valid_valid [in Continuity.continuity_zoo_Prop]
ex_self_mod_to_cpo_cont [in Continuity.Partial.Modulus]
ex_monotonic_mod_to_monotonic [in Continuity.Partial.Modulus]
ex_monotonic_mod_to_ex_mod [in Continuity.Partial.Modulus]
ex_strong_mod_to_ex_monotonic_mod [in Continuity.Partial.Modulus]
ex_mod_to_ex_mod_weak [in Continuity.Partial.Modulus]
ex_modulus_modulus_fun [in Continuity.continuity_zoo_Prop]

F

firstn_app_l [in Continuity.Partial.Common]
fixed_magic_size [in Continuity.BredeHerbelin.brede_herbelin]
fixed_magic_incl [in Continuity.BredeHerbelin.brede_herbelin]
fold_part_list_general_hasvalue [in Continuity.Partial.DialogueTree]
fold_tab_nth_undef [in Continuity.Partial.Common]
fold_part_list_ret [in Continuity.Partial.Common]
fold_part_list_ter [in Continuity.Partial.Common]
fold_part_list_app [in Continuity.Partial.Common]
fold_part_list_tabulate_length [in Continuity.Partial.Common]
fold_part_list_tabulate_add_length [in Continuity.Partial.Common]
fold_part_list_length [in Continuity.Partial.Common]
fold_part_list_cons [in Continuity.Partial.Common]
fold_part_list_aux_app' [in Continuity.Partial.Common]
fold_part_list_aux_app [in Continuity.Partial.Common]
followP [in Continuity.continuity_zoo_Prop]
Forall_app_r [in Continuity.Partial.Common]
Forall_app_l [in Continuity.Partial.Common]
Forall_app [in Continuity.Partial.Common]
Forall2_rev [in Continuity.Partial.Common]
Forall2_imp [in Continuity.Partial.Common]
Forall2_app_r [in Continuity.Partial.Common]
Forall2_app_l [in Continuity.Partial.Common]
Forall2_app [in Continuity.Partial.Common]
from_pref_finite_equal [in Continuity.Brouwer_ext]
from_pref_map_iota [in Continuity.Brouwer_ext]

G

GBI_BI_alt [in Continuity.BredeHerbelin.brede_herbelin]
GBI_inconsistent [in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot_dec [in Continuity.BredeHerbelin.brede_herbelin]
GBI_BI_dec [in Continuity.BredeHerbelin.brede_herbelin]
GBI_monot [in Continuity.BredeHerbelin.brede_herbelin]
GBI_GCI [in Continuity.BI]
GBI_GCI_Fail [in Continuity.BI]
GDC_inconsistent [in Continuity.BredeHerbelin.brede_herbelin]
GDC_tree [in Continuity.BredeHerbelin.brede_herbelin]
generalize_pBIT_iff_pBIT [in Continuity.Partial.DialogueTree]
good_list_extend_after [in Continuity.Partial.DialogueTree]
good_list_extend_before [in Continuity.Partial.DialogueTree]
good_list_extract [in Continuity.Partial.DialogueTree]
G_zero [in Continuity.Shared.mu_nat]
G_sig [in Continuity.Shared.mu_nat]

H

hereditary [in Continuity.Partial.DialogueTree]
hereditary_closure_rect [in Continuity.extra_principles]
hereditary_closure_Acc [in Continuity.extra_principles]
hered_Upmon_hered_dec [in Continuity.BredeHerbelin.brede_herbelin]
hered_Upmon_hered [in Continuity.BredeHerbelin.brede_herbelin]

I

ieval_finapp_one_step_fuel [in Continuity.BI]
ieval_finapp_trace [in Continuity.BI]
ieval_finapp_monotone_ask_list_nomorefuel [in Continuity.BI]
ieval_finapp_monotone_ask_fuel [in Continuity.BI]
ieval_finapp_monotone_ask_list [in Continuity.BI]
ieval_finapp_monotone_output_fuel [in Continuity.BI]
ieval_finapp_monotone_output_list [in Continuity.BI]
ieval_output_unique [in Continuity.continuity_zoo_Prop]
implementation.bind_hasvalue_imp [in Continuity.Shared.partial]
implementation.hasvalue_det [in Continuity.Shared.partial]
implementation.list_max_lookup [in Continuity.Shared.partial]
implementation.lookup_seq [in Continuity.Shared.partial]
implementation.lt_list' [in Continuity.Shared.partial]
implementation.lt_list [in Continuity.Shared.partial]
implementation.mu_hasvalue_imp [in Continuity.Shared.partial]
implementation.mu_fun_spec [in Continuity.Shared.partial]
implementation.ret_hasvalue [in Continuity.Shared.partial]
implementation.seval_hasvalue_imp [in Continuity.Shared.partial]
implementation.seval_mono [in Continuity.Shared.partial]
implementation.undef_hasvalue [in Continuity.Shared.partial]
inclP [in Continuity.Util]
included_size [in Continuity.BredeHerbelin.brede_herbelin]
incl_iota_max [in Continuity.BredeHerbelin.brede_herbelin]
inconsistent [in Continuity.Classical]
indbarred_inductively_barred_dual [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred_Down_dual [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_inductively_barred [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_fun_list_itree_indbarredP [in Continuity.BI]
indbarred_fun_list_itree_indbarredP_aux [in Continuity.BI]
inductively_barred_indbarred_dual [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred_Down_dual [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred_indbarred [in Continuity.BredeHerbelin.brede_herbelin]
InP [in Continuity.Util]
interrogation_equiv_eval_ext_tree [in Continuity.continuity_zoo_Prop]
interrogation_app [in Continuity.continuity_zoo_Prop]
interrogation_ext [in Continuity.continuity_zoo_Prop]
interrogation_cons [in Continuity.continuity_zoo_Prop]
interrogation_plus [in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree_one_step [in Continuity.continuity_zoo_Prop]
int_dialogue_cont_to_dialogue_cont [in Continuity.continuity_zoo_Prop]
inversion_ask [in Continuity.continuity_zoo_Prop]
in_iota [in Continuity.BredeHerbelin.brede_herbelin]
in_map [in Continuity.BredeHerbelin.brede_herbelin]
In_eval_list [in Continuity.BI]
iota_rcons [in Continuity.Util]
is_fun_rcons_notin_dom [in Continuity.BI]
is_fun_cons_notin_dom [in Continuity.BI]
is_fun_cat_notin_dom [in Continuity.BI]
is_fun_list_incl [in Continuity.BI]
is_fun_map [in Continuity.BI]
is_dialogue_to_dialogue [in Continuity.continuity_zoo_Prop]
is_dialogue_to_dialogue_ext [in Continuity.continuity_zoo_Prop]
itree_to_Bitree_cont [in Continuity.Brouwer_ext]
itree_to_BitreeP [in Continuity.Brouwer_ext]
itree_to_Bitree_seq [in Continuity.Brouwer_ext]
itree_indbarredP_change_fuel [in Continuity.BI]
itree_indbarredP_monotone [in Continuity.BI]
itree_indbarred_spec [in Continuity.BI]
itree_indbarredP_ind [in Continuity.BI]
itree_indbarred_dialogue [in Continuity.BI]
itree_indbarred_dialogue_aux [in Continuity.BI]

K

K0K [in Continuity.kawai2018]
K0K_aux [in Continuity.kawai2018]

L

list_max_spec [in Continuity.Shared.partial]
list_to_dialogue_eq [in Continuity.continuity_zoo_Prop]
list_to_dialogue_deval_eq [in Continuity.continuity_zoo_Prop]
list_to_cantor_swap [in Continuity.continuity_zoo_Prop]
lots_of_separation [in Continuity.Partial.Modulus]
lpo_cpo_cont_is_monotonic_mod_cont_nat [in Continuity.Partial.Modulus]
lpo_cpo_cont_is_strong_mod_cont_nat [in Continuity.Partial.Modulus]
lpo_monotonic_mod_fn_is_strong_mod_fn [in Continuity.Partial.Modulus]
lpo_monotonic_mod_is_strong_mod [in Continuity.Partial.Modulus]

M

make_well_founded_is_well_founded [in Continuity.Partial.Neighborhood]
make_well_founded_is_monotonic [in Continuity.Partial.Neighborhood]
make_well_founded_preserves_neighborhood [in Continuity.Partial.Neighborhood]
map_incl [in Continuity.BredeHerbelin.brede_herbelin]
mem_fixed_magic [in Continuity.BredeHerbelin.brede_herbelin]
mem_fst_dec [in Continuity.Partial.DialogueTree]
mkpart_hasvalue [in Continuity.Shared.partial]
mkpart_hasvalue2 [in Continuity.Shared.partial]
mkpart_hasvalue1 [in Continuity.Shared.partial]
mkproof_ter [in Continuity.Shared.partial]
modulus_of_cpo_nat_is_modulus [in Continuity.Partial.Modulus]
modulus_cont_to_extensional [in Continuity.Partial.Modulus]
modulus_to_weak_modulus [in Continuity.Partial.Modulus]
modulus_fn_to_have_modulus [in Continuity.Partial.Modulus]
modulus_at_nat_to_modulus_at [in Continuity.continuity_zoo_Prop]
modulus_at_to_modulus_at_nat [in Continuity.continuity_zoo_Prop]
modulus_ex_modulus [in Continuity.continuity_zoo_Prop]
monotone_bar_extend_true [in Continuity.Partial.Neighborhood]
monotone_ABUp_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
monotonic_to_extensional [in Continuity.Partial.Modulus]
monotonic_modulus_to_modulus [in Continuity.Partial.Modulus]
monotonic_agnostic [in Continuity.Shared.partial]
monot_barred [in Continuity.BredeHerbelin.brede_herbelin]
MP [in Continuity.Classical]
mu_nat_dep_irrel [in Continuity.Shared.mu_nat]
mu_nat_dep_min [in Continuity.Shared.mu_nat]
mu_nat' [in Continuity.Shared.mu_nat]
mu_nat [in Continuity.Shared.mu_nat]
mu_tot_ter [in Continuity.Shared.partial]
mu_tot_hasvalue [in Continuity.Shared.partial]
mu_ter [in Continuity.Shared.partial]
mu_fold_spec [in Continuity.Partial.DialogueTree]
mu_opt_hasvalue [in Continuity.Partial.Common]
mu_opt_ter [in Continuity.Partial.Common]

N

neighborhood_to_brouwer_op_pbit [in Continuity.Partial.Neighborhood]
neighborhood_canonical_correct [in Continuity.Partial.Neighborhood]
neighborhood_for_squash [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_strict [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_hasvalue_none [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_hasvalue_some [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_ter [in Continuity.Partial.Neighborhood]
neighborhood_cont_is_well_founded_neighborhood_cont [in Continuity.Partial.Neighborhood]
neighborhood_cont_to_tree_fun_cont [in Continuity.Partial.TreeFunction]
neighborhood_fun_to_tree_fun_spec [in Continuity.Partial.TreeFunction]
neighborhood_to_tree_trace [in Continuity.Partial.TreeFunction]
neighborhood_wf_valid_Bext_tree [in Continuity.kawai2018]
neigh_cont_iff_Bcoind_dial_cont [in Continuity.kawai2018]
neigh_cont_to_Bcoind_dial_cont [in Continuity.kawai2018]
neigh_cont_Btree_fun_cont [in Continuity.kawai2018]
neigh_realises_Beval [in Continuity.kawai2018]
neigh_realises_Beval_aux [in Continuity.kawai2018]
NoDupP [in Continuity.Util]
normalized_good_list_nodup [in Continuity.Partial.DialogueTree]
normalize_is_normalized [in Continuity.Partial.DialogueTree]
Notallin [in Continuity.Util]
nth_error_split_lr [in Continuity.Partial.DialogueTree]
nth_undef_app_r [in Continuity.Partial.Common]
nth_error_app [in Continuity.Partial.Common]
nth_nth' [in Continuity.BI]
n_comp_n_plus [in Continuity.continuity_zoo_Prop]

O

ordP [in Continuity.BredeHerbelin.brede_herbelin]
ord_dec [in Continuity.BredeHerbelin.brede_herbelin]
ord_iota_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_map_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size [in Continuity.BredeHerbelin.brede_herbelin]
ord_inf_size_aux [in Continuity.BredeHerbelin.brede_herbelin]
ord_incl' [in Continuity.BredeHerbelin.brede_herbelin]
ord_NoDup [in Continuity.BredeHerbelin.brede_herbelin]
ord_in_2 [in Continuity.BredeHerbelin.brede_herbelin]
ord_sizeu_notin [in Continuity.BredeHerbelin.brede_herbelin]
ord_notin [in Continuity.BredeHerbelin.brede_herbelin]
ord_incl [in Continuity.BredeHerbelin.brede_herbelin]
ord_nth_in [in Continuity.BredeHerbelin.brede_herbelin]
ord_in [in Continuity.BredeHerbelin.brede_herbelin]
ord_nth [in Continuity.BredeHerbelin.brede_herbelin]
ord_rcons [in Continuity.BredeHerbelin.brede_herbelin]
ord_size [in Continuity.BredeHerbelin.brede_herbelin]
ord_drop [in Continuity.BredeHerbelin.brede_herbelin]
ord_take [in Continuity.BredeHerbelin.brede_herbelin]
ord_cat [in Continuity.BredeHerbelin.brede_herbelin]
ord_inj [in Continuity.BredeHerbelin.brede_herbelin]
ord_map_snd [in Continuity.BredeHerbelin.brede_herbelin]

P

part_fold_preserves [in Continuity.Partial.DialogueTree]
part_fold_ter [in Continuity.Partial.DialogueTree]
par_hasvalue3 [in Continuity.Shared.partial]
par_hasvalue2 [in Continuity.Shared.partial]
par_hasvalue1 [in Continuity.Shared.partial]
pbit_neighborhood_cont_to_brouwer_cont_nat [in Continuity.Partial.Neighborhood]
pbit_neighborhood_cont_to_brouwer_cont [in Continuity.Partial.Neighborhood]
pbit_neighborhood_to_brouwer_op [in Continuity.Partial.Neighborhood]
pBIT_ext_tree_to_dialogue_tree [in Continuity.Partial.DialogueTree]
permutes_quantifier_strict_well_founded_brouwer_operation [in Continuity.Partial.Neighborhood]
por_true [in Continuity.Partial.Modulus]
por_false [in Continuity.Partial.Modulus]
pref_a_Bieval [in Continuity.BI]
pref_a_beval [in Continuity.BI]
pref_a_alpha [in Continuity.BI]
pref_a_eq [in Continuity.BI]
pref_padded_prefix [in Continuity.continuity_zoo_Prop]
pref_le_eq [in Continuity.continuity_zoo_Prop]
pruning_pruning_Downarbor [in Continuity.BredeHerbelin.brede_herbelin]
pruning_ABapprox_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
pruning_TtoP_ABapprox [in Continuity.BredeHerbelin.brede_herbelin]
pruning_cat [in Continuity.BredeHerbelin.brede_herbelin]
pruning_arbor [in Continuity.BredeHerbelin.minimal_example]
PtoT_dec [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_ret [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_TtoP_inv [in Continuity.BredeHerbelin.brede_herbelin]
ptree_restrict [in Continuity.Partial.Neighborhood]
ptree_branch_extend [in Continuity.Partial.Neighborhood]
P_ABUp_PtoTB [in Continuity.BredeHerbelin.brede_herbelin]
P_ABDown_PtoT [in Continuity.BredeHerbelin.brede_herbelin]
P_Uparbor_PtoT [in Continuity.BredeHerbelin.brede_herbelin]

R

rebuild_first_values_app [in Continuity.Partial.DialogueTree]
reify [in Continuity.continuity_zoo_Prop]
reify2 [in Continuity.continuity_zoo_Prop]
retraction_Lawvere [in Continuity.BredeHerbelin.cantor]
ret_hasvalue_iff [in Continuity.Shared.partial]
ret_hasvalue' [in Continuity.Shared.partial]
ret_hasvalue_inv [in Continuity.Shared.partial]
rev_combine [in Continuity.Partial.DialogueTree]
rev_firstn_rev [in Continuity.Partial.Common]

S

self_mod_to_self_mod_weak [in Continuity.Partial.Modulus]
self_modulus_cont_to_continuous_modulus_cont [in Continuity.Partial.Modulus]
self_modulus_equiv [in Continuity.Partial.Modulus]
self_mod_cont_not_tree_fun_cont [in Continuity.Partial.TreeFunction]
self_modulus_tree_fun_cont [in Continuity.continuity_zoo_Prop]
sigma1pfn [in Continuity.Partial.Common]
size_ord [in Continuity.BredeHerbelin.brede_herbelin]
split_app [in Continuity.Partial.DialogueTree]
strictify_self_mod_weak [in Continuity.Partial.Modulus]
strictify_continuous_mod_weak [in Continuity.Partial.Modulus]
strictify_weak_modulus [in Continuity.Partial.Modulus]
strictify_modulus_at [in Continuity.Partial.Modulus]
strictify_modulus_ter' [in Continuity.Partial.Modulus]
strictify_modulus_hasvalue' [in Continuity.Partial.Modulus]
strictify_modulus_hasvalue [in Continuity.Partial.Modulus]
strictify_modulus_ter [in Continuity.Partial.Modulus]
strictify_preserves_neighborhood [in Continuity.Partial.Neighborhood]
strict_modulus [in Continuity.Partial.Modulus]
strict_well_founded_neighborhood_for_squash [in Continuity.Partial.Neighborhood]
strict_well_founded_tree_fun_for_squash [in Continuity.Partial.DialogueTree]
strong_modulus_to_monotonic_modulus [in Continuity.Partial.Modulus]

T

tabulate_equiv [in Continuity.Partial.Common]
tabulate_map [in Continuity.Partial.Common]
tabulate_length [in Continuity.Partial.Common]
tabulate_add [in Continuity.Partial.Common]
tabulate_succ' [in Continuity.Partial.Common]
tabulate_succ [in Continuity.Partial.Common]
tabulate_same [in Continuity.Partial.Common]
test [in Continuity.BredeHerbelin.minimal_example]
Theorem5 [in Continuity.BredeHerbelin.brede_herbelin]
Theorem5rev [in Continuity.BredeHerbelin.brede_herbelin]
top_cons [in Continuity.BredeHerbelin.brede_herbelin]
tree_fun_cont_to_Brouwer [in Continuity.Brouwer_ext]
tree_fun_cont_to_Brouwer_aux [in Continuity.Brouwer_ext]
tree_fun_for_squash [in Continuity.Partial.DialogueTree]
tree_fun_cont_to_strong_self_modulus_cont [in Continuity.Partial.TreeFunction]
tree_fun_for_good_def [in Continuity.Partial.TreeFunction]
tree_fun_cont_strong_self_modulus [in Continuity.Partial.TreeFunction]
tree_fun_cont_strong_modulus' [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_restrict [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_restrict' [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_equiv_trace [in Continuity.Partial.TreeFunction]
tree_fun_cont_not_neighborhood_cont [in Continuity.Partial.TreeFunction]
tree_fun_cont_to_self_modulus_cont [in Continuity.Partial.TreeFunction]
tree_fun_cont_self_modulus [in Continuity.Partial.TreeFunction]
tree_fun_cont_modulus [in Continuity.Partial.TreeFunction]
tree_fun_trace_ter_fold [in Continuity.Partial.TreeFunction]
tree_fun_trace_mod [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_mod [in Continuity.Partial.TreeFunction]
tree_fun_trace_succ [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_succ [in Continuity.Partial.TreeFunction]
tree_fun_trace_val [in Continuity.Partial.TreeFunction]
tree_fun_trace_ter [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux_det [in Continuity.Partial.TreeFunction]
tree_fun_cont_equiv_self_modulus_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_self_modulus_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_tree_fun_cont_valid [in Continuity.continuity_zoo_Prop]
tree_fun_cont_iff_coind_dial_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_to_coind_dial_cont [in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf_to_tree_fun_cont [in Continuity.continuity_zoo_Prop]
TtoP_PtoT_inv [in Continuity.BredeHerbelin.brede_herbelin]
T14 [in Continuity.continuity_zoo_Prop]
T41 [in Continuity.continuity_zoo_Prop]

U

undef'_hasvalue [in Continuity.Shared.partial]
unembedP [in Continuity.Shared.embed_nat]
uniform_is_dialogue [in Continuity.continuity_zoo_Prop]
unzip1_ord [in Continuity.BredeHerbelin.brede_herbelin]
unzip2_ord [in Continuity.BredeHerbelin.brede_herbelin]
UpABarbor_is_tree [in Continuity.BredeHerbelin.brede_herbelin]
Uparbor_PtoT_P [in Continuity.BredeHerbelin.brede_herbelin]
UpmonotonisationP [in Continuity.BredeHerbelin.brede_herbelin]
Upmonot_monotone [in Continuity.BredeHerbelin.brede_herbelin]
Upmono_dec [in Continuity.BredeHerbelin.brede_herbelin]
upP [in Continuity.BredeHerbelin.brede_herbelin]
useless_hypothesis [in Continuity.kawai2018]

V

valid_cat [in Continuity.continuity_zoo_Prop]
VectorEmbedding.vec_nat_inv [in Continuity.Shared.embed_nat]

W

well_founded_neighborhood_for_squash [in Continuity.Partial.Neighborhood]
well_founded_neighborhood_hasvalue [in Continuity.Partial.Neighborhood]
well_founded_tree_fun_for_squash [in Continuity.Partial.DialogueTree]
without_loss_of_generality_le_sym [in Continuity.Partial.DialogueTree]

Constructor Index

A

approx [in Continuity.BredeHerbelin.brede_herbelin]
Ask [in Continuity.Partial.DialogueTree]
Ask [in Continuity.continuity_zoo_Prop]
ask [in Continuity.continuity_zoo_Prop]

B

Bbeta_dep [in Continuity.continuity_zoo_Prop]
Bconst [in Continuity.kawai2018]
Bconst_at [in Continuity.kawai2018]
Beta [in Continuity.BredeHerbelin.brede_herbelin]
beta [in Continuity.continuity_zoo_Prop]
Beta_dep [in Continuity.continuity_zoo_Prop]
BisimDelayF [in Continuity.Partial.Delay]
BisimNowF [in Continuity.Partial.Delay]
bite [in Continuity.continuity_zoo_Prop]
BOp [in Continuity.Partial.Neighborhood]
Bret [in Continuity.Brouwer_ext]
Bsup [in Continuity.kawai2018]
Bsup_at_Type [in Continuity.kawai2018]
Bsup_at' [in Continuity.kawai2018]
Bsup_at [in Continuity.kawai2018]
Bvis [in Continuity.Brouwer_ext]

D

DelayF [in Continuity.Partial.Delay]
DelayPartialImplem.HasValueDelay [in Continuity.Partial.Delay]
DelayPartialImplem.HasValueNow [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.HasValueAux [in Continuity.Partial.Delay]

E

Eta [in Continuity.BredeHerbelin.brede_herbelin]
eta [in Continuity.continuity_zoo_Prop]

G

GI [in Continuity.Shared.mu_nat]
GoodList [in Continuity.Partial.DialogueTree]

H

hereditary_sons [in Continuity.extra_principles]
hereditary_self [in Continuity.extra_principles]
hereditary_sons [in Continuity.BredeHerbelin.minimal_example]
hereditary_self [in Continuity.BredeHerbelin.minimal_example]
Hpbar [in Continuity.Partial.Neighborhood]
Hpbar [in Continuity.Partial.DialogueTree]

I

ibeta [in Continuity.BredeHerbelin.brede_herbelin]
ieta [in Continuity.BredeHerbelin.brede_herbelin]
implementation.Allfalse [in Continuity.Shared.partial]
implementation.Diverged [in Continuity.Shared.partial]
implementation.Trueat [in Continuity.Shared.partial]
inverse [in Continuity.BredeHerbelin.cantor]
itree_in [in Continuity.BI]
itree_beta [in Continuity.BI]
itree_succ [in Continuity.BI]
itree_eta [in Continuity.BI]

M

mon [in Continuity.BredeHerbelin.brede_herbelin]
mon [in Continuity.BredeHerbelin.minimal_example]

N

NoQuestions [in Continuity.continuity_zoo_Prop]
normask [in Continuity.continuity_zoo_Prop]
normret [in Continuity.continuity_zoo_Prop]
normsucccons [in Continuity.continuity_zoo_Prop]
normsuccnil [in Continuity.continuity_zoo_Prop]
normzerocons [in Continuity.continuity_zoo_Prop]
normzeronil [in Continuity.continuity_zoo_Prop]
NowF [in Continuity.Partial.Delay]

O

Output [in Continuity.Partial.DialogueTree]
output [in Continuity.continuity_zoo_Prop]

P

prune [in Continuity.BredeHerbelin.brede_herbelin]
prune [in Continuity.BredeHerbelin.minimal_example]
ptot [in Continuity.BredeHerbelin.brede_herbelin]

R

ret [in Continuity.continuity_zoo_Prop]
Ret [in Continuity.continuity_zoo_Prop]

S

sefl_mon [in Continuity.BredeHerbelin.brede_herbelin]
sons_mon [in Continuity.BredeHerbelin.brede_herbelin]
spit [in Continuity.continuity_zoo_Prop]

T

Tarbor [in Continuity.BredeHerbelin.brede_herbelin]
Tau [in Continuity.continuity_zoo_Prop]
tbeta [in Continuity.continuity_zoo_Prop]
teta [in Continuity.continuity_zoo_Prop]
Tmon [in Continuity.BredeHerbelin.brede_herbelin]
Tmon_size [in Continuity.BredeHerbelin.brede_herbelin]

V

vis [in Continuity.continuity_zoo_Prop]
Vis [in Continuity.continuity_zoo_Prop]

Inductive Index

A

ABapprox [in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size [in Continuity.BredeHerbelin.brede_herbelin]

B

Bitree [in Continuity.Brouwer_ext]
brouwer_op [in Continuity.Partial.Neighborhood]
Brouwer_operation_at_Type [in Continuity.kawai2018]
Brouwer_operation_at' [in Continuity.kawai2018]
Brouwer_operation_at [in Continuity.kawai2018]
Brouwer_operation [in Continuity.kawai2018]
Btree [in Continuity.continuity_zoo_Prop]
Btree_dep [in Continuity.continuity_zoo_Prop]

D

delayF [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux [in Continuity.Partial.Delay]
delay_bisimF [in Continuity.Partial.Delay]
dialogue [in Continuity.continuity_zoo_Prop]
dialogue_tree [in Continuity.Partial.DialogueTree]

G

G [in Continuity.Shared.mu_nat]
good_list [in Continuity.Partial.DialogueTree]

H

hereditarily_pbarred [in Continuity.Partial.Neighborhood]
hereditarily_pbarred [in Continuity.Partial.DialogueTree]
hereditary_closure [in Continuity.extra_principles]
hereditary_closure [in Continuity.BredeHerbelin.minimal_example]
hered_mon [in Continuity.BredeHerbelin.brede_herbelin]

I

implementation.res [in Continuity.Shared.partial]
indbarred [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec [in Continuity.BredeHerbelin.brede_herbelin]
interrogation [in Continuity.continuity_zoo_Prop]
is_dialogue [in Continuity.continuity_zoo_Prop]
Itree [in Continuity.continuity_zoo_Prop]
itree [in Continuity.continuity_zoo_Prop]
itree_indbarredP [in Continuity.BI]
itree_indbarred [in Continuity.BI]

N

norm1 [in Continuity.continuity_zoo_Prop]
norm2 [in Continuity.continuity_zoo_Prop]

P

pruning [in Continuity.BredeHerbelin.brede_herbelin]
pruning [in Continuity.BredeHerbelin.minimal_example]
PtoT [in Continuity.BredeHerbelin.brede_herbelin]

R

result [in Continuity.continuity_zoo_Prop]
right_invertible [in Continuity.BredeHerbelin.cantor]

U

Upmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation [in Continuity.BredeHerbelin.minimal_example]

Projection Index

B

bind [in Continuity.Shared.partial]
bind_hasvalue [in Continuity.Shared.partial]

D

delay_bisim_go [in Continuity.Partial.Delay]
delay_go [in Continuity.Partial.Delay]

F

F [in Continuity.Partial.Neighborhood]
F [in Continuity.Partial.DialogueTree]

G

gamma [in Continuity.Partial.Neighborhood]

H

hasvalue [in Continuity.Shared.partial]
hasvalue_det [in Continuity.Shared.partial]
Hgamma [in Continuity.Partial.Neighborhood]
Hptree_path [in Continuity.Partial.Neighborhood]
Hptree_branch [in Continuity.Partial.Neighborhood]
Hptree_path [in Continuity.Partial.DialogueTree]
Hptree_branch [in Continuity.Partial.DialogueTree]
Htau [in Continuity.Partial.DialogueTree]

I

implementation.spec_fun [in Continuity.Shared.partial]
implementation.the_fun [in Continuity.Shared.partial]

M

mu [in Continuity.Shared.partial]
mu_hasvalue [in Continuity.Shared.partial]

P

part [in Continuity.Shared.partial]
ptree_path [in Continuity.Partial.Neighborhood]
ptree_branch [in Continuity.Partial.Neighborhood]
ptree_path [in Continuity.Partial.DialogueTree]
ptree_branch [in Continuity.Partial.DialogueTree]

R

ret [in Continuity.Shared.partial]
ret_hasvalue [in Continuity.Shared.partial]

S

seval [in Continuity.Shared.partial]
seval_hasvalue [in Continuity.Shared.partial]
seval_mono [in Continuity.Shared.partial]

T

tau [in Continuity.Partial.DialogueTree]
the_func_proof [in Continuity.Shared.partial]
the_rel [in Continuity.Shared.partial]

U

undef [in Continuity.Shared.partial]
undef_hasvalue [in Continuity.Shared.partial]

Section Index

A

Additional_Lemmas [in Continuity.BredeHerbelin.brede_herbelin]
assume_part [in Continuity.Shared.partial]

B

BarInduction [in Continuity.BI]
Bars [in Continuity.extra_principles]
BI_mon [in Continuity.BredeHerbelin.brede_herbelin]
Brouwer [in Continuity.continuity_zoo_Prop]
Brouwer_interaction_trees [in Continuity.Brouwer_ext]
Brouwer_ext_tree [in Continuity.Brouwer_ext]

C

Cantor [in Continuity.continuity_zoo_Prop]
Cantor.fix_types [in Continuity.continuity_zoo_Prop]
cBI_implies_CI_fail [in Continuity.BI]
continuity_principles [in Continuity.continuity_zoo_Prop]
ContinuousBarInduction [in Continuity.BI]
ContinuousInduction [in Continuity.BI]

D

DC_GDC_BI_GBI [in Continuity.BredeHerbelin.brede_herbelin]
Dialogue_not_uniform [in Continuity.continuity_zoo_Prop]

F

FinQuestion [in Continuity.continuity_zoo_Prop]

G

GBI_dec.Magic [in Continuity.BredeHerbelin.brede_herbelin]
GBI_dec [in Continuity.BredeHerbelin.brede_herbelin]
GDC_gen [in Continuity.BredeHerbelin.brede_herbelin]
GDC_GBI_Definition [in Continuity.BredeHerbelin.brede_herbelin]
GeneralisedBarInduction [in Continuity.BI]

I

Intensional_Dialogue [in Continuity.continuity_zoo_Prop]

K

Kawai [in Continuity.kawai2018]

M

MinEx [in Continuity.BredeHerbelin.minimal_example]
Modulus [in Continuity.continuity_zoo_Prop]

N

nat_queries [in Continuity.continuity_zoo_Prop]

O

Ord [in Continuity.BredeHerbelin.brede_herbelin]

P

PartialZoo [in Continuity.Partial.Modulus]
PartialZoo [in Continuity.Partial.Neighborhood]
PartialZoo [in Continuity.Partial.TreeFunction]
PartialZoo [in Continuity.Partial.Common]

S

sec [in Continuity.continuity_zoo_Prop]

T

Technical [in Continuity.BredeHerbelin.brede_herbelin]
TreeFunction [in Continuity.continuity_zoo_Prop]

W

WO [in Continuity.Shared.mu_nat]

Instance Index

D

DelayPartialImplem.delay_monad [in Continuity.Partial.Delay]

I

implementation.monotonic_functions [in Continuity.Shared.partial]

P

part_equiv_Equivalence [in Continuity.Partial.Delay]
part_equiv_Equivalence [in Continuity.Shared.partial]

Abbreviation Index

B

Brouwer [in Continuity.continuity_zoo_Prop]

D

dialogue [in Continuity.continuity_zoo_Prop]

I

itree [in Continuity.Brouwer_ext]
Itree [in Continuity.BI]

Q

Q [in Continuity.Brouwer_ext]
Q [in Continuity.Brouwer_ext]
Q [in Continuity.BI]
Q [in Continuity.BI]
Q [in Continuity.continuity_zoo_Prop]
Q [in Continuity.continuity_zoo_Prop]
Q [in Continuity.continuity_zoo_Prop]

R

R [in Continuity.BI]

Definition Index

A

ABbarred [in Continuity.BredeHerbelin.brede_herbelin]
ABchoicefun [in Continuity.BredeHerbelin.brede_herbelin]
ABDownarborification [in Continuity.BredeHerbelin.brede_herbelin]
ABDownmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]
ABis_tree [in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone [in Continuity.BredeHerbelin.brede_herbelin]
ABmonotone_size [in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUparborification_ind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_size_ind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_sind [in Continuity.BredeHerbelin.brede_herbelin]
ABUpmonotonisation_ind [in Continuity.BredeHerbelin.brede_herbelin]
agnostic [in Continuity.Shared.partial]
approx [in Continuity.Partial.Modulus]

B

barred [in Continuity.extra_principles]
bar_to_neighborhood_fun [in Continuity.Partial.Neighborhood]
Bbeta [in Continuity.continuity_zoo_Prop]
Bcoind_dial_cont [in Continuity.Brouwer_ext]
beval [in Continuity.continuity_zoo_Prop]
Beval_ext_tree_trace [in Continuity.Brouwer_ext]
Beval_ext_tree_trace_aux [in Continuity.Brouwer_ext]
Beval_ext_tree [in Continuity.Brouwer_ext]
Beval_ext_tree_aux [in Continuity.Brouwer_ext]
beval_list [in Continuity.BI]
beval_trace [in Continuity.BI]
Bext_tree [in Continuity.Brouwer_ext]
Bieval [in Continuity.Brouwer_ext]
Bieval_trace [in Continuity.kawai2018]
Bieval_trace [in Continuity.BI]
BIProp11Down [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Down_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up [in Continuity.BredeHerbelin.brede_herbelin]
BIProp11Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12 [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_sym [in Continuity.BredeHerbelin.brede_herbelin]
BIProp12_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13 [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Down_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13Up_rev [in Continuity.BredeHerbelin.brede_herbelin]
BIProp13_rev [in Continuity.BredeHerbelin.brede_herbelin]
Bitree_to_itree [in Continuity.Brouwer_ext]
Bitree_to_itree_aux [in Continuity.Brouwer_ext]
Bitree_to_option [in Continuity.Brouwer_ext]
BI_alt [in Continuity.BredeHerbelin.brede_herbelin]
BI_ind [in Continuity.extra_principles]
Bneigh_cont [in Continuity.kawai2018]
brouwer_operation_cont [in Continuity.Partial.Neighborhood]
brouwer_op_for [in Continuity.Partial.Neighborhood]
brouwer_op_ind' [in Continuity.Partial.Neighborhood]
brouwer_op_sind [in Continuity.Partial.Neighborhood]
brouwer_op_ind [in Continuity.Partial.Neighborhood]
Brouwer_operation_at_Type_sind [in Continuity.kawai2018]
Brouwer_operation_at_Type_rec [in Continuity.kawai2018]
Brouwer_operation_at_Type_ind [in Continuity.kawai2018]
Brouwer_operation_at_Type_rect [in Continuity.kawai2018]
Brouwer_operation_at'_sind [in Continuity.kawai2018]
Brouwer_operation_at'_rec [in Continuity.kawai2018]
Brouwer_operation_at'_ind [in Continuity.kawai2018]
Brouwer_operation_at'_rect [in Continuity.kawai2018]
Brouwer_operation_at_sind [in Continuity.kawai2018]
Brouwer_operation_at_ind [in Continuity.kawai2018]
Brouwer_operation_sind [in Continuity.kawai2018]
Brouwer_operation_ind [in Continuity.kawai2018]
Btree_fun_cont_valid [in Continuity.Brouwer_ext]
Btree_fun_cont [in Continuity.Brouwer_ext]
Btree_to_dialogue [in Continuity.continuity_zoo_Prop]
Btree_to_dialogue_aux [in Continuity.continuity_zoo_Prop]
Btree_dep_sind [in Continuity.continuity_zoo_Prop]
Btree_dep_rec [in Continuity.continuity_zoo_Prop]
Btree_dep_ind [in Continuity.continuity_zoo_Prop]
Btree_dep_rect [in Continuity.continuity_zoo_Prop]
Btree_sind [in Continuity.continuity_zoo_Prop]
Btree_rec [in Continuity.continuity_zoo_Prop]
Btree_ind [in Continuity.continuity_zoo_Prop]
Btree_rect [in Continuity.continuity_zoo_Prop]
Bvalid_ext_tree [in Continuity.Brouwer_ext]

C

choicefun [in Continuity.BredeHerbelin.brede_herbelin]
coind_dial_cont [in Continuity.continuity_zoo_Prop]
comp_modulus'_cont [in Continuity.Partial.Modulus]
comp_modulus_cont [in Continuity.Partial.Modulus]
comp_modulus_cont [in Continuity.continuity_zoo_Prop]
Cont [in Continuity.Classical]
continuous_mod_weak_continuous' [in Continuity.Partial.Modulus]
continuous_mod_weak_continuous [in Continuity.Partial.Modulus]
continuous_modulus'_cont [in Continuity.Partial.Modulus]
continuous_modulus_cont [in Continuity.Partial.Modulus]
continuous_modulus_cont_nat [in Continuity.continuity_zoo_Prop]
continuous_modulus_cont [in Continuity.continuity_zoo_Prop]
cpo_cont [in Continuity.Partial.Modulus]
c_BI [in Continuity.BI]
c_bar [in Continuity.BI]

D

DC [in Continuity.BredeHerbelin.brede_herbelin]
DCProp11 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp11_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_sym [in Continuity.BredeHerbelin.brede_herbelin]
DCProp12_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13 [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym_rev [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_sym [in Continuity.BredeHerbelin.brede_herbelin]
DCProp13_rev [in Continuity.BredeHerbelin.brede_herbelin]
Delay [in Continuity.Partial.Delay]
delayF_sind [in Continuity.Partial.Delay]
delayF_rec [in Continuity.Partial.Delay]
delayF_ind [in Continuity.Partial.Delay]
delayF_rect [in Continuity.Partial.Delay]
DelayPartialImplem.bind [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_rect [in Continuity.Partial.Delay]
DelayPartialImplem.hasvalue_ind [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_rect [in Continuity.Partial.Delay]
DelayPartialImplem.HasValue.aux_ind [in Continuity.Partial.Delay]
DelayPartialImplem.mu [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_spec_reciprocal [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_spec_direct [in Continuity.Partial.Delay]
DelayPartialImplem.Mu.aux_none [in Continuity.Partial.Delay]
DelayPartialImplem.ret [in Continuity.Partial.Delay]
DelayPartialImplem.seval [in Continuity.Partial.Delay]
DelayPartialImplem.undef [in Continuity.Partial.Delay]
delay_bisim_trans [in Continuity.Partial.Delay]
delay_bisim_sym [in Continuity.Partial.Delay]
delay_bisim_refl [in Continuity.Partial.Delay]
delay_bisimF_sind [in Continuity.Partial.Delay]
delay_bisimF_ind [in Continuity.Partial.Delay]
deval [in Continuity.continuity_zoo_Prop]
deval_list_to_dialogue_trace [in Continuity.continuity_zoo_Prop]
dialogue_tree_for_at [in Continuity.Partial.DialogueTree]
dialogue_tree_cont [in Continuity.Partial.DialogueTree]
dialogue_tree_for [in Continuity.Partial.DialogueTree]
dialogue_tree_ind [in Continuity.Partial.DialogueTree]
dialogue_tree_rect [in Continuity.Partial.DialogueTree]
dialogue_to_list [in Continuity.continuity_zoo_Prop]
dialogue_to_ext_tree [in Continuity.continuity_zoo_Prop]
dialogue_to_Btree [in Continuity.continuity_zoo_Prop]
dialogue_to_Brouwer [in Continuity.continuity_zoo_Prop]
dialogue_cont_Brouwer [in Continuity.continuity_zoo_Prop]
dialogue_cont [in Continuity.continuity_zoo_Prop]
dialogue_sind [in Continuity.continuity_zoo_Prop]
dialogue_rec [in Continuity.continuity_zoo_Prop]
dialogue_ind [in Continuity.continuity_zoo_Prop]
dialogue_rect [in Continuity.continuity_zoo_Prop]
DNE [in Continuity.Classical]
Downarborification [in Continuity.BredeHerbelin.brede_herbelin]
Downarborification [in Continuity.BredeHerbelin.minimal_example]
Downmonotonisation [in Continuity.BredeHerbelin.brede_herbelin]

E

embed [in Continuity.Shared.embed_nat]
enumerable [in Continuity.Partial.Neighborhood]
enumerate_tuple [in Continuity.Partial.Neighborhood]
equiv [in Continuity.Shared.partial]
eval [in Continuity.Shared.partial]
eval_hasvalue [in Continuity.Shared.partial]
eval_dialogue_tree [in Continuity.Partial.DialogueTree]
eval_ext_tree [in Continuity.Partial.TreeFunction]
eval_ext_tree_aux [in Continuity.Partial.TreeFunction]
eval_list [in Continuity.BI]
eval_ext_tree_trace [in Continuity.continuity_zoo_Prop]
eval_ext_tree_trace_aux [in Continuity.continuity_zoo_Prop]
eval_ext_tree [in Continuity.continuity_zoo_Prop]
eval_ext_tree_aux [in Continuity.continuity_zoo_Prop]
eval' [in Continuity.Shared.partial]
extend [in Continuity.Partial.Common]
extensional [in Continuity.Partial.Modulus]
extree_to_Bextree_noo [in Continuity.Brouwer_ext]
extree_to_Bextree [in Continuity.Brouwer_ext]
extree_to_extree [in Continuity.Brouwer_ext]
ext_tree [in Continuity.Partial.TreeFunction]
ext_tree_valid [in Continuity.continuity_zoo_Prop]
ext_tree_valid_aux [in Continuity.continuity_zoo_Prop]
ext_tree_to_int_tree [in Continuity.continuity_zoo_Prop]
ext_tree_for [in Continuity.continuity_zoo_Prop]
ext_tree [in Continuity.continuity_zoo_Prop]
ex_monotonic_modulus [in Continuity.Partial.Modulus]
ex_strong_modulus [in Continuity.Partial.Modulus]
ex_mod_continuous_weak [in Continuity.Partial.Modulus]
ex_modulus_cont [in Continuity.Partial.Modulus]
ex_modulus_cont_nat [in Continuity.continuity_zoo_Prop]
ex_modulus_cont [in Continuity.continuity_zoo_Prop]

F

F [in Continuity.continuity_zoo_Prop]
fixed_magic [in Continuity.BredeHerbelin.brede_herbelin]
fold_part_list_general [in Continuity.Partial.DialogueTree]
fold_part_list [in Continuity.Partial.Common]
fold_part_list_aux [in Continuity.Partial.Common]
follow [in Continuity.continuity_zoo_Prop]
from_pref [in Continuity.continuity_zoo_Prop]
functional [in Continuity.Shared.partial]

G

GBI [in Continuity.BredeHerbelin.brede_herbelin]
GDC [in Continuity.BredeHerbelin.brede_herbelin]
good_list_ind [in Continuity.Partial.DialogueTree]
G_sind [in Continuity.Shared.mu_nat]
G_rec [in Continuity.Shared.mu_nat]
G_ind [in Continuity.Shared.mu_nat]
G_rect [in Continuity.Shared.mu_nat]

H

hereditarily_pbarred_ind' [in Continuity.Partial.Neighborhood]
hereditarily_pbarred_sind [in Continuity.Partial.Neighborhood]
hereditarily_pbarred_ind [in Continuity.Partial.Neighborhood]
hereditarily_pbarred_rect [in Continuity.Partial.DialogueTree]
hereditarily_pbarred_ind [in Continuity.Partial.DialogueTree]
hereditary_closure_sind [in Continuity.extra_principles]
hereditary_closure_ind [in Continuity.extra_principles]
hereditary_closure_sind [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rec [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_ind [in Continuity.BredeHerbelin.minimal_example]
hereditary_closure_rect [in Continuity.BredeHerbelin.minimal_example]
hered_mon_sind [in Continuity.BredeHerbelin.brede_herbelin]
hered_mon_ind [in Continuity.BredeHerbelin.brede_herbelin]

I

ieval [in Continuity.continuity_zoo_Prop]
ieval_trace [in Continuity.BI]
ieval_finapp [in Continuity.BI]
implementation.bind [in Continuity.Shared.partial]
implementation.equiv [in Continuity.Shared.partial]
implementation.hasvalue [in Continuity.Shared.partial]
implementation.mu [in Continuity.Shared.partial]
implementation.mu_fun [in Continuity.Shared.partial]
implementation.res_sind [in Continuity.Shared.partial]
implementation.res_rec [in Continuity.Shared.partial]
implementation.res_ind [in Continuity.Shared.partial]
implementation.res_rect [in Continuity.Shared.partial]
implementation.ret [in Continuity.Shared.partial]
implementation.seval [in Continuity.Shared.partial]
implementation.ter [in Continuity.Shared.partial]
implementation.undef [in Continuity.Shared.partial]
indbarred_spec_sind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_spec_ind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_sind [in Continuity.BredeHerbelin.brede_herbelin]
indbarred_ind [in Continuity.BredeHerbelin.brede_herbelin]
inductively_barred [in Continuity.extra_principles]
interrogation_sind [in Continuity.continuity_zoo_Prop]
interrogation_ind [in Continuity.continuity_zoo_Prop]
int_tree_to_ext_tree [in Continuity.continuity_zoo_Prop]
int_dialogue_cont [in Continuity.continuity_zoo_Prop]
is_tree [in Continuity.BredeHerbelin.brede_herbelin]
is_fun_list [in Continuity.BI]
is_dialogue_sind [in Continuity.continuity_zoo_Prop]
is_dialogue_rec [in Continuity.continuity_zoo_Prop]
is_dialogue_ind [in Continuity.continuity_zoo_Prop]
is_dialogue_rect [in Continuity.continuity_zoo_Prop]
itree_to_Bitree [in Continuity.Brouwer_ext]
itree_indbarredP_rect [in Continuity.BI]
itree_indbarred_sind [in Continuity.BI]
itree_indbarred_rec [in Continuity.BI]
itree_indbarred_ind [in Continuity.BI]
itree_indbarred_rect [in Continuity.BI]

L

least [in Continuity.Shared.mu_nat]
list_to_dialogue [in Continuity.continuity_zoo_Prop]
list_to_cantor [in Continuity.continuity_zoo_Prop]
lpo [in Continuity.Partial.Modulus]

M

make_well_founded [in Continuity.Partial.Neighborhood]
mem_snd_in [in Continuity.Partial.DialogueTree]
mkpart [in Continuity.Shared.partial]
modulus [in Continuity.Partial.Modulus]
modulus [in Continuity.continuity_zoo_Prop]
modulus_of_cpo_nat [in Continuity.Partial.Modulus]
modulus_at [in Continuity.Partial.Modulus]
modulus_to_ext_tree [in Continuity.continuity_zoo_Prop]
modulus_nat [in Continuity.continuity_zoo_Prop]
modulus_at_nat [in Continuity.continuity_zoo_Prop]
modulus_at [in Continuity.continuity_zoo_Prop]
modulus' [in Continuity.Partial.Modulus]
monotone [in Continuity.BredeHerbelin.brede_herbelin]
monotonic [in Continuity.Partial.Modulus]
monotonic [in Continuity.Shared.partial]
monotonic_seq [in Continuity.Partial.Modulus]
monotonic_self_modulus_cont [in Continuity.Partial.Modulus]
monotonic_cont_modulus_cont [in Continuity.Partial.Modulus]
monotonic_modulus_cont [in Continuity.Partial.Modulus]
monotonic_modulus [in Continuity.Partial.Modulus]
mu_nat_dep_least [in Continuity.Shared.mu_nat]
mu_nat_dep [in Continuity.Shared.mu_nat]
mu_tot [in Continuity.Shared.partial]
mu_fold [in Continuity.Partial.DialogueTree]
mu_opt [in Continuity.Partial.Common]

N

neighborhoodfunction [in Continuity.kawai2018]
neighborhood_canonical [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify_wf [in Continuity.Partial.Neighborhood]
neighborhood_fun_strictify [in Continuity.Partial.Neighborhood]
neighborhood_cont [in Continuity.Partial.Neighborhood]
neighborhood_for [in Continuity.Partial.Neighborhood]
neighborhood_fun [in Continuity.Partial.Neighborhood]
neighborhood_fun_to_tree_fun [in Continuity.Partial.TreeFunction]
neigh_to_Bitree [in Continuity.kawai2018]
neigh_cont [in Continuity.kawai2018]
neigh_realises [in Continuity.kawai2018]
normalized_strict_well_founded_tree_fun_cont [in Continuity.Partial.DialogueTree]
normalized_strict_well_founded_tree_fun_for [in Continuity.Partial.DialogueTree]
normalized_ext_tree [in Continuity.Partial.DialogueTree]
normalize_ext_tree [in Continuity.Partial.DialogueTree]
norm1_sind [in Continuity.continuity_zoo_Prop]
norm1_rec [in Continuity.continuity_zoo_Prop]
norm1_ind [in Continuity.continuity_zoo_Prop]
norm1_rect [in Continuity.continuity_zoo_Prop]
norm2_sind [in Continuity.continuity_zoo_Prop]
norm2_rec [in Continuity.continuity_zoo_Prop]
norm2_ind [in Continuity.continuity_zoo_Prop]
norm2_rect [in Continuity.continuity_zoo_Prop]
Now [in Continuity.Partial.Delay]
nth_undef [in Continuity.Partial.Common]
nth' [in Continuity.BI]
n_comp [in Continuity.continuity_zoo_Prop]

O

omega_cpo [in Continuity.Partial.Modulus]
ord [in Continuity.BredeHerbelin.brede_herbelin]
ord_aux [in Continuity.BredeHerbelin.brede_herbelin]

P

padded_prefix [in Continuity.continuity_zoo_Prop]
padded_seq [in Continuity.continuity_zoo_Prop]
par [in Continuity.Shared.partial]
part_fold [in Continuity.Partial.DialogueTree]
pbarred [in Continuity.Partial.Neighborhood]
pbarred [in Continuity.Partial.DialogueTree]
pBIT [in Continuity.Partial.Neighborhood]
pBIT [in Continuity.Partial.DialogueTree]
pcomputes [in Continuity.Shared.partial]
por [in Continuity.Partial.Modulus]
pred_to_fun [in Continuity.BI]
pred_to_Bitree_aux [in Continuity.BI]
pref [in Continuity.continuity_zoo_Prop]
prefix [in Continuity.extra_principles]
pref_a [in Continuity.BI]
proof_ter_spec [in Continuity.Partial.Common]
proof_ter [in Continuity.Partial.Common]
PtoT_dual [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_sind [in Continuity.BredeHerbelin.brede_herbelin]
PtoT_ind [in Continuity.BredeHerbelin.brede_herbelin]

R

rebuild_first_values [in Continuity.Partial.DialogueTree]
reflectspfn [in Continuity.Partial.Common]
reflect1 [in Continuity.continuity_zoo_Prop]
reflect2 [in Continuity.continuity_zoo_Prop]
result_sind [in Continuity.continuity_zoo_Prop]
result_rec [in Continuity.continuity_zoo_Prop]
result_ind [in Continuity.continuity_zoo_Prop]
result_rect [in Continuity.continuity_zoo_Prop]
retract_of [in Continuity.Classical]
right_invertible_sind [in Continuity.BredeHerbelin.cantor]
right_invertible_ind [in Continuity.BredeHerbelin.cantor]

S

self_mod_weak_continuous' [in Continuity.Partial.Modulus]
self_mod_weak_continuous [in Continuity.Partial.Modulus]
self_modulus'_cont [in Continuity.Partial.Modulus]
self_modulus_cont [in Continuity.Partial.Modulus]
self_modulus_cont [in Continuity.continuity_zoo_Prop]
sigma1 [in Continuity.Partial.Common]
strictify_modulus [in Continuity.Partial.Modulus]
strict_well_founded_neighborhood_cont [in Continuity.Partial.Neighborhood]
strict_well_founded_neighborhood_for [in Continuity.Partial.Neighborhood]
strict_neighborhood [in Continuity.Partial.Neighborhood]
strict_well_founded_tree_fun_cont [in Continuity.Partial.TreeFunction]
strict_well_founded_tree_fun_for [in Continuity.Partial.TreeFunction]
strict_ext_tree [in Continuity.Partial.TreeFunction]
strong_self_modulus_cont [in Continuity.Partial.Modulus]
strong_cont_modulus_cont [in Continuity.Partial.Modulus]
strong_modulus_cont [in Continuity.Partial.Modulus]
strong_modulus [in Continuity.Partial.Modulus]
sup [in Continuity.Partial.Modulus]

T

tabulate [in Continuity.Partial.Common]
tabulate_aux [in Continuity.Partial.Common]
ter [in Continuity.Shared.partial]
termination_tree [in Continuity.Partial.Neighborhood]
termination_tree [in Continuity.Partial.DialogueTree]
top [in Continuity.BredeHerbelin.brede_herbelin]
total [in Continuity.Shared.partial]
tree_fun_cont_strong_modulus_fn' [in Continuity.Partial.TreeFunction]
tree_fun_cont_mod_fn [in Continuity.Partial.TreeFunction]
tree_fun_trace [in Continuity.Partial.TreeFunction]
tree_fun_trace_aux [in Continuity.Partial.TreeFunction]
tree_fun_cont [in Continuity.Partial.TreeFunction]
tree_fun_for [in Continuity.Partial.TreeFunction]
tree_fun_cont_valid [in Continuity.continuity_zoo_Prop]
tree_fun_cont_wf [in Continuity.continuity_zoo_Prop]
tree_fun_cont_via_interrogations [in Continuity.continuity_zoo_Prop]
tree_fun_cont [in Continuity.continuity_zoo_Prop]
TtoP [in Continuity.BredeHerbelin.brede_herbelin]
TtoP_PtoT_ret [in Continuity.BredeHerbelin.brede_herbelin]
tuple [in Continuity.Partial.Neighborhood]
tuple_to_list [in Continuity.Partial.Neighborhood]

U

undef' [in Continuity.Shared.partial]
unembed [in Continuity.Shared.embed_nat]
uni_cont [in Continuity.continuity_zoo_Prop]
Unnamed_thm [in Continuity.Partial.Modulus]
Upmonotonisation_sind [in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_ind [in Continuity.BredeHerbelin.brede_herbelin]
Upmonotonisation_sind [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rec [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_ind [in Continuity.BredeHerbelin.minimal_example]
Upmonotonisation_rect [in Continuity.BredeHerbelin.minimal_example]

V

valid_ext_tree [in Continuity.continuity_zoo_Prop]
VectorEmbedding.nat_to_vec [in Continuity.Shared.embed_nat]
VectorEmbedding.vec_to_nat [in Continuity.Shared.embed_nat]

W

weak_modulus' [in Continuity.Partial.Modulus]
weak_modulus [in Continuity.Partial.Modulus]
well_founded_neighborhood_cont [in Continuity.Partial.Neighborhood]
well_founded_neighborhood_for [in Continuity.Partial.Neighborhood]
well_founded_neighborhood [in Continuity.Partial.Neighborhood]
well_founded_tree_fun_cont [in Continuity.Partial.TreeFunction]
well_founded_tree_fun_for [in Continuity.Partial.TreeFunction]
well_founded_ext_tree [in Continuity.Partial.TreeFunction]
wf_Bext_tree [in Continuity.Brouwer_ext]
wf_ext_tree [in Continuity.continuity_zoo_Prop]

Record Index

D

delay [in Continuity.Partial.Delay]
delay_bisim [in Continuity.Partial.Delay]

F

FunRel [in Continuity.Shared.partial]

I

implementation.part [in Continuity.Shared.partial]

P

partiality [in Continuity.Shared.partial]

S

sigma1_tree [in Continuity.Partial.Neighborhood]
sigma1_tree [in Continuity.Partial.DialogueTree]

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1260 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(31 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(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

_

other

(19 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(523 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(72 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(43 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(34 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(36 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(400 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7 entries)