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 (84 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 (9 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 (2 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 (5 entries)
Axiom 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 (22 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 (5 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 (3 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 (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 (19 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

C

ComposeTo [record, in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo [record, in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo11 [instance, in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo11 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo12 [instance, in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo12 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo21 [instance, in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo21 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo22 [instance, in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo22 [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
Compose11 [axiom, in CoqWorkshop.tactics_in_terms_presentation]
Compose11 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
Compose12 [axiom, in CoqWorkshop.tactics_in_terms_presentation]
Compose12 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
Compose21 [axiom, in CoqWorkshop.tactics_in_terms_presentation]
Compose21 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
Compose22 [axiom, in CoqWorkshop.tactics_in_terms_presentation]
Compose22 [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
composition [definition, in CoqWorkshop.tactics_in_terms_presentation]
composition [definition, in CoqWorkshop.tactics_in_terms_paper_examples]


D

do_make_apply_under_binders_in_helper_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]
do_make_apply_under_binders_in_helper_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]
do_make_apply_under_binders_in_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]
do_make_apply_under_binders_in_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]


E

eq [inductive, in CoqWorkshop.tactics_in_terms_presentation]
eq [inductive, in CoqWorkshop.tactics_in_terms_paper_examples]
eq_refl [constructor, in CoqWorkshop.tactics_in_terms_presentation]
eq_refl [constructor, in CoqWorkshop.tactics_in_terms_paper_examples]


F

F [axiom, in CoqWorkshop.tactics_in_terms_presentation]
F [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
funext_downward_closed [definition, in CoqWorkshop.tactics_in_terms_presentation]
funext_downward_closed [definition, in CoqWorkshop.tactics_in_terms_paper_examples]


G

G [axiom, in CoqWorkshop.tactics_in_terms_presentation]
G [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]


H

hnf_under_binders_helper [record, in CoqWorkshop.tactics_in_terms_presentation]
hnf_under_binders_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]


I

I_am_exactly_two [definition, in CoqWorkshop.tactics_in_terms_presentation]
I_am_exactly_one [definition, in CoqWorkshop.tactics_in_terms_presentation]
I_am_one [definition, in CoqWorkshop.tactics_in_terms_presentation]
I_am_exactly_one [definition, in CoqWorkshop.tactics_in_terms_paper_examples]
I_am_one [definition, in CoqWorkshop.tactics_in_terms_paper_examples]


L

Lift [definition, in CoqWorkshop.tactics_in_terms_presentation]
Lift [definition, in CoqWorkshop.tactics_in_terms_paper_examples]
lift_eq [definition, in CoqWorkshop.tactics_in_terms_presentation]
lift_eq [definition, in CoqWorkshop.tactics_in_terms_paper_examples]


M

make_apply_under_binders_in_helper_helper [record, in CoqWorkshop.tactics_in_terms_presentation]
make_apply_under_binders_in_helper_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]
make_apply_under_binders_in_helper [record, in CoqWorkshop.tactics_in_terms_presentation]
make_apply_under_binders_in_helper [inductive, in CoqWorkshop.tactics_in_terms_presentation]
make_hnf_under_binders_helper [projection, in CoqWorkshop.tactics_in_terms_presentation]
make_hnf_under_binders_helper [constructor, in CoqWorkshop.tactics_in_terms_presentation]
MyF [instance, in CoqWorkshop.tactics_in_terms_presentation]
MyF [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
MyG [instance, in CoqWorkshop.tactics_in_terms_presentation]
MyG [instance, in CoqWorkshop.tactics_in_terms_paper_examples]
mynotation [definition, in CoqWorkshop.tactics_in_terms_presentation]
MyNotation [record, in CoqWorkshop.tactics_in_terms_presentation]
mynotation [definition, in CoqWorkshop.tactics_in_terms_paper_examples]
MyNotation [record, in CoqWorkshop.tactics_in_terms_paper_examples]


N

NaiveFunext [definition, in CoqWorkshop.tactics_in_terms_presentation]
NaiveFunext [definition, in CoqWorkshop.tactics_in_terms_paper_examples]


T

tactics_in_terms_paper_examples [library]
tactics_in_terms_presentation [library]
t₁ [axiom, in CoqWorkshop.tactics_in_terms_presentation]
T₁ [axiom, in CoqWorkshop.tactics_in_terms_presentation]
t₁ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
T₁ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
t₂ [axiom, in CoqWorkshop.tactics_in_terms_presentation]
T₂ [axiom, in CoqWorkshop.tactics_in_terms_presentation]
t₂ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
T₂ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]
T₃ [axiom, in CoqWorkshop.tactics_in_terms_presentation]
T₃ [axiom, in CoqWorkshop.tactics_in_terms_paper_examples]


U

unfold_me_too [definition, in CoqWorkshop.tactics_in_terms_presentation]
unfold_me [definition, in CoqWorkshop.tactics_in_terms_presentation]


other

_ = _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_presentation]
_ = _ :> _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_presentation]
_ = _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_paper_examples]
_ = _ :> _ (type_scope) [notation, in CoqWorkshop.tactics_in_terms_paper_examples]
_ ∘ _ [notation, in CoqWorkshop.tactics_in_terms_presentation]
_ ∘ _ [notation, in CoqWorkshop.tactics_in_terms_paper_examples]
%% _ [notation, in CoqWorkshop.tactics_in_terms_presentation]
% _ [notation, in CoqWorkshop.tactics_in_terms_presentation]
% _ [notation, in CoqWorkshop.tactics_in_terms_paper_examples]



Notation Index

other

_ = _ (type_scope) [in CoqWorkshop.tactics_in_terms_presentation]
_ = _ :> _ (type_scope) [in CoqWorkshop.tactics_in_terms_presentation]
_ = _ (type_scope) [in CoqWorkshop.tactics_in_terms_paper_examples]
_ = _ :> _ (type_scope) [in CoqWorkshop.tactics_in_terms_paper_examples]
_ ∘ _ [in CoqWorkshop.tactics_in_terms_presentation]
_ ∘ _ [in CoqWorkshop.tactics_in_terms_paper_examples]
%% _ [in CoqWorkshop.tactics_in_terms_presentation]
% _ [in CoqWorkshop.tactics_in_terms_presentation]
% _ [in CoqWorkshop.tactics_in_terms_paper_examples]



Library Index

T

tactics_in_terms_paper_examples
tactics_in_terms_presentation



Constructor Index

D

do_make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]
do_make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]


E

eq_refl [in CoqWorkshop.tactics_in_terms_presentation]
eq_refl [in CoqWorkshop.tactics_in_terms_paper_examples]


M

make_hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]



Axiom Index

C

Compose11 [in CoqWorkshop.tactics_in_terms_presentation]
Compose11 [in CoqWorkshop.tactics_in_terms_paper_examples]
Compose12 [in CoqWorkshop.tactics_in_terms_presentation]
Compose12 [in CoqWorkshop.tactics_in_terms_paper_examples]
Compose21 [in CoqWorkshop.tactics_in_terms_presentation]
Compose21 [in CoqWorkshop.tactics_in_terms_paper_examples]
Compose22 [in CoqWorkshop.tactics_in_terms_presentation]
Compose22 [in CoqWorkshop.tactics_in_terms_paper_examples]


F

F [in CoqWorkshop.tactics_in_terms_presentation]
F [in CoqWorkshop.tactics_in_terms_paper_examples]


G

G [in CoqWorkshop.tactics_in_terms_presentation]
G [in CoqWorkshop.tactics_in_terms_paper_examples]


T

t₁ [in CoqWorkshop.tactics_in_terms_presentation]
T₁ [in CoqWorkshop.tactics_in_terms_presentation]
t₁ [in CoqWorkshop.tactics_in_terms_paper_examples]
T₁ [in CoqWorkshop.tactics_in_terms_paper_examples]
t₂ [in CoqWorkshop.tactics_in_terms_presentation]
T₂ [in CoqWorkshop.tactics_in_terms_presentation]
t₂ [in CoqWorkshop.tactics_in_terms_paper_examples]
T₂ [in CoqWorkshop.tactics_in_terms_paper_examples]
T₃ [in CoqWorkshop.tactics_in_terms_presentation]
T₃ [in CoqWorkshop.tactics_in_terms_paper_examples]



Inductive Index

E

eq [in CoqWorkshop.tactics_in_terms_presentation]
eq [in CoqWorkshop.tactics_in_terms_paper_examples]


H

hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]


M

make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]
make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]



Projection Index

D

do_make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]
do_make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]


