| 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 | (529 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 | (47 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 | (1 entry) |
| 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 | (15 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 | (131 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 | (45 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 | (37 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 | (24 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 | (140 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 | (6 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 | (1 entry) |
| 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 | (52 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 | (30 entries) |
Global Index
A
acc [projection, in coqrel.KLR]all_monotonic_params [instance, in coqrel.Relators]
all_monotonic [instance, in coqrel.Relators]
andb_leb [instance, in coqrel.BoolRel]
and_monotonic [instance, in coqrel.Relators]
apply_candidate_subrel [instance, in coqrel.Monotonicity]
apply_candidate [instance, in coqrel.Monotonicity]
app_rel [instance, in coqrel.Relators]
arrow_pointwise_rel_compose [instance, in coqrel.Relators]
arrow_pointwise_refl [lemma, in coqrel.Relators]
arrow_pointwise_relim [lemma, in coqrel.Relators]
arrow_pointwise_rintro [lemma, in coqrel.Relators]
arrow_pointwise_subrel_params [instance, in coqrel.Relators]
arrow_pointwise_subrel [instance, in coqrel.Relators]
arrow_pointwise_rel [definition, in coqrel.Relators]
arrow_relim [lemma, in coqrel.RelDefinitions]
arrow_rintro [lemma, in coqrel.RelDefinitions]
arrow_subrel_params [instance, in coqrel.RelDefinitions]
arrow_subrel [instance, in coqrel.RelDefinitions]
arrow_rel [definition, in coqrel.RelDefinitions]
arrow_rdecompose [instance, in coqrel.RelClasses]
arrow_rcompose [instance, in coqrel.RelClasses]
ARROW_REL_COMPOSE [section, in coqrel.RelClasses]
arrow_corefl [instance, in coqrel.RelClasses]
arrow_refl [instance, in coqrel.RelClasses]
ARROW_MOD [section, in coqrel.KLR]
arrow_pointwise_klr [definition, in coqrel.KLR]
arrow_klr [definition, in coqrel.KLR]
as_is_candidate [instance, in coqrel.Monotonicity]
B
BoolRel [library]C
CandidateProperty [record, in coqrel.Monotonicity]CandidateProperty [inductive, in coqrel.Monotonicity]
candidate_related [projection, in coqrel.Monotonicity]
candidate_related [constructor, in coqrel.Monotonicity]
CommonPrefix [record, in coqrel.Monotonicity]
cons_rel [instance, in coqrel.Relators]
cons_rel_def [constructor, in coqrel.Relators]
convertible [projection, in coqrel.RelDefinitions]
Convertible [record, in coqrel.RelDefinitions]
convertible [constructor, in coqrel.RelDefinitions]
Convertible [inductive, in coqrel.RelDefinitions]
Coreflexive [record, in coqrel.RelClasses]
Coreflexive [inductive, in coqrel.RelClasses]
coreflexivity [projection, in coqrel.RelClasses]
coreflexivity [constructor, in coqrel.RelClasses]
curry [definition, in coqrel.RelOperators]
D
delay [definition, in coqrel.Delay]Delay [module, in coqrel.Delay]
Delay [library]
Delay.delayed_goal [definition, in coqrel.Delay]
Delay.open_conjunction_proj [projection, in coqrel.Delay]
Delay.open_conjunction [record, in coqrel.Delay]
Delay.unpack [definition, in coqrel.Delay]
direct_rexists [lemma, in coqrel.RelDefinitions]
E
eapply [projection, in coqrel.Delay]EApply [record, in coqrel.Delay]
eapply [constructor, in coqrel.Delay]
EApply [inductive, in coqrel.Delay]
Empty_set_rel [inductive, in coqrel.Relators]
eqrel [definition, in coqrel.RelOperators]
eqrel_subrel [instance, in coqrel.RelOperators]
eqrel_equivalence [instance, in coqrel.RelOperators]
eq_subrel [instance, in coqrel.RelDefinitions]
eq_corefl [instance, in coqrel.RelClasses]
eq_candidate [instance, in coqrel.Monotonicity]
ex_monotonic_params [instance, in coqrel.Relators]
ex_monotonic [instance, in coqrel.Relators]
F
false_leb [lemma, in coqrel.BoolRel]flip_rexists [lemma, in coqrel.RelDefinitions]
flip_rdestruct [lemma, in coqrel.RelDefinitions]
flip_relim [lemma, in coqrel.RelDefinitions]
flip_rintro [lemma, in coqrel.RelDefinitions]
flip_subrel_params [instance, in coqrel.RelDefinitions]
flip_subrel [instance, in coqrel.RelDefinitions]
flip_context_candidate [lemma, in coqrel.Monotonicity]
fold_impl_rstep [lemma, in coqrel.Relators]
fold_left_rel [instance, in coqrel.Relators]
fold_right_rel [instance, in coqrel.Relators]
forallp_relim [lemma, in coqrel.Relators]
forallp_rintro [lemma, in coqrel.Relators]
forallp_rel [definition, in coqrel.Relators]
forall_pointwise_relim [lemma, in coqrel.Relators]
forall_pointwise_rintro [lemma, in coqrel.Relators]
forall_pointwise_rel [definition, in coqrel.Relators]
forall_relation_relim [lemma, in coqrel.MorphismsInterop]
forall_relation_rintro [lemma, in coqrel.MorphismsInterop]
forall_relation_params [instance, in coqrel.MorphismsInterop]
forall_relation_subrel [instance, in coqrel.MorphismsInterop]
forall_relim [lemma, in coqrel.RelDefinitions]
forall_rintro [lemma, in coqrel.RelDefinitions]
forall_rel [definition, in coqrel.RelDefinitions]
fst_rel [instance, in coqrel.Relators]
f_equal_relim [lemma, in coqrel.Monotonicity]
I
implb_leb [instance, in coqrel.BoolRel]impl_transport [lemma, in coqrel.Transport]
inl_rel [instance, in coqrel.Relators]
inl_rel_def [constructor, in coqrel.Relators]
inr_rel [instance, in coqrel.Relators]
inr_rel_def [constructor, in coqrel.Relators]
K
k [definition, in coqrel.KLR]klr [definition, in coqrel.KLR]
KLR [library]
klr_pullw_relim [lemma, in coqrel.KLR]
klr_pullw_rintro [lemma, in coqrel.KLR]
klr_pullw_subrel_params [instance, in coqrel.KLR]
klr_pullw_subrel [instance, in coqrel.KLR]
klr_pullw [definition, in coqrel.KLR]
klr_diamat [definition, in coqrel.KLR]
klr_boxto [definition, in coqrel.KLR]
klr_diam_subrel_params [instance, in coqrel.KLR]
klr_box_subrel_params [instance, in coqrel.KLR]
klr_diam_relim [lemma, in coqrel.KLR]
klr_diam_rintro [lemma, in coqrel.KLR]
klr_diam_subrel [instance, in coqrel.KLR]
klr_diam [definition, in coqrel.KLR]
klr_box_relim [lemma, in coqrel.KLR]
klr_box_rintro [lemma, in coqrel.KLR]
klr_box_subrel [instance, in coqrel.KLR]
klr_box [definition, in coqrel.KLR]
klr_curry [definition, in coqrel.KLR]
klr_inter [definition, in coqrel.KLR]
klr_union [definition, in coqrel.KLR]
klr_inr [constructor, in coqrel.KLR]
klr_inl [constructor, in coqrel.KLR]
klr_sum [inductive, in coqrel.KLR]
KripkeFrame [record, in coqrel.KLR]
k_rel_params [instance, in coqrel.KLR]
k_relim [lemma, in coqrel.KLR]
k_rintro [lemma, in coqrel.KLR]
k_rel [instance, in coqrel.KLR]
k1 [definition, in coqrel.KLR]
k1_rel_params [instance, in coqrel.KLR]
k1_relim [lemma, in coqrel.KLR]
k1_rintro [lemma, in coqrel.KLR]
k1_rel [instance, in coqrel.KLR]
k2 [definition, in coqrel.KLR]
k2_rel_params [instance, in coqrel.KLR]
k2_unfold [instance, in coqrel.KLR]
k2_relim [lemma, in coqrel.KLR]
k2_rintro [lemma, in coqrel.KLR]
k2_rel [instance, in coqrel.KLR]
L
leb_transport_eq_true [instance, in coqrel.BoolRel]leb_rdestruct [lemma, in coqrel.BoolRel]
leb_preo [instance, in coqrel.BoolRel]
left_le [constructor, in coqrel.BoolRel]
left_rel [instance, in coqrel.BoolRel]
left_rel_def [constructor, in coqrel.BoolRel]
length_rel [instance, in coqrel.Relators]
LIFT [section, in coqrel.KLR]
list_rel_trans [lemma, in coqrel.Relators]
list_rel_sym [lemma, in coqrel.Relators]
list_rel_corefl [lemma, in coqrel.Relators]
list_rel_refl [lemma, in coqrel.Relators]
list_subrel_params [instance, in coqrel.Relators]
list_subrel [instance, in coqrel.Relators]
list_rel [inductive, in coqrel.Relators]
list_klr [definition, in coqrel.KLR]
LogicalRelations [library]
LogicalRelationsTests [library]
lsat [definition, in coqrel.RelOperators]
lsat_subrel_params [instance, in coqrel.RelOperators]
lsat_subrel [instance, in coqrel.RelOperators]
M
map_rel [instance, in coqrel.Relators]MODALITIES [section, in coqrel.KLR]
Monotonic [abbreviation, in coqrel.RelDefinitions]
monotonicity [projection, in coqrel.Monotonicity]
Monotonicity [record, in coqrel.Monotonicity]
monotonicity [constructor, in coqrel.Monotonicity]
Monotonicity [inductive, in coqrel.Monotonicity]
Monotonicity [library]
monotonicity_rstep [instance, in coqrel.Monotonicity]
MorphismsInterop [library]
morphisms_proper_related [instance, in coqrel.MorphismsInterop]
N
negb_leb [instance, in coqrel.BoolRel]nil_rel [instance, in coqrel.Relators]
nil_rel_def [constructor, in coqrel.Relators]
nondelayed [projection, in coqrel.Delay]
NonDelayed [record, in coqrel.Delay]
nondelayed [constructor, in coqrel.Delay]
NonDelayed [inductive, in coqrel.Delay]
None_rel [instance, in coqrel.Relators]
None_rel_def [constructor, in coqrel.Relators]
None_ge [lemma, in coqrel.OptionRel]
None_ge_def [constructor, in coqrel.OptionRel]
None_le [lemma, in coqrel.OptionRel]
None_le_def [constructor, in coqrel.OptionRel]
NotEvar [record, in coqrel.RelDefinitions]
O
once [projection, in coqrel.RelDefinitions]Once [record, in coqrel.RelDefinitions]
once [constructor, in coqrel.RelDefinitions]
Once [inductive, in coqrel.RelDefinitions]
OptionRel [library]
option_rel_some_inv [lemma, in coqrel.Relators]
option_map_rel [instance, in coqrel.Relators]
option_rel_refl [lemma, in coqrel.Relators]
option_subrel_params [instance, in coqrel.Relators]
option_subrel [instance, in coqrel.Relators]
option_rel [inductive, in coqrel.Relators]
option_ge_transport_eq_none [instance, in coqrel.OptionRel]
option_le_transport_eq_some [instance, in coqrel.OptionRel]
option_map_ge [instance, in coqrel.OptionRel]
option_ge_trans [lemma, in coqrel.OptionRel]
option_ge_refl [lemma, in coqrel.OptionRel]
option_ge_rel [instance, in coqrel.OptionRel]
option_ge_subrel_params [instance, in coqrel.OptionRel]
option_ge_subrel [instance, in coqrel.OptionRel]
option_ge [inductive, in coqrel.OptionRel]
option_map_le [instance, in coqrel.OptionRel]
option_le_trans [lemma, in coqrel.OptionRel]
option_le_refl [lemma, in coqrel.OptionRel]
option_le_rel [instance, in coqrel.OptionRel]
option_le_subrel_params [instance, in coqrel.OptionRel]
option_le_subrel [instance, in coqrel.OptionRel]
option_le [inductive, in coqrel.OptionRel]
orb_leb [instance, in coqrel.BoolRel]
or_monotonic [instance, in coqrel.Relators]
P
pair_rel [instance, in coqrel.Relators]pointwise_relation_subrel_subrel [instance, in coqrel.MorphismsInterop]
pointwise_relation_relim [lemma, in coqrel.MorphismsInterop]
pointwise_relation_rintro [lemma, in coqrel.MorphismsInterop]
pointwise_relation_params [instance, in coqrel.MorphismsInterop]
pointwise_relation_subrel [instance, in coqrel.MorphismsInterop]
PolarityResolved [record, in coqrel.RelDefinitions]
PreOrderTactic [library]
prod_rel_preorder [lemma, in coqrel.Relators]
prod_rel_sym [lemma, in coqrel.Relators]
prod_rel_trans [lemma, in coqrel.Relators]
prod_rel_corefl [lemma, in coqrel.Relators]
prod_rel_refl [lemma, in coqrel.Relators]
prod_rdestruct [instance, in coqrel.Relators]
prod_subrel_params [instance, in coqrel.Relators]
prod_subrel [instance, in coqrel.Relators]
prod_rel [definition, in coqrel.Relators]
prod_rel_transport_eq_pair [instance, in coqrel.Transport]
prod_klr [definition, in coqrel.KLR]
psat [inductive, in coqrel.RelOperators]
psat_corefl [lemma, in coqrel.RelOperators]
psat_subrel_params [instance, in coqrel.RelOperators]
psat_subrel [instance, in coqrel.RelOperators]
psat_intro [constructor, in coqrel.RelOperators]
Q
QueryParams [record, in coqrel.Monotonicity]query_params_both [lemma, in coqrel.Monotonicity]
query_params_one [lemma, in coqrel.Monotonicity]
R
rauto [projection, in coqrel.RelDefinitions]RAuto [record, in coqrel.RelDefinitions]
rauto [constructor, in coqrel.RelDefinitions]
RAuto [inductive, in coqrel.RelDefinitions]
RAutoSubgoals [record, in coqrel.RelDefinitions]
RAutoSubgoals [inductive, in coqrel.RelDefinitions]
rauto_rstep [instance, in coqrel.RelDefinitions]
rauto_subgoals [projection, in coqrel.RelDefinitions]
rauto_subgoals [constructor, in coqrel.RelDefinitions]
rcompose [projection, in coqrel.RelClasses]
RCompose [record, in coqrel.RelClasses]
rcompose [constructor, in coqrel.RelClasses]
RCompose [inductive, in coqrel.RelClasses]
rcompose_transitive [instance, in coqrel.RelClasses]
rcompose_subrel [instance, in coqrel.RelOperators]
rdecompose [projection, in coqrel.RelClasses]
RDecompose [record, in coqrel.RelClasses]
rdecompose [constructor, in coqrel.RelClasses]
RDecompose [inductive, in coqrel.RelClasses]
rdecompose_subrel [instance, in coqrel.RelOperators]
rdestruct [projection, in coqrel.RelDefinitions]
RDestruct [record, in coqrel.RelDefinitions]
rdestruct [constructor, in coqrel.RelDefinitions]
RDestruct [inductive, in coqrel.RelDefinitions]
RDestruct [library]
rdestruct_remember_rintro [lemma, in coqrel.RDestruct]
rdestruct_forget_rintro [lemma, in coqrel.RDestruct]
rdestruct_remember_intro [constructor, in coqrel.RDestruct]
rdestruct_remember [inductive, in coqrel.RDestruct]
rdestruct_rstep [lemma, in coqrel.RDestruct]
rdestruct_result [definition, in coqrel.RDestruct]
reflexivity_rstep [lemma, in coqrel.RelDefinitions]
rel [definition, in coqrel.RelDefinitions]
related [projection, in coqrel.RelDefinitions]
Related [record, in coqrel.RelDefinitions]
related [constructor, in coqrel.RelDefinitions]
Related [inductive, in coqrel.RelDefinitions]
Relators [library]
RelClasses [library]
RelDefinitions [library]
relim [projection, in coqrel.RelDefinitions]
RElim [record, in coqrel.RelDefinitions]
relim [constructor, in coqrel.RelDefinitions]
RElim [inductive, in coqrel.RelDefinitions]
relim_base [instance, in coqrel.RelDefinitions]
RelOperators [library]
rel_top_component_trsym [lemma, in coqrel.LogicalRelationsTests]
rel_top_component_refl [lemma, in coqrel.LogicalRelationsTests]
rel_ex_1 [lemma, in coqrel.LogicalRelationsTests]
rel_all_1 [lemma, in coqrel.LogicalRelationsTests]
rel_pull_2 [lemma, in coqrel.LogicalRelationsTests]
rel_curry2_set_le_transport [lemma, in coqrel.Transport]
rel_curry_set_le_transport [lemma, in coqrel.Transport]
rel_incr_rdestruct [lemma, in coqrel.RelOperators]
rel_incr_rintro [lemma, in coqrel.RelOperators]
rel_incr_subrel_params [instance, in coqrel.RelOperators]
rel_incr_subrel [instance, in coqrel.RelOperators]
rel_incr [definition, in coqrel.RelOperators]
rel_ex_relim [lemma, in coqrel.RelOperators]
rel_ex_rintro [lemma, in coqrel.RelOperators]
rel_ex [definition, in coqrel.RelOperators]
rel_all_relim [lemma, in coqrel.RelOperators]
rel_all_rintro [lemma, in coqrel.RelOperators]
rel_all [definition, in coqrel.RelOperators]
rel_curry_relim [lemma, in coqrel.RelOperators]
rel_uncurry [definition, in coqrel.RelOperators]
rel_curry [definition, in coqrel.RelOperators]
rel_push_snd_rexists [lemma, in coqrel.RelOperators]
rel_push_fst_rexists [lemma, in coqrel.RelOperators]
rel_push_corefl [lemma, in coqrel.RelOperators]
rel_push_subrel_params [instance, in coqrel.RelOperators]
rel_push_subrel [instance, in coqrel.RelOperators]
rel_push_rintro [constructor, in coqrel.RelOperators]
rel_push [inductive, in coqrel.RelOperators]
rel_pull_relim [lemma, in coqrel.RelOperators]
rel_pull_rintro [lemma, in coqrel.RelOperators]
rel_pull_rcompose [lemma, in coqrel.RelOperators]
rel_pull_sym [lemma, in coqrel.RelOperators]
rel_pull_refl [lemma, in coqrel.RelOperators]
rel_pull_subrel_params [instance, in coqrel.RelOperators]
rel_pull_subrel [instance, in coqrel.RelOperators]
rel_pull [definition, in coqrel.RelOperators]
rel_compose_rdecompose [instance, in coqrel.RelOperators]
rel_compose_rcompose [instance, in coqrel.RelOperators]
rel_compose_assoc [lemma, in coqrel.RelOperators]
rel_compose_id_right [lemma, in coqrel.RelOperators]
rel_compose_id_left [lemma, in coqrel.RelOperators]
rel_compose_params [instance, in coqrel.RelOperators]
rel_compose_eqrel [instance, in coqrel.RelOperators]
rel_compose_subrel [instance, in coqrel.RelOperators]
rel_compose [definition, in coqrel.RelOperators]
rel_top_equiv [instance, in coqrel.RelOperators]
rel_top_rintro [lemma, in coqrel.RelOperators]
rel_top [definition, in coqrel.RelOperators]
rel_bot_relim [lemma, in coqrel.RelOperators]
rel_bot_subrel [lemma, in coqrel.RelOperators]
rel_bot [definition, in coqrel.RelOperators]
rel_impl_subrel_codomain [lemma, in coqrel.RelOperators]
rel_impl_relim [lemma, in coqrel.RelOperators]
rel_impl_rintro [lemma, in coqrel.RelOperators]
rel_impl_subrel_params [instance, in coqrel.RelOperators]
rel_impl_subrel [instance, in coqrel.RelOperators]
rel_impl [definition, in coqrel.RelOperators]
rel_inter_flip_sym [instance, in coqrel.RelOperators]
rel_inter_sym [lemma, in coqrel.RelOperators]
rel_inter_trans [lemma, in coqrel.RelOperators]
rel_inter_corefl_r [lemma, in coqrel.RelOperators]
rel_inter_corefl_l [lemma, in coqrel.RelOperators]
rel_inter_refl [lemma, in coqrel.RelOperators]
rel_inter_glb [lemma, in coqrel.RelOperators]
rel_inter_subrel_rexists_r [lemma, in coqrel.RelOperators]
rel_inter_subrel_rexists_l [lemma, in coqrel.RelOperators]
rel_inter_rexists [lemma, in coqrel.RelOperators]
rel_inter_params [instance, in coqrel.RelOperators]
rel_inter_subrel [instance, in coqrel.RelOperators]
rel_inter [definition, in coqrel.RelOperators]
rel_union_sym [lemma, in coqrel.RelOperators]
rel_union_corefl [lemma, in coqrel.RelOperators]
rel_union_refl_r [lemma, in coqrel.RelOperators]
rel_union_refl_l [lemma, in coqrel.RelOperators]
rel_union_lub [lemma, in coqrel.RelOperators]
rel_union_subrel_rexists_r [lemma, in coqrel.RelOperators]
rel_union_subrel_rexists_l [lemma, in coqrel.RelOperators]
rel_union_rexists_r [lemma, in coqrel.RelOperators]
rel_union_rexists_l [lemma, in coqrel.RelOperators]
rel_union_subrel_params [instance, in coqrel.RelOperators]
rel_union_subrel [instance, in coqrel.RelOperators]
rel_union [definition, in coqrel.RelOperators]
rel_kvd_subrel_params [instance, in coqrel.KLR]
rel_kvd_relim [lemma, in coqrel.KLR]
rel_kvd_rintro [lemma, in coqrel.KLR]
rel_kvd_subrel [instance, in coqrel.KLR]
rel_kvd [definition, in coqrel.KLR]
RemoveAllParams [record, in coqrel.Monotonicity]
RemoveParams [record, in coqrel.Monotonicity]
remove_all_params_candidate [instance, in coqrel.Monotonicity]
remove_params_candidate [instance, in coqrel.Monotonicity]
req [inductive, in coqrel.RelOperators]
req_corefl [lemma, in coqrel.RelOperators]
req_rintro [lemma, in coqrel.RelOperators]
req_intro [constructor, in coqrel.RelOperators]
respectful_relim [lemma, in coqrel.MorphismsInterop]
respectful_rintro [lemma, in coqrel.MorphismsInterop]
respectful_params [instance, in coqrel.MorphismsInterop]
respectful_subrel [instance, in coqrel.MorphismsInterop]
rexists [projection, in coqrel.RelDefinitions]
RExists [record, in coqrel.RelDefinitions]
rexists [constructor, in coqrel.RelDefinitions]
RExists [inductive, in coqrel.RelDefinitions]
rexists_rstep [instance, in coqrel.RelDefinitions]
rgraph_queue_cons [constructor, in coqrel.PreOrderTactic]
rgraph_queue_nil [constructor, in coqrel.PreOrderTactic]
rgraph_queue [inductive, in coqrel.PreOrderTactic]
rgraph_done [definition, in coqrel.PreOrderTactic]
right_le [constructor, in coqrel.BoolRel]
right_rel [instance, in coqrel.BoolRel]
right_rel_def [constructor, in coqrel.BoolRel]
rimpl [projection, in coqrel.Monotonicity]
RImpl [record, in coqrel.Monotonicity]
rimpl [constructor, in coqrel.Monotonicity]
RImpl [inductive, in coqrel.Monotonicity]
rimpl_flip_subrel [instance, in coqrel.Monotonicity]
rimpl_subrel [instance, in coqrel.Monotonicity]
rimpl_refl [instance, in coqrel.Monotonicity]
rintro [projection, in coqrel.RelDefinitions]
RIntro [record, in coqrel.RelDefinitions]
rintro [constructor, in coqrel.RelDefinitions]
RIntro [inductive, in coqrel.RelDefinitions]
rintro_rstep [instance, in coqrel.RelDefinitions]
rsat [definition, in coqrel.RelOperators]
rsat_subrel_params [instance, in coqrel.RelOperators]
rsat_subrel [instance, in coqrel.RelOperators]
rstep [projection, in coqrel.RelDefinitions]
RStep [record, in coqrel.RelDefinitions]
rstep [constructor, in coqrel.RelDefinitions]
RStep [inductive, in coqrel.RelDefinitions]
S
set_ge_compose [instance, in coqrel.Relators]set_ge_refl [lemma, in coqrel.Relators]
set_ge_subrel_params [instance, in coqrel.Relators]
set_ge_subrel [instance, in coqrel.Relators]
set_ge [definition, in coqrel.Relators]
set_le_compose [instance, in coqrel.Relators]
set_le_refl [lemma, in coqrel.Relators]
set_le_subrel_params [instance, in coqrel.Relators]
set_le_subrel [instance, in coqrel.Relators]
set_le [definition, in coqrel.Relators]
set_le_transport [lemma, in coqrel.Transport]
set_kge [definition, in coqrel.KLR]
set_kle [definition, in coqrel.KLR]
snd_rel [instance, in coqrel.Relators]
Some_rel [instance, in coqrel.Relators]
Some_rel_def [constructor, in coqrel.Relators]
Some_ge [instance, in coqrel.OptionRel]
Some_ge_def [constructor, in coqrel.OptionRel]
Some_le [instance, in coqrel.OptionRel]
Some_le_def [constructor, in coqrel.OptionRel]
subrel [definition, in coqrel.RelDefinitions]
subrelation_subrel [lemma, in coqrel.MorphismsInterop]
SubrelMonotonicity [record, in coqrel.Monotonicity]
SubrelMonotonicity [inductive, in coqrel.Monotonicity]
subrel_impl_relim [instance, in coqrel.RelDefinitions]
subrel_preorder [instance, in coqrel.RelDefinitions]
subrel_eq [instance, in coqrel.RelClasses]
subrel_sym_flip [lemma, in coqrel.RelOperators]
subrel_monotonicity [projection, in coqrel.Monotonicity]
subrel_monotonicity [constructor, in coqrel.Monotonicity]
sumbool_le [inductive, in coqrel.BoolRel]
sumbool_rel [inductive, in coqrel.BoolRel]
sum_rel_preorder [lemma, in coqrel.Relators]
sum_rel_sym [lemma, in coqrel.Relators]
sum_rel_trans [lemma, in coqrel.Relators]
sum_rel_corefl [lemma, in coqrel.Relators]
sum_rel_refl [lemma, in coqrel.Relators]
sum_subrel_params [instance, in coqrel.Relators]
sum_subrel [instance, in coqrel.Relators]
sum_rel [inductive, in coqrel.Relators]
sum_klr [definition, in coqrel.KLR]
T
transitive_rcompose [lemma, in coqrel.RelClasses]transport [projection, in coqrel.Transport]
Transport [record, in coqrel.Transport]
transport [constructor, in coqrel.Transport]
Transport [inductive, in coqrel.Transport]
Transport [library]
transport_in_goal [lemma, in coqrel.Transport]
true_leb [lemma, in coqrel.BoolRel]
tt_rel [constructor, in coqrel.Relators]
U
unconvertible [projection, in coqrel.RelDefinitions]Unconvertible [record, in coqrel.RelDefinitions]
unconvertible [constructor, in coqrel.RelDefinitions]
Unconvertible [inductive, in coqrel.RelDefinitions]
uncurry [definition, in coqrel.RelOperators]
UnfoldUncurry [record, in coqrel.RelOperators]
UnfoldUncurry [inductive, in coqrel.RelOperators]
unfold_monotonic_rstep [lemma, in coqrel.RelDefinitions]
unfold_uncurry_before_after [projection, in coqrel.RelOperators]
unfold_uncurry_before_after [constructor, in coqrel.RelOperators]
unit_rel [inductive, in coqrel.Relators]
UNKRIPKIFY [section, in coqrel.KLR]
USUAL [section, in coqrel.KLR]
other
_ @@ [ _ ] (klr_scope) [notation, in coqrel.KLR]<> * _ (klr_scope) [notation, in coqrel.KLR]
[] -> _ (klr_scope) [notation, in coqrel.KLR]
<> _ (klr_scope) [notation, in coqrel.KLR]
[] _ (klr_scope) [notation, in coqrel.KLR]
< _ > _ (klr_scope) [notation, in coqrel.KLR]
[ _ ] _ (klr_scope) [notation, in coqrel.KLR]
% _ (klr_scope) [notation, in coqrel.KLR]
_ /\ _ (klr_scope) [notation, in coqrel.KLR]
_ \/ _ (klr_scope) [notation, in coqrel.KLR]
_ + _ (klr_scope) [notation, in coqrel.KLR]
_ * _ (klr_scope) [notation, in coqrel.KLR]
- ==> _ (klr_scope) [notation, in coqrel.KLR]
_ --> _ (klr_scope) [notation, in coqrel.KLR]
_ ++> _ (klr_scope) [notation, in coqrel.KLR]
_ ==> _ (klr_scope) [notation, in coqrel.KLR]
_ * _ (rel_scope) [notation, in coqrel.Relators]
_ + _ (rel_scope) [notation, in coqrel.Relators]
forallr _ _ : _ , _ (rel_scope) [notation, in coqrel.Relators]
- ==> _ (rel_scope) [notation, in coqrel.Relators]
forallr _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ : _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ @ _ _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
forallr _ @ _ _ : _ , _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ --> _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ ++> _ (rel_scope) [notation, in coqrel.RelDefinitions]
_ ==> _ (rel_scope) [notation, in coqrel.RelDefinitions]
rexists _ .. _ , _ (rel_scope) [notation, in coqrel.RelOperators]
rforall _ .. _ , _ (rel_scope) [notation, in coqrel.RelOperators]
% _ (rel_scope) [notation, in coqrel.RelOperators]
_ !! ( _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ !! _ (rel_scope) [notation, in coqrel.RelOperators]
_ !! ( _ , _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ @@ ( _ ) (rel_scope) [notation, in coqrel.RelOperators]
_ @@ _ (rel_scope) [notation, in coqrel.RelOperators]
_ @@ ( _ , _ ) (rel_scope) [notation, in coqrel.RelOperators]
⊤ (rel_scope) [notation, in coqrel.RelOperators]
⊥ (rel_scope) [notation, in coqrel.RelOperators]
_ /\ _ (rel_scope) [notation, in coqrel.RelOperators]
_ \/ _ (rel_scope) [notation, in coqrel.RelOperators]
|= _ (rel_scope) [notation, in coqrel.KLR]
_ ~> _ [notation, in coqrel.KLR]
forallr - , _ [notation, in coqrel.Relators]
forallr - : _ , _ [notation, in coqrel.Relators]
forallr - @ _ , _ [notation, in coqrel.Relators]
forallr - @ _ : _ , _ [notation, in coqrel.Relators]
@ Monotonic _ _ _ [notation, in coqrel.RelDefinitions]
Notation Index
other
_ @@ [ _ ] (klr_scope) [in coqrel.KLR]<> * _ (klr_scope) [in coqrel.KLR]
[] -> _ (klr_scope) [in coqrel.KLR]
<> _ (klr_scope) [in coqrel.KLR]
[] _ (klr_scope) [in coqrel.KLR]
< _ > _ (klr_scope) [in coqrel.KLR]
[ _ ] _ (klr_scope) [in coqrel.KLR]
% _ (klr_scope) [in coqrel.KLR]
_ /\ _ (klr_scope) [in coqrel.KLR]
_ \/ _ (klr_scope) [in coqrel.KLR]
_ + _ (klr_scope) [in coqrel.KLR]
_ * _ (klr_scope) [in coqrel.KLR]
- ==> _ (klr_scope) [in coqrel.KLR]
_ --> _ (klr_scope) [in coqrel.KLR]
_ ++> _ (klr_scope) [in coqrel.KLR]
_ ==> _ (klr_scope) [in coqrel.KLR]
_ * _ (rel_scope) [in coqrel.Relators]
_ + _ (rel_scope) [in coqrel.Relators]
forallr _ _ : _ , _ (rel_scope) [in coqrel.Relators]
- ==> _ (rel_scope) [in coqrel.Relators]
forallr _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ : _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ @ _ _ , _ (rel_scope) [in coqrel.RelDefinitions]
forallr _ @ _ _ : _ , _ (rel_scope) [in coqrel.RelDefinitions]
_ --> _ (rel_scope) [in coqrel.RelDefinitions]
_ ++> _ (rel_scope) [in coqrel.RelDefinitions]
_ ==> _ (rel_scope) [in coqrel.RelDefinitions]
rexists _ .. _ , _ (rel_scope) [in coqrel.RelOperators]
rforall _ .. _ , _ (rel_scope) [in coqrel.RelOperators]
% _ (rel_scope) [in coqrel.RelOperators]
_ !! ( _ ) (rel_scope) [in coqrel.RelOperators]
_ !! _ (rel_scope) [in coqrel.RelOperators]
_ !! ( _ , _ ) (rel_scope) [in coqrel.RelOperators]
_ @@ ( _ ) (rel_scope) [in coqrel.RelOperators]
_ @@ _ (rel_scope) [in coqrel.RelOperators]
_ @@ ( _ , _ ) (rel_scope) [in coqrel.RelOperators]
⊤ (rel_scope) [in coqrel.RelOperators]
⊥ (rel_scope) [in coqrel.RelOperators]
_ /\ _ (rel_scope) [in coqrel.RelOperators]
_ \/ _ (rel_scope) [in coqrel.RelOperators]
|= _ (rel_scope) [in coqrel.KLR]
_ ~> _ [in coqrel.KLR]
forallr - , _ [in coqrel.Relators]
forallr - : _ , _ [in coqrel.Relators]
forallr - @ _ , _ [in coqrel.Relators]
forallr - @ _ : _ , _ [in coqrel.Relators]
@ Monotonic _ _ _ [in coqrel.RelDefinitions]
Module Index
D
Delay [in coqrel.Delay]Library Index
B
BoolRelD
DelayK
KLRL
LogicalRelationsLogicalRelationsTests
M
MonotonicityMorphismsInterop
O
OptionRelP
PreOrderTacticR
RDestructRelators
RelClasses
RelDefinitions
RelOperators
T
TransportLemma Index
A
arrow_pointwise_refl [in coqrel.Relators]arrow_pointwise_relim [in coqrel.Relators]
arrow_pointwise_rintro [in coqrel.Relators]
arrow_relim [in coqrel.RelDefinitions]
arrow_rintro [in coqrel.RelDefinitions]
D
direct_rexists [in coqrel.RelDefinitions]F
false_leb [in coqrel.BoolRel]flip_rexists [in coqrel.RelDefinitions]
flip_rdestruct [in coqrel.RelDefinitions]
flip_relim [in coqrel.RelDefinitions]
flip_rintro [in coqrel.RelDefinitions]
flip_context_candidate [in coqrel.Monotonicity]
fold_impl_rstep [in coqrel.Relators]
forallp_relim [in coqrel.Relators]
forallp_rintro [in coqrel.Relators]
forall_pointwise_relim [in coqrel.Relators]
forall_pointwise_rintro [in coqrel.Relators]
forall_relation_relim [in coqrel.MorphismsInterop]
forall_relation_rintro [in coqrel.MorphismsInterop]
forall_relim [in coqrel.RelDefinitions]
forall_rintro [in coqrel.RelDefinitions]
f_equal_relim [in coqrel.Monotonicity]
I
impl_transport [in coqrel.Transport]K
klr_pullw_relim [in coqrel.KLR]klr_pullw_rintro [in coqrel.KLR]
klr_diam_relim [in coqrel.KLR]
klr_diam_rintro [in coqrel.KLR]
klr_box_relim [in coqrel.KLR]
klr_box_rintro [in coqrel.KLR]
k_relim [in coqrel.KLR]
k_rintro [in coqrel.KLR]
k1_relim [in coqrel.KLR]
k1_rintro [in coqrel.KLR]
k2_relim [in coqrel.KLR]
k2_rintro [in coqrel.KLR]
L
leb_rdestruct [in coqrel.BoolRel]list_rel_trans [in coqrel.Relators]
list_rel_sym [in coqrel.Relators]
list_rel_corefl [in coqrel.Relators]
list_rel_refl [in coqrel.Relators]
N
None_ge [in coqrel.OptionRel]None_le [in coqrel.OptionRel]
O
option_rel_some_inv [in coqrel.Relators]option_rel_refl [in coqrel.Relators]
option_ge_trans [in coqrel.OptionRel]
option_ge_refl [in coqrel.OptionRel]
option_le_trans [in coqrel.OptionRel]
option_le_refl [in coqrel.OptionRel]
P
pointwise_relation_relim [in coqrel.MorphismsInterop]pointwise_relation_rintro [in coqrel.MorphismsInterop]
prod_rel_preorder [in coqrel.Relators]
prod_rel_sym [in coqrel.Relators]
prod_rel_trans [in coqrel.Relators]
prod_rel_corefl [in coqrel.Relators]
prod_rel_refl [in coqrel.Relators]
psat_corefl [in coqrel.RelOperators]
Q
query_params_both [in coqrel.Monotonicity]query_params_one [in coqrel.Monotonicity]
R
rdestruct_remember_rintro [in coqrel.RDestruct]rdestruct_forget_rintro [in coqrel.RDestruct]
rdestruct_rstep [in coqrel.RDestruct]
reflexivity_rstep [in coqrel.RelDefinitions]
rel_top_component_trsym [in coqrel.LogicalRelationsTests]
rel_top_component_refl [in coqrel.LogicalRelationsTests]
rel_ex_1 [in coqrel.LogicalRelationsTests]
rel_all_1 [in coqrel.LogicalRelationsTests]
rel_pull_2 [in coqrel.LogicalRelationsTests]
rel_curry2_set_le_transport [in coqrel.Transport]
rel_curry_set_le_transport [in coqrel.Transport]
rel_incr_rdestruct [in coqrel.RelOperators]
rel_incr_rintro [in coqrel.RelOperators]
rel_ex_relim [in coqrel.RelOperators]
rel_ex_rintro [in coqrel.RelOperators]
rel_all_relim [in coqrel.RelOperators]
rel_all_rintro [in coqrel.RelOperators]
rel_curry_relim [in coqrel.RelOperators]
rel_push_snd_rexists [in coqrel.RelOperators]
rel_push_fst_rexists [in coqrel.RelOperators]
rel_push_corefl [in coqrel.RelOperators]
rel_pull_relim [in coqrel.RelOperators]
rel_pull_rintro [in coqrel.RelOperators]
rel_pull_rcompose [in coqrel.RelOperators]
rel_pull_sym [in coqrel.RelOperators]
rel_pull_refl [in coqrel.RelOperators]
rel_compose_assoc [in coqrel.RelOperators]
rel_compose_id_right [in coqrel.RelOperators]
rel_compose_id_left [in coqrel.RelOperators]
rel_top_rintro [in coqrel.RelOperators]
rel_bot_relim [in coqrel.RelOperators]
rel_bot_subrel [in coqrel.RelOperators]
rel_impl_subrel_codomain [in coqrel.RelOperators]
rel_impl_relim [in coqrel.RelOperators]
rel_impl_rintro [in coqrel.RelOperators]
rel_inter_sym [in coqrel.RelOperators]
rel_inter_trans [in coqrel.RelOperators]
rel_inter_corefl_r [in coqrel.RelOperators]
rel_inter_corefl_l [in coqrel.RelOperators]
rel_inter_refl [in coqrel.RelOperators]
rel_inter_glb [in coqrel.RelOperators]
rel_inter_subrel_rexists_r [in coqrel.RelOperators]
rel_inter_subrel_rexists_l [in coqrel.RelOperators]
rel_inter_rexists [in coqrel.RelOperators]
rel_union_sym [in coqrel.RelOperators]
rel_union_corefl [in coqrel.RelOperators]
rel_union_refl_r [in coqrel.RelOperators]
rel_union_refl_l [in coqrel.RelOperators]
rel_union_lub [in coqrel.RelOperators]
rel_union_subrel_rexists_r [in coqrel.RelOperators]
rel_union_subrel_rexists_l [in coqrel.RelOperators]
rel_union_rexists_r [in coqrel.RelOperators]
rel_union_rexists_l [in coqrel.RelOperators]
rel_kvd_relim [in coqrel.KLR]
rel_kvd_rintro [in coqrel.KLR]
req_corefl [in coqrel.RelOperators]
req_rintro [in coqrel.RelOperators]
respectful_relim [in coqrel.MorphismsInterop]
respectful_rintro [in coqrel.MorphismsInterop]
S
set_ge_refl [in coqrel.Relators]set_le_refl [in coqrel.Relators]
set_le_transport [in coqrel.Transport]
subrelation_subrel [in coqrel.MorphismsInterop]
subrel_sym_flip [in coqrel.RelOperators]
sum_rel_preorder [in coqrel.Relators]
sum_rel_sym [in coqrel.Relators]
sum_rel_trans [in coqrel.Relators]
sum_rel_corefl [in coqrel.Relators]
sum_rel_refl [in coqrel.Relators]
T
transitive_rcompose [in coqrel.RelClasses]transport_in_goal [in coqrel.Transport]
true_leb [in coqrel.BoolRel]
U
unfold_monotonic_rstep [in coqrel.RelDefinitions]Constructor Index
C
candidate_related [in coqrel.Monotonicity]cons_rel_def [in coqrel.Relators]
convertible [in coqrel.RelDefinitions]
coreflexivity [in coqrel.RelClasses]
E
eapply [in coqrel.Delay]I
inl_rel_def [in coqrel.Relators]inr_rel_def [in coqrel.Relators]
K
klr_inr [in coqrel.KLR]klr_inl [in coqrel.KLR]
L
left_le [in coqrel.BoolRel]left_rel_def [in coqrel.BoolRel]
M
monotonicity [in coqrel.Monotonicity]N
nil_rel_def [in coqrel.Relators]nondelayed [in coqrel.Delay]
None_rel_def [in coqrel.Relators]
None_ge_def [in coqrel.OptionRel]
None_le_def [in coqrel.OptionRel]
O
once [in coqrel.RelDefinitions]P
psat_intro [in coqrel.RelOperators]R
rauto [in coqrel.RelDefinitions]rauto_subgoals [in coqrel.RelDefinitions]
rcompose [in coqrel.RelClasses]
rdecompose [in coqrel.RelClasses]
rdestruct [in coqrel.RelDefinitions]
rdestruct_remember_intro [in coqrel.RDestruct]
related [in coqrel.RelDefinitions]
relim [in coqrel.RelDefinitions]
rel_push_rintro [in coqrel.RelOperators]
req_intro [in coqrel.RelOperators]
rexists [in coqrel.RelDefinitions]
rgraph_queue_cons [in coqrel.PreOrderTactic]
rgraph_queue_nil [in coqrel.PreOrderTactic]
right_le [in coqrel.BoolRel]
right_rel_def [in coqrel.BoolRel]
rimpl [in coqrel.Monotonicity]
rintro [in coqrel.RelDefinitions]
rstep [in coqrel.RelDefinitions]
S
Some_rel_def [in coqrel.Relators]Some_ge_def [in coqrel.OptionRel]
Some_le_def [in coqrel.OptionRel]
subrel_monotonicity [in coqrel.Monotonicity]
T
transport [in coqrel.Transport]tt_rel [in coqrel.Relators]
U
unconvertible [in coqrel.RelDefinitions]unfold_uncurry_before_after [in coqrel.RelOperators]
Inductive Index
C
CandidateProperty [in coqrel.Monotonicity]Convertible [in coqrel.RelDefinitions]
Coreflexive [in coqrel.RelClasses]
E
EApply [in coqrel.Delay]Empty_set_rel [in coqrel.Relators]
K
klr_sum [in coqrel.KLR]L
list_rel [in coqrel.Relators]M
Monotonicity [in coqrel.Monotonicity]N
NonDelayed [in coqrel.Delay]O
Once [in coqrel.RelDefinitions]option_rel [in coqrel.Relators]
option_ge [in coqrel.OptionRel]
option_le [in coqrel.OptionRel]
P
psat [in coqrel.RelOperators]R
RAuto [in coqrel.RelDefinitions]RAutoSubgoals [in coqrel.RelDefinitions]
RCompose [in coqrel.RelClasses]
RDecompose [in coqrel.RelClasses]
RDestruct [in coqrel.RelDefinitions]
rdestruct_remember [in coqrel.RDestruct]
Related [in coqrel.RelDefinitions]
RElim [in coqrel.RelDefinitions]
rel_push [in coqrel.RelOperators]
req [in coqrel.RelOperators]
RExists [in coqrel.RelDefinitions]
rgraph_queue [in coqrel.PreOrderTactic]
RImpl [in coqrel.Monotonicity]
RIntro [in coqrel.RelDefinitions]
RStep [in coqrel.RelDefinitions]
S
SubrelMonotonicity [in coqrel.Monotonicity]sumbool_le [in coqrel.BoolRel]
sumbool_rel [in coqrel.BoolRel]
sum_rel [in coqrel.Relators]
T
Transport [in coqrel.Transport]U
Unconvertible [in coqrel.RelDefinitions]UnfoldUncurry [in coqrel.RelOperators]
unit_rel [in coqrel.Relators]
Projection Index
A
acc [in coqrel.KLR]C
candidate_related [in coqrel.Monotonicity]convertible [in coqrel.RelDefinitions]
coreflexivity [in coqrel.RelClasses]
D
Delay.open_conjunction_proj [in coqrel.Delay]E
eapply [in coqrel.Delay]M
monotonicity [in coqrel.Monotonicity]N
nondelayed [in coqrel.Delay]O
once [in coqrel.RelDefinitions]R
rauto [in coqrel.RelDefinitions]rauto_subgoals [in coqrel.RelDefinitions]
rcompose [in coqrel.RelClasses]
rdecompose [in coqrel.RelClasses]
rdestruct [in coqrel.RelDefinitions]
related [in coqrel.RelDefinitions]
relim [in coqrel.RelDefinitions]
rexists [in coqrel.RelDefinitions]
rimpl [in coqrel.Monotonicity]
rintro [in coqrel.RelDefinitions]
rstep [in coqrel.RelDefinitions]
S
subrel_monotonicity [in coqrel.Monotonicity]T
transport [in coqrel.Transport]U
unconvertible [in coqrel.RelDefinitions]unfold_uncurry_before_after [in coqrel.RelOperators]
Instance Index
A
all_monotonic_params [in coqrel.Relators]all_monotonic [in coqrel.Relators]
andb_leb [in coqrel.BoolRel]
and_monotonic [in coqrel.Relators]
apply_candidate_subrel [in coqrel.Monotonicity]
apply_candidate [in coqrel.Monotonicity]
app_rel [in coqrel.Relators]
arrow_pointwise_rel_compose [in coqrel.Relators]
arrow_pointwise_subrel_params [in coqrel.Relators]
arrow_pointwise_subrel [in coqrel.Relators]
arrow_subrel_params [in coqrel.RelDefinitions]
arrow_subrel [in coqrel.RelDefinitions]
arrow_rdecompose [in coqrel.RelClasses]
arrow_rcompose [in coqrel.RelClasses]
arrow_corefl [in coqrel.RelClasses]
arrow_refl [in coqrel.RelClasses]
as_is_candidate [in coqrel.Monotonicity]
C
cons_rel [in coqrel.Relators]E
eqrel_subrel [in coqrel.RelOperators]eqrel_equivalence [in coqrel.RelOperators]
eq_subrel [in coqrel.RelDefinitions]
eq_corefl [in coqrel.RelClasses]
eq_candidate [in coqrel.Monotonicity]
ex_monotonic_params [in coqrel.Relators]
ex_monotonic [in coqrel.Relators]
F
flip_subrel_params [in coqrel.RelDefinitions]flip_subrel [in coqrel.RelDefinitions]
fold_left_rel [in coqrel.Relators]
fold_right_rel [in coqrel.Relators]
forall_relation_params [in coqrel.MorphismsInterop]
forall_relation_subrel [in coqrel.MorphismsInterop]
fst_rel [in coqrel.Relators]
I
implb_leb [in coqrel.BoolRel]inl_rel [in coqrel.Relators]
inr_rel [in coqrel.Relators]
K
klr_pullw_subrel_params [in coqrel.KLR]klr_pullw_subrel [in coqrel.KLR]
klr_diam_subrel_params [in coqrel.KLR]
klr_box_subrel_params [in coqrel.KLR]
klr_diam_subrel [in coqrel.KLR]
klr_box_subrel [in coqrel.KLR]
k_rel_params [in coqrel.KLR]
k_rel [in coqrel.KLR]
k1_rel_params [in coqrel.KLR]
k1_rel [in coqrel.KLR]
k2_rel_params [in coqrel.KLR]
k2_unfold [in coqrel.KLR]
k2_rel [in coqrel.KLR]
L
leb_transport_eq_true [in coqrel.BoolRel]leb_preo [in coqrel.BoolRel]
left_rel [in coqrel.BoolRel]
length_rel [in coqrel.Relators]
list_subrel_params [in coqrel.Relators]
list_subrel [in coqrel.Relators]
lsat_subrel_params [in coqrel.RelOperators]
lsat_subrel [in coqrel.RelOperators]
M
map_rel [in coqrel.Relators]monotonicity_rstep [in coqrel.Monotonicity]
morphisms_proper_related [in coqrel.MorphismsInterop]
N
negb_leb [in coqrel.BoolRel]nil_rel [in coqrel.Relators]
None_rel [in coqrel.Relators]
O
option_map_rel [in coqrel.Relators]option_subrel_params [in coqrel.Relators]
option_subrel [in coqrel.Relators]
option_ge_transport_eq_none [in coqrel.OptionRel]
option_le_transport_eq_some [in coqrel.OptionRel]
option_map_ge [in coqrel.OptionRel]
option_ge_rel [in coqrel.OptionRel]
option_ge_subrel_params [in coqrel.OptionRel]
option_ge_subrel [in coqrel.OptionRel]
option_map_le [in coqrel.OptionRel]
option_le_rel [in coqrel.OptionRel]
option_le_subrel_params [in coqrel.OptionRel]
option_le_subrel [in coqrel.OptionRel]
orb_leb [in coqrel.BoolRel]
or_monotonic [in coqrel.Relators]
P
pair_rel [in coqrel.Relators]pointwise_relation_subrel_subrel [in coqrel.MorphismsInterop]
pointwise_relation_params [in coqrel.MorphismsInterop]
pointwise_relation_subrel [in coqrel.MorphismsInterop]
prod_rdestruct [in coqrel.Relators]
prod_subrel_params [in coqrel.Relators]
prod_subrel [in coqrel.Relators]
prod_rel_transport_eq_pair [in coqrel.Transport]
psat_subrel_params [in coqrel.RelOperators]
psat_subrel [in coqrel.RelOperators]
R
rauto_rstep [in coqrel.RelDefinitions]rcompose_transitive [in coqrel.RelClasses]
rcompose_subrel [in coqrel.RelOperators]
rdecompose_subrel [in coqrel.RelOperators]
relim_base [in coqrel.RelDefinitions]
rel_incr_subrel_params [in coqrel.RelOperators]
rel_incr_subrel [in coqrel.RelOperators]
rel_push_subrel_params [in coqrel.RelOperators]
rel_push_subrel [in coqrel.RelOperators]
rel_pull_subrel_params [in coqrel.RelOperators]
rel_pull_subrel [in coqrel.RelOperators]
rel_compose_rdecompose [in coqrel.RelOperators]
rel_compose_rcompose [in coqrel.RelOperators]
rel_compose_params [in coqrel.RelOperators]
rel_compose_eqrel [in coqrel.RelOperators]
rel_compose_subrel [in coqrel.RelOperators]
rel_top_equiv [in coqrel.RelOperators]
rel_impl_subrel_params [in coqrel.RelOperators]
rel_impl_subrel [in coqrel.RelOperators]
rel_inter_flip_sym [in coqrel.RelOperators]
rel_inter_params [in coqrel.RelOperators]
rel_inter_subrel [in coqrel.RelOperators]
rel_union_subrel_params [in coqrel.RelOperators]
rel_union_subrel [in coqrel.RelOperators]
rel_kvd_subrel_params [in coqrel.KLR]
rel_kvd_subrel [in coqrel.KLR]
remove_all_params_candidate [in coqrel.Monotonicity]
remove_params_candidate [in coqrel.Monotonicity]
respectful_params [in coqrel.MorphismsInterop]
respectful_subrel [in coqrel.MorphismsInterop]
rexists_rstep [in coqrel.RelDefinitions]
right_rel [in coqrel.BoolRel]
rimpl_flip_subrel [in coqrel.Monotonicity]
rimpl_subrel [in coqrel.Monotonicity]
rimpl_refl [in coqrel.Monotonicity]
rintro_rstep [in coqrel.RelDefinitions]
rsat_subrel_params [in coqrel.RelOperators]
rsat_subrel [in coqrel.RelOperators]
S
set_ge_compose [in coqrel.Relators]set_ge_subrel_params [in coqrel.Relators]
set_ge_subrel [in coqrel.Relators]
set_le_compose [in coqrel.Relators]
set_le_subrel_params [in coqrel.Relators]
set_le_subrel [in coqrel.Relators]
snd_rel [in coqrel.Relators]
Some_rel [in coqrel.Relators]
Some_ge [in coqrel.OptionRel]
Some_le [in coqrel.OptionRel]
subrel_impl_relim [in coqrel.RelDefinitions]
subrel_preorder [in coqrel.RelDefinitions]
subrel_eq [in coqrel.RelClasses]
sum_subrel_params [in coqrel.Relators]
sum_subrel [in coqrel.Relators]
Section Index
A
ARROW_REL_COMPOSE [in coqrel.RelClasses]ARROW_MOD [in coqrel.KLR]
L
LIFT [in coqrel.KLR]M
MODALITIES [in coqrel.KLR]U
UNKRIPKIFY [in coqrel.KLR]USUAL [in coqrel.KLR]
Abbreviation Index
M
Monotonic [in coqrel.RelDefinitions]Definition Index
A
arrow_pointwise_rel [in coqrel.Relators]arrow_rel [in coqrel.RelDefinitions]
arrow_pointwise_klr [in coqrel.KLR]
arrow_klr [in coqrel.KLR]
C
curry [in coqrel.RelOperators]D
delay [in coqrel.Delay]Delay.delayed_goal [in coqrel.Delay]
Delay.unpack [in coqrel.Delay]
E
eqrel [in coqrel.RelOperators]F
forallp_rel [in coqrel.Relators]forall_pointwise_rel [in coqrel.Relators]
forall_rel [in coqrel.RelDefinitions]
K
k [in coqrel.KLR]klr [in coqrel.KLR]
klr_pullw [in coqrel.KLR]
klr_diamat [in coqrel.KLR]
klr_boxto [in coqrel.KLR]
klr_diam [in coqrel.KLR]
klr_box [in coqrel.KLR]
klr_curry [in coqrel.KLR]
klr_inter [in coqrel.KLR]
klr_union [in coqrel.KLR]
k1 [in coqrel.KLR]
k2 [in coqrel.KLR]
L
list_klr [in coqrel.KLR]lsat [in coqrel.RelOperators]
P
prod_rel [in coqrel.Relators]prod_klr [in coqrel.KLR]
R
rdestruct_result [in coqrel.RDestruct]rel [in coqrel.RelDefinitions]
rel_incr [in coqrel.RelOperators]
rel_ex [in coqrel.RelOperators]
rel_all [in coqrel.RelOperators]
rel_uncurry [in coqrel.RelOperators]
rel_curry [in coqrel.RelOperators]
rel_pull [in coqrel.RelOperators]
rel_compose [in coqrel.RelOperators]
rel_top [in coqrel.RelOperators]
rel_bot [in coqrel.RelOperators]
rel_impl [in coqrel.RelOperators]
rel_inter [in coqrel.RelOperators]
rel_union [in coqrel.RelOperators]
rel_kvd [in coqrel.KLR]
rgraph_done [in coqrel.PreOrderTactic]
rsat [in coqrel.RelOperators]
S
set_ge [in coqrel.Relators]set_le [in coqrel.Relators]
set_kge [in coqrel.KLR]
set_kle [in coqrel.KLR]
subrel [in coqrel.RelDefinitions]
sum_klr [in coqrel.KLR]
U
uncurry [in coqrel.RelOperators]Record Index
C
CandidateProperty [in coqrel.Monotonicity]CommonPrefix [in coqrel.Monotonicity]
Convertible [in coqrel.RelDefinitions]
Coreflexive [in coqrel.RelClasses]
D
Delay.open_conjunction [in coqrel.Delay]E
EApply [in coqrel.Delay]K
KripkeFrame [in coqrel.KLR]M
Monotonicity [in coqrel.Monotonicity]N
NonDelayed [in coqrel.Delay]NotEvar [in coqrel.RelDefinitions]
O
Once [in coqrel.RelDefinitions]P
PolarityResolved [in coqrel.RelDefinitions]Q
QueryParams [in coqrel.Monotonicity]R
RAuto [in coqrel.RelDefinitions]RAutoSubgoals [in coqrel.RelDefinitions]
RCompose [in coqrel.RelClasses]
RDecompose [in coqrel.RelClasses]
RDestruct [in coqrel.RelDefinitions]
Related [in coqrel.RelDefinitions]
RElim [in coqrel.RelDefinitions]
RemoveAllParams [in coqrel.Monotonicity]
RemoveParams [in coqrel.Monotonicity]
RExists [in coqrel.RelDefinitions]
RImpl [in coqrel.Monotonicity]
RIntro [in coqrel.RelDefinitions]
RStep [in coqrel.RelDefinitions]
S
SubrelMonotonicity [in coqrel.Monotonicity]T
Transport [in coqrel.Transport]U
Unconvertible [in coqrel.RelDefinitions]UnfoldUncurry [in coqrel.RelOperators]
| 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 | (529 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 | (47 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 | (1 entry) |
| 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 | (15 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 | (131 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 | (45 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 | (37 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 | (24 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 | (140 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 | (6 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 | (1 entry) |
| 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 | (52 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 | (30 entries) |
This page has been generated by coqdoc