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 (205 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 (80 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 (7 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 (33 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 (1 entry)
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 (17 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 (45 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 (18 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 (4 entries)

Global Index

A

add [definition, in add]
App [constructor, in App]
approx [definition, in approx]
approx_nats_eq_helper [lemma, in approx_nats_eq_helper]
approx_nats_eq [lemma, in approx_nats_eq]
approx_nats_eq [lemma, in approx_nats_eq]


C

CoindSem [library]
CoindStart [library]
CoindTactic [library]
collatz [definition, in collatz]
Cons [constructor, in Cons]
Const [constructor, in Const]
cored [inductive, in cored]
cored_coind [definition, in cored_coind]
cored_coind [section, in cored_coind]
cored_coind.H [variable, in H]
cored_step [constructor, in cored_step]
cored_coind.R [variable, in R]
cored_refl [constructor, in cored_refl]
cored_red_or_redinf [lemma, in cored_red_or_redinf]
cored_irred_redinf [lemma, in cored_irred_redinf]
CpdtTactics [library]
cstep [definition, in cstep]
cycles [definition, in cycles]
cycles_collatz_100 [lemma, in cycles_collatz_100]
cycles_collatz_5 [lemma, in cycles_collatz_5]


D

done [definition, in done]
drop [definition, in drop]
dup [definition, in dup]


E

equiv [lemma, in equiv]
eval [inductive, in eval]
evalinf [inductive, in evalinf]
evalinf_gen_app_l [constructor, in evalinf_gen_app_l]
evalinf_gen_app_r [constructor, in evalinf_gen_app_r]
evalinf_fold [constructor, in evalinf_fold]
evalinf_tloops [lemma, in evalinf_tloops]
evalinf_coind [definition, in evalinf_coind]
evalinf_coind [section, in evalinf_coind]
evalinf_equiv_evalinf' [lemma, in evalinf_equiv_evalinf']
evalinf_app_f [constructor, in evalinf_app_f]
evalinf_tomega' [lemma, in evalinf_tomega']
evalinf_tomega [lemma, in evalinf_tomega]
evalinf_app_l [constructor, in evalinf_app_l]
evalinf_tomega1 [lemma, in evalinf_tomega1]
evalinf_app_r [constructor, in evalinf_app_r]
evalinf_coind_equiv.H [variable, in H]
evalinf_coind'.H [variable, in H]
evalinf_coind.H [variable, in H]
evalinf_coind_equiv.R [variable, in R]
evalinf_coind'.R [variable, in R]
evalinf_coind.R [variable, in R]
evalinf_gen [inductive, in evalinf_gen]
evalinf_coind_equiv.a [variable, in a]
evalinf_coind' [definition, in evalinf_coind']
evalinf_coind' [section, in evalinf_coind']
evalinf_red1 [lemma, in evalinf_red1]
evalinf_redinf [lemma, in evalinf_redinf]
evalinf_tgrows [lemma, in evalinf_tgrows]
evalinf_coind_equiv [lemma, in evalinf_coind_equiv]
evalinf_coind_equiv [section, in evalinf_coind_equiv]
evalinf_gen_app_f [constructor, in evalinf_gen_app_f]
evalinf' [inductive, in evalinf']
eval_fun [constructor, in eval_fun]
eval_redfin [lemma, in eval_redfin]
eval_app [constructor, in eval_app]
eval_deterministic [lemma, in eval_deterministic]
eval_const [constructor, in eval_const]
eval_val [lemma, in eval_val]
evenb [definition, in evenb]
exists_forall_impl [lemma, in exists_forall_impl]
exists_forall_impl [lemma, in exists_forall_impl]


F

falses_trues [definition, in falses_trues]
from_tgrows_sound [lemma, in from_tgrows_sound]
from_tgrows [inductive, in from_tgrows]
from_tgrows_redfin [lemma, in from_tgrows_redfin]
from_grows_complete [lemma, in from_grows_complete]
from_tgrows_red1 [lemma, in from_tgrows_red1]
ft_step [constructor, in ft_step]
ft_base [constructor, in ft_base]
Fun [constructor, in Fun]


G

goes_wrong [definition, in goes_wrong]
goes_wrong_twrong [lemma, in goes_wrong_twrong]


H

head [definition, in head]


I

infinite_progress_redinf [lemma, in infinite_progress_redinf]
interleave [definition, in interleave]
irred [definition, in irred]
iterate [definition, in iterate]


L

ladd [constructor, in ladd]
LCons [constructor, in LCons]
llist [inductive, in llist]
LNil [constructor, in LNil]
loops [inductive, in loops]
lt [inductive, in lt]


M

map [definition, in map]
map_iterate [lemma, in map_iterate]


N

Nat [inductive, in Nat]
nats [definition, in nats]
nats_eq_helper_auto [lemma, in nats_eq_helper_auto]
nats_eq_helper_with_step_by_step_R [lemma, in nats_eq_helper_with_step_by_step_R]
nats_eq_direct [lemma, in nats_eq_direct]
nats_eq_helper [lemma, in nats_eq_helper]
nats_eq [lemma, in nats_eq]
nats_eq [lemma, in nats_eq]
nats_eq [lemma, in nats_eq]
nats_eq_auto [lemma, in nats_eq_auto]
nats_from_n [definition, in nats_from_n]
nats' [definition, in nats']
NO [constructor, in NO]
non_standard [lemma, in non_standard]
not_eval_tomega [lemma, in not_eval_tomega]
not_evalinf_tstuck [lemma, in not_evalinf_tstuck]
not_evalinf_stuck [lemma, in not_evalinf_stuck]
not_eval_tstuck [lemma, in not_eval_tstuck]
NS [constructor, in NS]


O

ones [definition, in ones]
ones_eq [lemma, in ones_eq]
ones_eq [lemma, in ones_eq]
ones_eq'' [lemma, in ones_eq'']
ones_eq' [lemma, in ones_eq']
ones_eq' [lemma, in ones_eq']
ones' [definition, in ones']


