| 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 | (213 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 | (7 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 | (10 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 | (6 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 | (84 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 | (41 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 | (14 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 | (14 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 | (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 | (2 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 | (31 entries) |
Global Index
A
App [constructor, in L]App [constructor, in UntypedLambda]
App [constructor, in SK]
ARS [library]
C
church_rosser [lemma, in Confluence]cofinal [definition, in ARS]
CoFinal [section, in ARS]
cofinal_normalizing [lemma, in ARS]
CoFinal.R [variable, in ARS]
CoFinal.rho [variable, in ARS]
CoFinal.tri [variable, in ARS]
CoFinal.X [variable, in ARS]
com [definition, in ARS]
Commutation [section, in ARS]
Commutation.X [variable, in ARS]
com_lift [lemma, in ARS]
com_strip [lemma, in ARS]
Confluence [library]
confluent [definition, in ARS]
confluent_stable [lemma, in ARS]
confluent_semi [lemma, in ARS]
conv [abbreviation, in Reduction]
conv [inductive, in ARS]
convmn [inductive, in ARS]
convmnR [constructor, in ARS]
convmnSR [constructor, in ARS]
convmnSRi [constructor, in ARS]
convR [constructor, in ARS]
convRS [lemma, in ARS]
convRSi [lemma, in ARS]
convSR [constructor, in ARS]
convSRi [constructor, in ARS]
conv_subst_proper [instance, in Reduction]
conv_compat [lemma, in Reduction]
conv_lam [instance, in Reduction]
conv_app [instance, in Reduction]
conv_substitutivity [lemma, in Reduction]
conv_closure [lemma, in ARS]
conv_hom [lemma, in ARS]
conv_img [lemma, in ARS]
conv_sym [lemma, in ARS]
conv_trans [lemma, in ARS]
conv1 [lemma, in ARS]
conv1i [lemma, in ARS]
CR [definition, in ARS]
cr_method [lemma, in ARS]
cr_conv_normal [lemma, in ARS]
cr_star_normal [lemma, in ARS]
cr_confluent [lemma, in ARS]
D
Definitions [section, in ARS]Definitions.R [variable, in ARS]
Definitions.X [variable, in ARS]
diamond [definition, in ARS]
diamond_confluent [lemma, in ARS]
E
eqn [definition, in L]equivalence_conv [lemma, in ARS]
equiv_conv [instance, in Reduction]
eq_star [lemma, in ARS]
F
funcomp [definition, in UntypedLambda]I
italian_uniform_confluence [lemma, in ARS]iter [definition, in ARS]
J
joinable [definition, in ARS]join_conv [lemma, in ARS]
K
K [constructor, in SK]L
L [library]Lam [constructor, in L]
Lam [constructor, in UntypedLambda]
L_confluent [lemma, in L]
L_uniform_confluent [lemma, in L]
N
nf [definition, in ARS]normal [definition, in ARS]
normalizing [definition, in ARS]
normal_star [lemma, in ARS]
P
Pred [definition, in ARS]preorder_red [instance, in Reduction]
preorder_star [lemma, in ARS]
pstep [inductive, in Confluence]
pstep [inductive, in SK]
pstepA [constructor, in SK]
pstepK [constructor, in SK]
pstepR [constructor, in SK]
psteps [definition, in Confluence]
pstepS [constructor, in SK]
psteps_up [lemma, in Confluence]
pstep_subst1 [lemma, in Confluence]
pstep_subst [lemma, in Confluence]
pstep_ren [lemma, in Confluence]
pstep_red [lemma, in Confluence]
pstep_refl [lemma, in Confluence]
pstep_var [constructor, in Confluence]
pstep_lam [constructor, in Confluence]
pstep_app [constructor, in Confluence]
pstep_beta [constructor, in Confluence]
R
red [abbreviation, in Reduction]reducible [definition, in ARS]
Reduction [library]
red_subst_proper [instance, in Reduction]
red_compat [lemma, in Reduction]
red_lam [instance, in Reduction]
red_app [instance, in Reduction]
red_substitutivity [lemma, in Reduction]
Rel [definition, in ARS]
ren [definition, in UntypedLambda]
rename [definition, in UntypedLambda]
rename_subst [lemma, in UntypedLambda]
ren_subst [lemma, in UntypedLambda]
rho [definition, in Confluence]
rho [definition, in SK]
rho_triangle [lemma, in Confluence]
S
S [constructor, in SK]scomp [definition, in UntypedLambda]
scomp_proper [instance, in UntypedLambda]
scons [definition, in UntypedLambda]
scons_scomp [lemma, in UntypedLambda]
scons_proper [instance, in UntypedLambda]
scons_comp [lemma, in UntypedLambda]
semi_cr [lemma, in ARS]
semi_confluent [definition, in ARS]
SK [library]
sn [inductive, in ARS]
SNI [constructor, in ARS]
sn_preimage [lemma, in ARS]
star [inductive, in ARS]
starn [inductive, in ARS]
starnRS [constructor, in ARS]
starnxx [constructor, in ARS]
starn_star [lemma, in ARS]
starn_trans [lemma, in ARS]
starn_uj [lemma, in ARS]
starR [constructor, in ARS]
starRS [lemma, in ARS]
starSR [constructor, in ARS]
star_interpolation [lemma, in ARS]
star_monotone [lemma, in ARS]
star_closure [lemma, in ARS]
star_proper2 [lemma, in ARS]
star_proper [lemma, in ARS]
star_hom [lemma, in ARS]
star_img [lemma, in ARS]
star_conv [lemma, in ARS]
star_trans [lemma, in ARS]
star1 [lemma, in ARS]
step [inductive, in Reduction]
step [inductive, in L]
step_ebeta [lemma, in Reduction]
step_lam [constructor, in Reduction]
step_appr [constructor, in Reduction]
step_appl [constructor, in Reduction]
step_beta [constructor, in Reduction]
step_pstep [lemma, in Confluence]
step_appr [constructor, in L]
step_appl [constructor, in L]
step_beta [constructor, in L]
subrel_star_conv [instance, in ARS]
subrel_conv [instance, in ARS]
subrel_star [instance, in ARS]
subst [definition, in UntypedLambda]
substitutivity [lemma, in Reduction]
substk [definition, in L]
subst_beta [lemma, in UntypedLambda]
subst_extend [lemma, in UntypedLambda]
subst_comp [lemma, in UntypedLambda]
subst_ren [lemma, in UntypedLambda]
subst_id [lemma, in UntypedLambda]
subst_proper [instance, in UntypedLambda]
T
term [inductive, in L]term [inductive, in UntypedLambda]
term [inductive, in SK]
Termination [section, in ARS]
Termination.cr [variable, in ARS]
Termination.R [variable, in ARS]
Termination.X [variable, in ARS]
triangle [definition, in ARS]
triangle_cofinal [lemma, in ARS]
triangle_monotone [lemma, in ARS]
triangle_diamond [lemma, in ARS]
U
uc [definition, in L]uc_confluent [lemma, in ARS]
uf_ucr [lemma, in ARS]
uf_uj [lemma, in ARS]
uj [inductive, in ARS]
uj_joinable [lemma, in ARS]
uj_UCP [lemma, in ARS]
uj_normal [lemma, in ARS]
uj_normal_le [lemma, in ARS]
uj_extendn [lemma, in ARS]
uj_extend [lemma, in ARS]
uj_weaken [constructor, in ARS]
uj_stepr [constructor, in ARS]
uj_stepl [constructor, in ARS]
uj_refl [constructor, in ARS]
UniformConfluenceI [constructor, in ARS]
UniformConfluenceP [inductive, in ARS]
uniform_normalization [lemma, in ARS]
uniform_confluent [definition, in ARS]
UntypedLambda [library]
up [definition, in UntypedLambda]
upE [lemma, in UntypedLambda]
upr [definition, in UntypedLambda]
upr_up [lemma, in UntypedLambda]
up_comp [lemma, in UntypedLambda]
up_id [lemma, in UntypedLambda]
V
Var [constructor, in L]Var [constructor, in UntypedLambda]
Var [constructor, in SK]
W
wn [definition, in ARS]other
_ <<= _ (prop_scope) [notation, in ARS]_ .[ _ /] (subst_scope) [notation, in UntypedLambda]
_ .[ _ ] (subst_scope) [notation, in UntypedLambda]
_ .: _ (subst_scope) [notation, in UntypedLambda]
_ >>> _ (subst_scope) [notation, in UntypedLambda]
_ >> _ [notation, in UntypedLambda]
_ >> _ [notation, in SK]
Notation Index
other
_ <<= _ (prop_scope) [in ARS]_ .[ _ /] (subst_scope) [in UntypedLambda]
_ .[ _ ] (subst_scope) [in UntypedLambda]
_ .: _ (subst_scope) [in UntypedLambda]
_ >>> _ (subst_scope) [in UntypedLambda]
_ >> _ [in UntypedLambda]
_ >> _ [in SK]
Variable Index
C
CoFinal.R [in ARS]CoFinal.rho [in ARS]
CoFinal.tri [in ARS]
CoFinal.X [in ARS]
Commutation.X [in ARS]
D
Definitions.R [in ARS]Definitions.X [in ARS]
T
Termination.cr [in ARS]Termination.R [in ARS]
Termination.X [in ARS]
Library Index
A
ARSC
ConfluenceL
LR
ReductionS
SKU
UntypedLambdaLemma Index
C
church_rosser [in Confluence]cofinal_normalizing [in ARS]
com_lift [in ARS]
com_strip [in ARS]
confluent_stable [in ARS]
confluent_semi [in ARS]
convRS [in ARS]
convRSi [in ARS]
conv_compat [in Reduction]
conv_substitutivity [in Reduction]
conv_closure [in ARS]
conv_hom [in ARS]
conv_img [in ARS]
conv_sym [in ARS]
conv_trans [in ARS]
conv1 [in ARS]
conv1i [in ARS]
cr_method [in ARS]
cr_conv_normal [in ARS]
cr_star_normal [in ARS]
cr_confluent [in ARS]
D
diamond_confluent [in ARS]E
equivalence_conv [in ARS]eq_star [in ARS]
I
italian_uniform_confluence [in ARS]J
join_conv [in ARS]L
L_confluent [in L]L_uniform_confluent [in L]
N
normal_star [in ARS]P
preorder_star [in ARS]psteps_up [in Confluence]
pstep_subst1 [in Confluence]
pstep_subst [in Confluence]
pstep_ren [in Confluence]
pstep_red [in Confluence]
pstep_refl [in Confluence]
R
red_compat [in Reduction]red_substitutivity [in Reduction]
rename_subst [in UntypedLambda]
ren_subst [in UntypedLambda]
rho_triangle [in Confluence]
S
scons_scomp [in UntypedLambda]scons_comp [in UntypedLambda]
semi_cr [in ARS]
sn_preimage [in ARS]
starn_star [in ARS]
starn_trans [in ARS]
starn_uj [in ARS]
starRS [in ARS]
star_interpolation [in ARS]
star_monotone [in ARS]
star_closure [in ARS]
star_proper2 [in ARS]
star_proper [in ARS]
star_hom [in ARS]
star_img [in ARS]
star_conv [in ARS]
star_trans [in ARS]
star1 [in ARS]
step_ebeta [in Reduction]
step_pstep [in Confluence]
substitutivity [in Reduction]
subst_beta [in UntypedLambda]
subst_extend [in UntypedLambda]
subst_comp [in UntypedLambda]
subst_ren [in UntypedLambda]
subst_id [in UntypedLambda]
T
triangle_cofinal [in ARS]triangle_monotone [in ARS]
triangle_diamond [in ARS]
U
uc_confluent [in ARS]uf_ucr [in ARS]
uf_uj [in ARS]
uj_joinable [in ARS]
uj_UCP [in ARS]
uj_normal [in ARS]
uj_normal_le [in ARS]
uj_extendn [in ARS]
uj_extend [in ARS]
uniform_normalization [in ARS]
upE [in UntypedLambda]
upr_up [in UntypedLambda]
up_comp [in UntypedLambda]
up_id [in UntypedLambda]
Constructor Index
A
App [in L]App [in UntypedLambda]
App [in SK]
C
convmnR [in ARS]convmnSR [in ARS]
convmnSRi [in ARS]
convR [in ARS]
convSR [in ARS]
convSRi [in ARS]
K
K [in SK]L
Lam [in L]Lam [in UntypedLambda]
P
pstepA [in SK]pstepK [in SK]
pstepR [in SK]
pstepS [in SK]
pstep_var [in Confluence]
pstep_lam [in Confluence]
pstep_app [in Confluence]
pstep_beta [in Confluence]
S
S [in SK]SNI [in ARS]
starnRS [in ARS]
starnxx [in ARS]
starR [in ARS]
starSR [in ARS]
step_lam [in Reduction]
step_appr [in Reduction]
step_appl [in Reduction]
step_beta [in Reduction]
step_appr [in L]
step_appl [in L]
step_beta [in L]
U
uj_weaken [in ARS]uj_stepr [in ARS]
uj_stepl [in ARS]
uj_refl [in ARS]
UniformConfluenceI [in ARS]
V
Var [in L]Var [in UntypedLambda]
Var [in SK]
Inductive Index
C
conv [in ARS]convmn [in ARS]
P
pstep [in Confluence]pstep [in SK]
S
sn [in ARS]star [in ARS]
starn [in ARS]
step [in Reduction]
step [in L]
T
term [in L]term [in UntypedLambda]
term [in SK]
U
uj [in ARS]UniformConfluenceP [in ARS]
Instance Index
C
conv_subst_proper [in Reduction]conv_lam [in Reduction]
conv_app [in Reduction]
E
equiv_conv [in Reduction]P
preorder_red [in Reduction]R
red_subst_proper [in Reduction]red_lam [in Reduction]
red_app [in Reduction]
S
scomp_proper [in UntypedLambda]scons_proper [in UntypedLambda]
subrel_star_conv [in ARS]
subrel_conv [in ARS]
subrel_star [in ARS]
subst_proper [in UntypedLambda]
Section Index
C
CoFinal [in ARS]Commutation [in ARS]
D
Definitions [in ARS]T
Termination [in ARS]Abbreviation Index
C
conv [in Reduction]R
red [in Reduction]Definition Index
C
cofinal [in ARS]com [in ARS]
confluent [in ARS]
CR [in ARS]
D
diamond [in ARS]E
eqn [in L]F
funcomp [in UntypedLambda]I
iter [in ARS]J
joinable [in ARS]N
nf [in ARS]normal [in ARS]
normalizing [in ARS]
P
Pred [in ARS]psteps [in Confluence]
R
reducible [in ARS]Rel [in ARS]
ren [in UntypedLambda]
rename [in UntypedLambda]
rho [in Confluence]
rho [in SK]
S
scomp [in UntypedLambda]scons [in UntypedLambda]
semi_confluent [in ARS]
subst [in UntypedLambda]
substk [in L]
T
triangle [in ARS]U
uc [in L]uniform_confluent [in ARS]
up [in UntypedLambda]
upr [in UntypedLambda]
W
wn [in ARS]| 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 | (213 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 | (7 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 | (10 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 | (6 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 | (84 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 | (41 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 | (14 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 | (14 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 | (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 | (2 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 | (31 entries) |
This page has been generated by coqdoc