Global Index

D

F

J

K

Q

R

U

V

W

X

Y

Z

_

(114 entries)

Tactic Index

D

E

F

G

H

J

K

L

O

P

Q

R

T

U

V

W

X

Y

Z

_

(20 entries)

Axiom Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

(2 entries)

Lemma Index

D

F

H

I

J

K

M

O

Q

R

S

T

U

V

W

X

Y

Z

_

(33 entries)

Constructor Index

A

B

C

D

F

G

H

I

J

K

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(11 entries)

Inductive Index

A

B

C

D

F

G

H

I

J

K

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(5 entries)

Definition Index

D

F

J

K

M

N

Q

R

S

U

V

W

X

Y

Z

_

(37 entries)

Module Index

B

C

D

E

F

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(6 entries)

Global Index

A

AbGroup [tactic definition, in abgroup]
abgroup [module]
AbGroupAux [tactic definition, in abgroup]
AbGroup1 [tactic definition, in abgroup]
AbGroup2 [tactic definition, in abgroup]
abgroup_test [module]
add_assoc [lemma, in group]
add_dx_zero [lemma, in group]
add_sx_zero [lemma, in group]
Assoc [tactic definition, in abgroup]
A_of_Group_Theory [definition, in group]

B

beq_nat_not_ref [lemma, in group_ref]
blt_imp_lt [lemma, in group_ref]
blt_nat [definition, in group_ref]
BuildVarList [tactic definition, in abgroup]

C

CGroup [tactic definition, in abgroup]
CGroupBuildVarList [tactic definition, in abgroup]
CGroupInterp [tactic definition, in abgroup]
CGroupSeekVar [tactic definition, in abgroup]
CGroupSeekVarAux [tactic definition, in abgroup]
CGroup1 [tactic definition, in abgroup]
CGroup1Aux [tactic definition, in abgroup]
CGroup2 [tactic definition, in abgroup]
cgroup_iv_op [lemma, in group]
cgroup_of [definition, in abgroup]
congr [lemma, in misc]
congr2 [lemma, in misc]

E

Eatom [constructor, in group_ref]
Eid [constructor, in group_ref]
Eiv [constructor, in group_ref]
Eop [constructor, in group_ref]
expr [inductive, in group_ref]
expr_interp [definition, in group_ref]
expr_simpl [definition, in group_ref]
expr_simpl_ok [lemma, in group_ref]
extensionality [axiom, in misc]

G

group [module]
group_dx_cancel [lemma, in group]
group_dx_id [lemma, in group]
group_dx_iv [lemma, in group]
group_id_dx_char [lemma, in group]
group_id_sx_char [lemma, in group]
group_iv_dx_char [lemma, in group]
group_iv_id [lemma, in group]
group_iv_inj [lemma, in group]
group_iv_iv [lemma, in group]
group_iv_op [lemma, in group]
group_iv_sx_char [lemma, in group]
group_morph_comp [definition, in group]
group_morph_comp_eq [lemma, in group]
group_morph_extensionality [lemma, in group]
group_morph_id [lemma, in group]
group_morph_iv [lemma, in group]
group_ref [module]
group_switch [lemma, in group]
group_sx_cancel [lemma, in group]
group_theory_monoid [lemma, in group]

H

h [definition, in group]

I

id_dx_char [definition, in group]
Id_of_Group_Theory [definition, in group]
id_sx_char [definition, in group]
Interp [tactic definition, in abgroup]
is_a_cgroup [definition, in group]
is_a_group [definition, in group]
is_a_monoid [definition, in monoid]
is_a_monoid_morph [definition, in monoid]
iv_dx_char [definition, in group]
iv_iv [definition, in group]
Iv_of_Group_Theory [definition, in group]
iv_op [definition, in group]
iv_sx_char [definition, in group]

L

lgrp [inductive, in group_ref]
lgrp_cons [constructor, in group_ref]
lgrp_interp [definition, in group_ref]
lgrp_interp1 [definition, in group_ref]
lgrp_inv [definition, in group_ref]
lgrp_nil [constructor, in group_ref]
lgrp_of_expr [definition, in group_ref]
lgrp_snoc [constructor, in group_ref]
lgrp_sort_append [definition, in group_ref]
lgrp_sort_cons [definition, in group_ref]
lgrp_sort_snoc [definition, in group_ref]
lt_imp_blt [lemma, in group_ref]
lt_imp_not_blt [lemma, in group_ref]
lt_not_refl [lemma, in group_ref]

M

MemAssoc [tactic definition, in abgroup]
misc [module]
monoid [module]

N

nondep_extensionality [lemma, in misc]
Number [tactic definition, in abgroup]
NumberAux [tactic definition, in abgroup]

O

op_assoc [definition, in group]
op_dx_id [definition, in group]
op_dx_iv [definition, in group]
Op_of_Group_Theory [definition, in group]
op_switch [definition, in group]
op_sx_id [definition, in group]
op_sx_iv [definition, in group]

P

pair [constructor, in misc]
pair1 [definition, in misc]
pair2 [definition, in misc]
plug [lemma, in misc]
plug2 [lemma, in misc]
pointer [definition, in misc]
Prod [inductive, in misc]
proof_irrelevance [axiom, in misc]