R

redfin [inductive, in redfin]
redfin_eval [lemma, in redfin_eval]
redfin_step [constructor, in redfin_step]
redfin_refl [constructor, in redfin_refl]
redfin_cored [lemma, in redfin_cored]
redfin_or_redinf [lemma, in redfin_or_redinf]
redfin_one [lemma, in redfin_one]
redfin_app_l [lemma, in redfin_app_l]
redfin_trans [lemma, in redfin_trans]
redfin_app_r [lemma, in redfin_app_r]
redinf [inductive, in redinf]
redinf_tloops [lemma, in redinf_tloops]
redinf_app_l [lemma, in redinf_app_l]
redinf_app_r [lemma, in redinf_app_r]
redinf_tgrows_stronger [lemma, in redinf_tgrows_stronger]
redinf_tgrows_stronger [lemma, in redinf_tgrows_stronger]
redinf_tomega [lemma, in redinf_tomega]
redinf_tomega1_stronger [lemma, in redinf_tomega1_stronger]
redinf_coind.H [variable, in H]
redinf_coind.R [variable, in R]
redinf_tomega1 [lemma, in redinf_tomega1]
redinf_tomega1 [lemma, in redinf_tomega1]
redinf_intro [constructor, in redinf_intro]
redinf_tgrows [lemma, in redinf_tgrows]
redinf_cored [lemma, in redinf_cored]
redinf_evalinf [lemma, in redinf_evalinf]
redinf_coind [definition, in redinf_coind]
redinf_coind [section, in redinf_coind]
red1 [inductive, in red1]
red1_app_l [constructor, in red1_app_l]
red1_app_r [constructor, in red1_app_r]
red1_tgrows [lemma, in red1_tgrows]
red1_deterministic [lemma, in red1_deterministic]
red1_beta [constructor, in red1_beta]
red1_tomega [lemma, in red1_tomega]
red1_tomega1_tomega2 [lemma, in red1_tomega1_tomega2]
red1_App_dup [lemma, in red1_App_dup]
red1_eval [lemma, in red1_eval]
red1_tomega2_tomega1 [lemma, in red1_tomega2_tomega1]


S

same [definition, in same]
stream [inductive, in stream]
Stream_eq [constructor, in Stream_eq]
stream_eq_coind.H1 [variable, in H1]
stream_eq_coind.H2 [variable, in H2]
stream_eq_coind.A [variable, in A]
stream_eq_coind1.A [variable, in A]
stream_eq_coind1.H [variable, in H]
stream_eq_coind.R [variable, in R]
stream_eq_coind1.R [variable, in R]
stream_eq_coind1 [lemma, in stream_eq_coind1]
stream_eq_coind1 [section, in stream_eq_coind1]
stream_eta [lemma, in stream_eta]
stream_eq [inductive, in stream_eq]
stream_eq_coind [lemma, in stream_eq_coind]
stream_eq_coind [section, in stream_eq_coind]
stuck [definition, in stuck]
stuck_tstuck [lemma, in stuck_tstuck]
subst [definition, in subst]


T

