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

(42 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

_

other

(4 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

(3 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

(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

(3 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

(6 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

(1 entry)

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

(18 entries)

Global Index

D

double_num [definition, in Ltac2Tutorial.tutorial0]

E

ex1 [lemma, in Ltac2Tutorial.tutorial0]
ex2 [lemma, in Ltac2Tutorial.tutorial0]

F

four [definition, in Ltac2Tutorial.tutorial0]

I

id_prop' [lemma, in Ltac2Tutorial.tutorial0]
id_prop [lemma, in Ltac2Tutorial.tutorial0]

M

Monoid [module, in Ltac2Tutorial.tutorial1]
MonoidSimp [module, in Ltac2Tutorial.tutorial1]
MonoidSimpTest [module, in Ltac2Tutorial.tutorial1]
MonoidSimpTest.AS [module, in Ltac2Tutorial.tutorial1]
MonoidSimpTest.test0 [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.denote_append [lemma, in Ltac2Tutorial.tutorial1]
MonoidSimp.denote_mexps [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.denote_mexp [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.flatten [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.flatten_correct [lemma, in Ltac2Tutorial.tutorial1]
MonoidSimp.Id [constructor, in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp [inductive, in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_sind [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_rec [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_ind [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_rect [definition, in Ltac2Tutorial.tutorial1]
MonoidSimp.monoid_reflect [lemma, in Ltac2Tutorial.tutorial1]
MonoidSimp.Op [constructor, in Ltac2Tutorial.tutorial1]
MonoidSimp.Var [constructor, in Ltac2Tutorial.tutorial1]
Monoid.M [axiom, in Ltac2Tutorial.tutorial1]
Monoid.madd [axiom, in Ltac2Tutorial.tutorial1]
Monoid.madd_idr [axiom, in Ltac2Tutorial.tutorial1]
Monoid.madd_idl [axiom, in Ltac2Tutorial.tutorial1]
Monoid.madd_assoc [axiom, in Ltac2Tutorial.tutorial1]
Monoid.mzero [axiom, in Ltac2Tutorial.tutorial1]

T

tutorial0 [library]
tutorial1 [library]
tutorial2 [library]

U

Unnamed_thm5 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm4 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm3 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm2 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm1 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm0 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm0 [definition, in Ltac2Tutorial.tutorial0]
Unnamed_thm [definition, in Ltac2Tutorial.tutorial0]

Module Index

M

Monoid [in Ltac2Tutorial.tutorial1]
MonoidSimp [in Ltac2Tutorial.tutorial1]
MonoidSimpTest [in Ltac2Tutorial.tutorial1]
MonoidSimpTest.AS [in Ltac2Tutorial.tutorial1]

Library Index

T

tutorial0
tutorial1
tutorial2

Lemma Index

E

ex1 [in Ltac2Tutorial.tutorial0]
ex2 [in Ltac2Tutorial.tutorial0]

I

id_prop' [in Ltac2Tutorial.tutorial0]
id_prop [in Ltac2Tutorial.tutorial0]

M

MonoidSimp.denote_append [in Ltac2Tutorial.tutorial1]
MonoidSimp.flatten_correct [in Ltac2Tutorial.tutorial1]
MonoidSimp.monoid_reflect [in Ltac2Tutorial.tutorial1]

Constructor Index

M

MonoidSimp.Id [in Ltac2Tutorial.tutorial1]
MonoidSimp.Op [in Ltac2Tutorial.tutorial1]
MonoidSimp.Var [in Ltac2Tutorial.tutorial1]

Axiom Index

M

Monoid.M [in Ltac2Tutorial.tutorial1]
Monoid.madd [in Ltac2Tutorial.tutorial1]
Monoid.madd_idr [in Ltac2Tutorial.tutorial1]
Monoid.madd_idl [in Ltac2Tutorial.tutorial1]
Monoid.madd_assoc [in Ltac2Tutorial.tutorial1]
Monoid.mzero [in Ltac2Tutorial.tutorial1]

Inductive Index

M

MonoidSimp.mexp [in Ltac2Tutorial.tutorial1]

Definition Index

D

double_num [in Ltac2Tutorial.tutorial0]

F

four [in Ltac2Tutorial.tutorial0]

M

MonoidSimpTest.test0 [in Ltac2Tutorial.tutorial1]
MonoidSimp.denote_mexps [in Ltac2Tutorial.tutorial1]
MonoidSimp.denote_mexp [in Ltac2Tutorial.tutorial1]
MonoidSimp.flatten [in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_sind [in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_rec [in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_ind [in Ltac2Tutorial.tutorial1]
MonoidSimp.mexp_rect [in Ltac2Tutorial.tutorial1]

U

Unnamed_thm5 [in Ltac2Tutorial.tutorial0]
Unnamed_thm4 [in Ltac2Tutorial.tutorial0]
Unnamed_thm3 [in Ltac2Tutorial.tutorial0]
Unnamed_thm2 [in Ltac2Tutorial.tutorial0]
Unnamed_thm1 [in Ltac2Tutorial.tutorial0]
Unnamed_thm0 [in Ltac2Tutorial.tutorial0]
Unnamed_thm0 [in Ltac2Tutorial.tutorial0]
Unnamed_thm [in Ltac2Tutorial.tutorial0]

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

(42 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

_

other

(4 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

(3 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

(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

(3 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

(6 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

(1 entry)

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

(18 entries)