S

SeekVar [tactic definition, in abgroup]
SeekVarAux [tactic definition, in abgroup]
Star [inductive, in misc]
star_intro [constructor, in misc]
Sum [inductive, in misc]
sum1 [constructor, in misc]
sum2 [constructor, in misc]

T

type_of [definition, in misc]

Tactic Index

A

AbGroup [in abgroup]
AbGroupAux [in abgroup]
AbGroup1 [in abgroup]
AbGroup2 [in abgroup]
Assoc [in abgroup]

B

BuildVarList [in abgroup]

C

CGroup [in abgroup]
CGroupBuildVarList [in abgroup]
CGroupInterp [in abgroup]
CGroupSeekVar [in abgroup]
CGroupSeekVarAux [in abgroup]
CGroup1 [in abgroup]
CGroup1Aux [in abgroup]
CGroup2 [in abgroup]

I

Interp [in abgroup]

M

MemAssoc [in abgroup]

N

Number [in abgroup]
NumberAux [in abgroup]

S

SeekVar [in abgroup]
SeekVarAux [in abgroup]

Axiom Index

E

extensionality [in misc]

P

proof_irrelevance [in misc]

Lemma Index

A

add_assoc [in group]
add_dx_zero [in group]
add_sx_zero [in group]

B

beq_nat_not_ref [in group_ref]
blt_imp_lt [in group_ref]

C

cgroup_iv_op [in group]
congr [in misc]
congr2 [in misc]

E

expr_simpl_ok [in group_ref]

G

group_dx_cancel [in group]
group_dx_id [in group]
group_dx_iv [in group]
group_id_dx_char [in group]
group_id_sx_char [in group]
group_iv_dx_char [in group]
group_iv_id [in group]
group_iv_inj [in group]
group_iv_iv [in group]
group_iv_op [in group]
group_iv_sx_char [in group]
group_morph_comp_eq [in group]
group_morph_extensionality [in group]
group_morph_id [in group]
group_morph_iv [in group]
group_switch [in group]
group_sx_cancel [in group]
group_theory_monoid [in group]

L

lt_imp_blt [in group_ref]
lt_imp_not_blt [in group_ref]
lt_not_refl [in group_ref]

N

nondep_extensionality [in misc]

P

plug [in misc]
plug2 [in misc]

Constructor Index

E

Eatom [in group_ref]
Eid [in group_ref]
Eiv [in group_ref]
Eop [in group_ref]

L

lgrp_cons [in group_ref]
lgrp_nil [in group_ref]
lgrp_snoc [in group_ref]

P

pair [in misc]

S

star_intro [in misc]
sum1 [in misc]
sum2 [in misc]

Inductive Index

E

expr [in group_ref]

L

lgrp [in group_ref]

P

Prod [in misc]

S

Star [in misc]
Sum [in misc]

Definition Index

A

A_of_Group_Theory [in group]

B

blt_nat [in group_ref]

C

cgroup_of [in abgroup]

E

expr_interp [in group_ref]
expr_simpl [in group_ref]

G

group_morph_comp [in group]

H

h [in group]

I

id_dx_char [in group]
Id_of_Group_Theory [in group]
id_sx_char [in group]
is_a_cgroup [in group]
is_a_group [in group]
is_a_monoid [in monoid]
is_a_monoid_morph [in monoid]
iv_dx_char [in group]
iv_iv [in group]
Iv_of_Group_Theory [in group]
iv_op [in group]
iv_sx_char [in group]

L

lgrp_interp [in group_ref]
lgrp_interp1 [in group_ref]
lgrp_inv [in group_ref]
lgrp_of_expr [in group_ref]
lgrp_sort_append [in group_ref]
lgrp_sort_cons [in group_ref]
lgrp_sort_snoc [in group_ref]

O

op_assoc [in group]
op_dx_id [in group]
op_dx_iv [in group]
Op_of_Group_Theory [in group]
op_switch [in group]
op_sx_id [in group]
op_sx_iv [in group]

P

pair1 [in misc]
pair2 [in misc]
pointer [in misc]

T

type_of [in misc]

Module Index

A

abgroup
abgroup_test

G

group
group_ref

M

Global Index

D

F

J

K

Q

R

U

V

W

X

Y

Z

_

(114 entries)

Tactic Index

D

E

F

G

H

J

K

L

O

P

Q

R

T

U

V

W

X

Y

Z

_

(20 entries)

Axiom Index

A

B

C

D

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

(2 entries)

Lemma Index

D

F

H

I

J

K

M

O

Q

R

S

T

U

V

W

X

Y

Z

_

(33 entries)

Constructor Index

A

B

C

D

F

G

H

I

J

K

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(11 entries)

Inductive Index

A

B

C

D

F

G

H

I

J

K

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(5 entries)

Definition Index

D

F

J

K

M

N

Q

R

S

U

V

W

X

Y

Z

_

(37 entries)

Module Index

B

C

D

E

F

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

(6 entries)

This page has been generated by coqdoc