tail [definition, in tail]
tdelta [definition, in tdelta]
tdelta' [definition, in tdelta']
term [inductive, in term]
tgrows [definition, in tgrows]
tloops [definition, in tloops]
tomega [definition, in tomega]
tomega1 [definition, in tomega1]
tomega2 [definition, in tomega2]
trues_falses [definition, in trues_falses]
tstuck [definition, in tstuck]
twrong [definition, in twrong]


V

val [inductive, in val]
value_irred [lemma, in value_irred]
val_eval [lemma, in val_eval]
val_const [constructor, in val_const]
val_fun [constructor, in val_fun]
Var [constructor, in Var]
var [definition, in var]
var_eq [lemma, in var_eq]
vf [definition, in vf]
vx [definition, in vx]
vy [definition, in vy]


Y

ydup [definition, in ydup]
ypart [definition, in ypart]


other

_ < _ [notation, in ::x_'<'_x]



Lemma Index

A

approx_nats_eq_helper [in approx_nats_eq_helper]
approx_nats_eq [in approx_nats_eq]
approx_nats_eq [in approx_nats_eq]


C

cored_red_or_redinf [in cored_red_or_redinf]
cored_irred_redinf [in cored_irred_redinf]
cycles_collatz_100 [in cycles_collatz_100]
cycles_collatz_5 [in cycles_collatz_5]


E

equiv [in equiv]
evalinf_tloops [in evalinf_tloops]
evalinf_equiv_evalinf' [in evalinf_equiv_evalinf']
evalinf_tomega' [in evalinf_tomega']
evalinf_tomega [in evalinf_tomega]
evalinf_tomega1 [in evalinf_tomega1]
evalinf_red1 [in evalinf_red1]
evalinf_redinf [in evalinf_redinf]
evalinf_tgrows [in evalinf_tgrows]
evalinf_coind_equiv [in evalinf_coind_equiv]
eval_redfin [in eval_redfin]
eval_deterministic [in eval_deterministic]
eval_val [in eval_val]
exists_forall_impl [in exists_forall_impl]
exists_forall_impl [in exists_forall_impl]


F

from_tgrows_sound [in from_tgrows_sound]
from_tgrows_redfin [in from_tgrows_redfin]
from_grows_complete [in from_grows_complete]
from_tgrows_red1 [in from_tgrows_red1]


G

goes_wrong_twrong [in goes_wrong_twrong]


I

infinite_progress_redinf [in infinite_progress_redinf]


M

map_iterate [in map_iterate]


N

nats_eq_helper_auto [in nats_eq_helper_auto]
nats_eq_helper_with_step_by_step_R [in nats_eq_helper_with_step_by_step_R]
nats_eq_direct [in nats_eq_direct]
nats_eq_helper [in nats_eq_helper]
nats_eq [in nats_eq]
nats_eq [in nats_eq]
nats_eq [in nats_eq]
nats_eq_auto [in nats_eq_auto]
non_standard [in non_standard]
not_eval_tomega [in not_eval_tomega]
not_evalinf_tstuck [in not_evalinf_tstuck]
not_evalinf_stuck [in not_evalinf_stuck]
not_eval_tstuck [in not_eval_tstuck]


O

ones_eq [in ones_eq]
ones_eq [in ones_eq]
ones_eq'' [in ones_eq'']
ones_eq' [in ones_eq']
ones_eq' [in ones_eq']


R

redfin_eval [in redfin_eval]
redfin_cored [in redfin_cored]
redfin_or_redinf [in redfin_or_redinf]
redfin_one [in redfin_one]
redfin_app_l [in redfin_app_l]
redfin_trans [in redfin_trans]
redfin_app_r [in redfin_app_r]
redinf_tloops [in redinf_tloops]
redinf_app_l [in redinf_app_l]
redinf_app_r [in redinf_app_r]
redinf_tgrows_stronger [in redinf_tgrows_stronger]
redinf_tgrows_stronger [in redinf_tgrows_stronger]
redinf_tomega [in redinf_tomega]
redinf_tomega1_stronger [in redinf_tomega1_stronger]
redinf_tomega1 [in redinf_tomega1]
redinf_tomega1 [in redinf_tomega1]
redinf_tgrows [in redinf_tgrows]
redinf_cored [in redinf_cored]
redinf_evalinf [in redinf_evalinf]
red1_tgrows [in red1_tgrows]
red1_deterministic [in red1_deterministic]
red1_tomega [in red1_tomega]
red1_tomega1_tomega2 [in red1_tomega1_tomega2]
red1_App_dup [in red1_App_dup]
red1_eval [in red1_eval]
red1_tomega2_tomega1 [in red1_tomega2_tomega1]


S

