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 _ (43 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 _ (17 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 _ (16 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 _ (5 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 _ (4 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 _ (1 entry)

Global Index

A

app [constructor, in combinators]

C

combinators [module]
computes [definition, in combinators]
confluence [definition, in combinators]

D

decompose [lemma, in combinators]
diamond [definition, in combinators]
diamond_par_step [lemma, in combinators]
diamond_trcl [lemma, in combinators]

K

K [constructor, in combinators]
km [lemma, in combinators]

O

onestep_sub_par [lemma, in combinators]
one_step [inductive, in combinators]

P

parapp [constructor, in combinators]
park [constructor, in combinators]
pars [constructor, in combinators]
parstar_is_reduce [lemma, in combinators]
par_refl [constructor, in combinators]
par_step [inductive, in combinators]
par_sub_reduce [lemma, in combinators]
pComputes [lemma, in combinators]
pConfluence [lemma, in combinators]
pStuck [lemma, in combinators]

R

rclosure [inductive, in combinators]
rcl_refl [constructor, in combinators]
rcl_step [constructor, in combinators]
redk [constructor, in combinators]
redl [constructor, in combinators]
redr [constructor, in combinators]
reds [constructor, in combinators]
reduce [definition, in combinators]
reduce_left [lemma, in combinators]
reduce_right [lemma, in combinators]

S

S [constructor, in combinators]
sm [lemma, in combinators]
smn [lemma, in combinators]
substDiamond [lemma, in combinators]

T

Term [inductive, in combinators]
trclosure [inductive, in combinators]
trcl_monotonic [lemma, in combinators]
trcl_refl [constructor, in combinators]
trcl_step [constructor, in combinators]
trcl_trans [constructor, in combinators]
tr_rcl_is_trcl [lemma, in combinators]


Lemma Index

D

decompose [in combinators]
diamond_par_step [in combinators]
diamond_trcl [in combinators]

K

km [in combinators]

O

onestep_sub_par [in combinators]

P

parstar_is_reduce [in combinators]
par_sub_reduce [in combinators]
pComputes [in combinators]
pConfluence [in combinators]
pStuck [in combinators]

R

reduce_left [in combinators]
reduce_right [in combinators]

S

sm [in combinators]
smn [in combinators]
substDiamond [in combinators]

T

trcl_monotonic [in combinators]
tr_rcl_is_trcl [in combinators]


Constructor Index

A

app [in combinators]

K

K [in combinators]

P

parapp [in combinators]
park [in combinators]
pars [in combinators]
par_refl [in combinators]

R

rcl_refl [in combinators]
rcl_step [in combinators]
redk [in combinators]
redl [in combinators]
redr [in combinators]
reds [in combinators]

S

S [in combinators]

T

trcl_refl [in combinators]
trcl_step [in combinators]
trcl_trans [in combinators]


Inductive Index

O

one_step [in combinators]

P

par_step [in combinators]

R

rclosure [in combinators]

T

Term [in combinators]
trclosure [in combinators]


Definition Index

C

computes [in combinators]
confluence [in combinators]

D

diamond [in combinators]

R

reduce [in combinators]


Module Index

C

combinators


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 _ (43 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 _ (17 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 _ (16 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 _ (5 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 _ (4 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 _ (1 entry)

This page has been generated by coqdoc