M

make_hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]



Instance Index

C

ComposeTo11 [in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo11 [in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo12 [in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo12 [in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo21 [in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo21 [in CoqWorkshop.tactics_in_terms_paper_examples]
ComposeTo22 [in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo22 [in CoqWorkshop.tactics_in_terms_paper_examples]


M

MyF [in CoqWorkshop.tactics_in_terms_presentation]
MyF [in CoqWorkshop.tactics_in_terms_paper_examples]
MyG [in CoqWorkshop.tactics_in_terms_presentation]
MyG [in CoqWorkshop.tactics_in_terms_paper_examples]



Definition Index

C

composition [in CoqWorkshop.tactics_in_terms_presentation]
composition [in CoqWorkshop.tactics_in_terms_paper_examples]


F

funext_downward_closed [in CoqWorkshop.tactics_in_terms_presentation]
funext_downward_closed [in CoqWorkshop.tactics_in_terms_paper_examples]


I

I_am_exactly_two [in CoqWorkshop.tactics_in_terms_presentation]
I_am_exactly_one [in CoqWorkshop.tactics_in_terms_presentation]
I_am_one [in CoqWorkshop.tactics_in_terms_presentation]
I_am_exactly_one [in CoqWorkshop.tactics_in_terms_paper_examples]
I_am_one [in CoqWorkshop.tactics_in_terms_paper_examples]


L

Lift [in CoqWorkshop.tactics_in_terms_presentation]
Lift [in CoqWorkshop.tactics_in_terms_paper_examples]
lift_eq [in CoqWorkshop.tactics_in_terms_presentation]
lift_eq [in CoqWorkshop.tactics_in_terms_paper_examples]


M

mynotation [in CoqWorkshop.tactics_in_terms_presentation]
mynotation [in CoqWorkshop.tactics_in_terms_paper_examples]


N

NaiveFunext [in CoqWorkshop.tactics_in_terms_presentation]
NaiveFunext [in CoqWorkshop.tactics_in_terms_paper_examples]


U

unfold_me_too [in CoqWorkshop.tactics_in_terms_presentation]
unfold_me [in CoqWorkshop.tactics_in_terms_presentation]



Record Index

C

ComposeTo [in CoqWorkshop.tactics_in_terms_presentation]
ComposeTo [in CoqWorkshop.tactics_in_terms_paper_examples]


H

hnf_under_binders_helper [in CoqWorkshop.tactics_in_terms_presentation]


M

make_apply_under_binders_in_helper_helper [in CoqWorkshop.tactics_in_terms_presentation]
make_apply_under_binders_in_helper [in CoqWorkshop.tactics_in_terms_presentation]
MyNotation [in CoqWorkshop.tactics_in_terms_presentation]
MyNotation [in CoqWorkshop.tactics_in_terms_paper_examples]



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 (84 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 (9 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 (2 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 (5 entries)
Axiom 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 (22 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 (5 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 (3 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 (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 (19 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)

This page has been generated by coqdoc