stream_eq_coind1 [in stream_eq_coind1]
stream_eta [in stream_eta]
stream_eq_coind [in stream_eq_coind]
stuck_tstuck [in stuck_tstuck]


V

value_irred [in value_irred]
val_eval [in val_eval]
var_eq [in var_eq]



Section Index

C

cored_coind [in cored_coind]


E

evalinf_coind [in evalinf_coind]
evalinf_coind' [in evalinf_coind']
evalinf_coind_equiv [in evalinf_coind_equiv]


R

redinf_coind [in redinf_coind]


S

stream_eq_coind1 [in stream_eq_coind1]
stream_eq_coind [in stream_eq_coind]



Constructor Index

A

App [in App]


C

Cons [in Cons]
Const [in Const]
cored_step [in cored_step]
cored_refl [in cored_refl]


E

evalinf_gen_app_l [in evalinf_gen_app_l]
evalinf_gen_app_r [in evalinf_gen_app_r]
evalinf_fold [in evalinf_fold]
evalinf_app_f [in evalinf_app_f]
evalinf_app_l [in evalinf_app_l]
evalinf_app_r [in evalinf_app_r]
evalinf_gen_app_f [in evalinf_gen_app_f]
eval_fun [in eval_fun]
eval_app [in eval_app]
eval_const [in eval_const]


F

ft_step [in ft_step]
ft_base [in ft_base]
Fun [in Fun]


L

ladd [in ladd]
LCons [in LCons]
LNil [in LNil]


N

NO [in NO]
NS [in NS]


R

redfin_step [in redfin_step]
redfin_refl [in redfin_refl]
redinf_intro [in redinf_intro]
red1_app_l [in red1_app_l]
red1_app_r [in red1_app_r]
red1_beta [in red1_beta]


S

Stream_eq [in Stream_eq]


V

val_const [in val_const]
val_fun [in val_fun]
Var [in Var]



Notation Index

other

_ < _ [in ::x_'<'_x]



Inductive Index

C

cored [in cored]


E

eval [in eval]
evalinf [in evalinf]
evalinf_gen [in evalinf_gen]
evalinf' [in evalinf']


F

from_tgrows [in from_tgrows]


L

llist [in llist]
loops [in loops]
lt [in lt]


N

Nat [in Nat]


R

redfin [in redfin]
redinf [in redinf]
red1 [in red1]


S

stream [in stream]
stream_eq [in stream_eq]


T

term [in term]


V

val [in val]



Definition Index

A

add [in add]
approx [in approx]


C

collatz [in collatz]
cored_coind [in cored_coind]
cstep [in cstep]
cycles [in cycles]


D

done [in done]
drop [in drop]
dup [in dup]


E

evalinf_coind [in evalinf_coind]
evalinf_coind' [in evalinf_coind']
evenb [in evenb]


F

falses_trues [in falses_trues]


G

goes_wrong [in goes_wrong]


H

head [in head]


I

interleave [in interleave]
irred [in irred]
iterate [in iterate]


M

map [in map]


N

nats [in nats]
nats_from_n [in nats_from_n]
nats' [in nats']


O

ones [in ones]
ones' [in ones']


R

redinf_coind [in redinf_coind]


S

same [in same]
stuck [in stuck]
subst [in subst]


T

tail [in tail]
tdelta [in tdelta]
tdelta' [in tdelta']
tgrows [in tgrows]
tloops [in tloops]
tomega [in tomega]
tomega1 [in tomega1]
tomega2 [in tomega2]
trues_falses [in trues_falses]
tstuck [in tstuck]
twrong [in twrong]


V

var [in var]
vf [in vf]
vx [in vx]
vy [in vy]


Y

ydup [in ydup]
ypart [in ypart]



Variable Index

C

cored_coind.H [in H]
cored_coind.R [in R]


E

evalinf_coind_equiv.H [in H]
evalinf_coind'.H [in H]
evalinf_coind.H [in H]
evalinf_coind_equiv.R [in R]
evalinf_coind'.R [in R]
evalinf_coind.R [in R]
evalinf_coind_equiv.a [in a]


R

redinf_coind.H [in H]
redinf_coind.R [in R]


S

stream_eq_coind.H1 [in H1]
stream_eq_coind.H2 [in H2]
stream_eq_coind.A [in A]
stream_eq_coind1.A [in A]
stream_eq_coind1.H [in H]
stream_eq_coind.R [in R]
stream_eq_coind1.R [in R]



Library Index

C

CoindSem
CoindStart
CoindTactic
CpdtTactics



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 (205 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 (80 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 (7 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 (33 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 (1 entry)
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 (17 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 (45 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 (18 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 (4 entries)

This page has been generated by coqdoc