Global Index

A

B

J

K

O

P

Q

R

S

V

W

X

Y

Z

_

(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

_

(9 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(2 entries)

Constructor Index

A

B

C

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Axiom Index

A

B

D

E

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(22 entries)

Inductive Index

A

B

C

D

F

G

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Projection Index

A

B

C

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Instance Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

D

E

G

H

J

K

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(19 entries)

Record Index

A

B

D

E

F

G

I

J

K

L

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

J

K

O

P

Q

R

S

V

W

X

Y

Z

_

(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

_

(9 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(2 entries)

Constructor Index

A

B

C

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Axiom Index

A

B

D

E

H

I

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(22 entries)

Inductive Index

A

B

C

D

F

G

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Projection Index

A

B

C

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Instance Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(12 entries)

Definition Index

A

B

D

E

G

H

J

K

O

P

Q

R

S

T

V

W

X

Y

Z

_

other

(19 entries)

Record Index

A

B

D

E

F

G

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(7 entries)

This page has been generated by coqdoc