Global Index

B

K

V

W

X

Y

Z

_

(220 entries)

Notation Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

R

T

U

V

W

X

Y

Z

_

(14 entries)

Module Index

A

B

D

E

F

G

H

I

J

K

L

O

P

Q

T

U

V

W

X

Y

Z

_

other

(5 entries)

Library Index

A

B

E

G

H

I

J

K

M

N

O

P

S

T

V

W

X

Y

Z

_

other

(8 entries)

Lemma Index

A

B

H

J

K

O

P

T

V

W

X

Y

Z

_

other

(63 entries)

Constructor Index

A

B

D

E

F

G

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

B

D

E

F

G

H

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Projection Index

A

B

E

F

G

J

K

L

M

N

O

Q

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Instance Index

A

B

F

G

J

K

L

N

O

R

T

V

W

X

Y

Z

_

other

(36 entries)

Section Index

B

D

E

F

G

H

I

J

K

L

M

N

O

P

R

T

U

V

W

X

Y

Z

_

other

(7 entries)

Abbreviation Index

A

B

C

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

F

H

K

P

V

W

X

Y

Z

_

other

(64 entries)

Record Index

A

B

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Global Index

A

Algebraic [section, in FinSet.FinSet]

C

Canonize [definition, in FinSet.Lib.DProp]
canonize_spec [lemma, in FinSet.Lib.DProp]
CEExt [library]
choice [definition, in FinSet.Quotients.Countable]
Choice [section, in FinSet.Quotients.Countable]
choice [definition, in FinSet.Lib.CEExt]
Choice [section, in FinSet.Lib.CEExt]
ChoiceExt [section, in FinSet.Quotients.Countable]
ChoiceExt [section, in FinSet.Lib.CEExt]
Π _ _ : _ , _ [notation, in FinSet.Quotients.Countable]
Π _ _ : _ , _ [notation, in FinSet.Lib.CEExt]
choose [definition, in FinSet.Quotients.Countable]
choose [definition, in FinSet.Lib.CEExt]
choose_ext [lemma, in FinSet.Quotients.Countable]
choose_spec [lemma, in FinSet.Quotients.Countable]
choose_ext [lemma, in FinSet.Lib.CEExt]
choose_spec [lemma, in FinSet.Lib.CEExt]
compose [definition, in FinSet.Quotients.Retract]
ComprehensionNotations [module, in FinSet.FinSet]
_ \ (comprehension) [notation, in FinSet.FinSet]
_ ﬆ _ (comprehension) [notation, in FinSet.FinSet]
_ ⍪ _ ∈ _ (comprehension) [notation, in FinSet.FinSet]
⦃ _ ⦄ [notation, in FinSet.FinSet]
contradictory [projection, in FinSet.Lib.DProp]
countable [projection, in FinSet.Quotients.Countable]
Countable [record, in FinSet.Quotients.Countable]
countable [constructor, in FinSet.Quotients.Countable]
Countable [inductive, in FinSet.Quotients.Countable]
Countable [library]
countable_sum [instance, in FinSet.Quotients.Countable]
countable_pair [instance, in FinSet.Quotients.Countable]
countable_option [instance, in FinSet.Quotients.Countable]
countable_unit [instance, in FinSet.Quotients.Countable]
countable_list [instance, in FinSet.Quotients.Countable]
countable_empty_set [instance, in FinSet.Quotients.Countable]
countable_n [instance, in FinSet.Quotients.Countable]
countable_nat [instance, in FinSet.Quotients.Countable]
countable_eq_dec [definition, in FinSet.Quotients.Countable]
countable_of_opt_retract [definition, in FinSet.Quotients.Countable]
countable_of_retract [definition, in FinSet.Quotients.Countable]

D

DAnd [definition, in FinSet.Lib.DProp]
dand_proper [instance, in FinSet.Lib.DProp]
dec [projection, in FinSet.Lib.DProp]
dec_irrelevant [lemma, in FinSet.Lib.DProp]
dec_alt [definition, in FinSet.Lib.DProp]
dec_lift [abbreviation, in FinSet.Lib.DProp]
deduplicate [definition, in FinSet.Lib.ListSet]
deduplicate_eq_set_list [lemma, in FinSet.Lib.ListSet]
deduplicate_nodup [lemma, in FinSet.Lib.ListSet]
Denies [projection, in FinSet.Lib.DProp]
denies_proper [instance, in FinSet.Lib.DProp]
denies_spec [lemma, in FinSet.Lib.DProp]
dexists [definition, in FinSet.FinSet]
dexists [definition, in FinSet.Lib.ListSet]
DFalse [definition, in FinSet.Lib.DProp]
dforall [definition, in FinSet.FinSet]
dforall [definition, in FinSet.Lib.ListSet]
DNot [definition, in FinSet.Lib.DProp]
dnot_proper [instance, in FinSet.Lib.DProp]
dnot_spec [lemma, in FinSet.Lib.DProp]
DOr [definition, in FinSet.Lib.DProp]
dor_proper [instance, in FinSet.Lib.DProp]
double_inclusion [lemma, in FinSet.FinSet]
DProp [record, in FinSet.Lib.DProp]
DProp [library]
dprop_of_bool [definition, in FinSet.Lib.DProp]
dprop_proper [instance, in FinSet.Lib.DProp]
dsigma_ext [lemma, in FinSet.Lib.DProp]
DTrue [definition, in FinSet.Lib.DProp]

E

elim_is_true_false [definition, in FinSet.Lib.DProp]
empty [definition, in FinSet.FinSet]
empty_bottom [lemma, in FinSet.FinSet]
empty_spec_iff [lemma, in FinSet.FinSet]
empty_spec [lemma, in FinSet.FinSet]
equivalence_preorder [instance, in FinSet.Lib.ListSet]
eq_dprop_eq [instance, in FinSet.Lib.DProp]
eq_dprop [definition, in FinSet.Lib.DProp]
eq_countable_eq [instance, in FinSet.Quotients.Countable]
eq_countable [definition, in FinSet.Quotients.Countable]
eq_set_eq [instance, in FinSet.Quotients.UList]
eq_set_ulist [definition, in FinSet.Quotients.UList]
eq_set_list_eq [instance, in FinSet.Lib.ListSet]
eq_set_list [definition, in FinSet.Lib.ListSet]
exists_dec [definition, in FinSet.Lib.ListSet]

F

filter_nodup [lemma, in FinSet.Lib.ListSet]
filter_sub [lemma, in FinSet.Lib.ListSet]
FinSet [library]

G

guard [definition, in FinSet.FinSet]
guard_Union [lemma, in FinSet.FinSet]
guard_spec [lemma, in FinSet.FinSet]
guard_spec_tt [lemma, in FinSet.FinSet]

H

head [constructor, in FinSet.Lib.ListSet]
Holds [projection, in FinSet.Lib.DProp]
holds_proper [instance, in FinSet.Lib.DProp]

I

id [definition, in FinSet.Quotients.Retract]
included_list_preorder [instance, in FinSet.Lib.ListSet]
included_list [definition, in FinSet.Lib.ListSet]
inhabitant [projection, in FinSet.Quotients.Countable]
inhabitant [constructor, in FinSet.Quotients.Countable]
Inhabited [record, in FinSet.Quotients.Countable]
Inhabited [inductive, in FinSet.Quotients.Countable]
inhabited_sum_right [instance, in FinSet.Quotients.Countable]
inhabited_sum_left [instance, in FinSet.Quotients.Countable]
inhabited_pair [instance, in FinSet.Quotients.Countable]
inhabited_list [instance, in FinSet.Quotients.Countable]
inhabited_option [instance, in FinSet.Quotients.Countable]
inhabited_unit [instance, in FinSet.Quotients.Countable]
inj [projection, in FinSet.Quotients.Retract]
inter [definition, in FinSet.FinSet]
inter_inf [lemma, in FinSet.FinSet]
inter_union_distr [lemma, in FinSet.FinSet]
inter_idempotent [lemma, in FinSet.FinSet]
inter_commutative [lemma, in FinSet.FinSet]
inter_assoc [lemma, in FinSet.FinSet]
inter_spec [lemma, in FinSet.FinSet]
in_eq_set [instance, in FinSet.FinSet]
in_is_mem [lemma, in FinSet.Lib.ListSet]
irrelevant_is_true [lemma, in FinSet.Lib.DProp]
irrelevant_canonize [lemma, in FinSet.Lib.DProp]
Is_true [inductive, in FinSet.Lib.DProp]

J

join [definition, in FinSet.FinSet]

L

Liftp [definition, in FinSet.Quotients.Countable]
liftp_extract_ext [lemma, in FinSet.Quotients.Countable]
liftp_extract [definition, in FinSet.Quotients.Countable]
Liftp_exists [lemma, in FinSet.Quotients.Countable]
linear_search_ext [lemma, in FinSet.Lib.CEExt]
listset [definition, in FinSet.FinSet]
ListSet [library]

M

map [definition, in FinSet.FinSet]
mem [definition, in FinSet.FinSet]
Mem [inductive, in FinSet.Lib.ListSet]
MembershipNotation [module, in FinSet.FinSet]
_ ∈ _ [notation, in FinSet.FinSet]
mem_spec_in [lemma, in FinSet.FinSet]
mem_spec [lemma, in FinSet.FinSet]
mem_eq_set_list_proper [instance, in FinSet.Lib.ListSet]
mem_eq_set_list [lemma, in FinSet.Lib.ListSet]
mem_included_list [lemma, in FinSet.Lib.ListSet]
mem_of_mem_list_spec [lemma, in FinSet.Lib.ListSet]
mem_of_mem_list [definition, in FinSet.Lib.ListSet]
mem_list_app [lemma, in FinSet.Lib.ListSet]
mem_list_cons [lemma, in FinSet.Lib.ListSet]
mem_list_left [lemma, in FinSet.Lib.ListSet]
mem_list_right [lemma, in FinSet.Lib.ListSet]
mem_list [definition, in FinSet.Lib.ListSet]

N

nat_retract [lemma, in FinSet.Quotients.Countable]
nodup [definition, in FinSet.Lib.ListSet]
Notations [module, in FinSet.FinSet]
no_mem_list_empty [lemma, in FinSet.Lib.ListSet]
no_mem_empty [definition, in FinSet.Lib.ListSet]

O

of_nat [definition, in FinSet.Quotients.Countable]
of_mem [definition, in FinSet.Lib.ListSet]
opt_lift [definition, in FinSet.Quotients.Retract]
opt_compose [definition, in FinSet.Quotients.Retract]

P

PreOrder [instance, in FinSet.FinSet]
proj [projection, in FinSet.Quotients.Retract]
proj_proper [instance, in FinSet.Quotients.Quotient]

Q

Quantifiers [section, in FinSet.FinSet]
_ ∈ _ [notation, in FinSet.FinSet]
quotient [definition, in FinSet.Quotients.Quotient]
Quotient [definition, in FinSet.Quotients.Quotient]
Quotient [library]
quotient_inhabited [instance, in FinSet.Quotients.Quotient]
quotient_countable [instance, in FinSet.Quotients.Quotient]
quotient_ext [lemma, in FinSet.Quotients.Quotient]

R

retract [projection, in FinSet.Quotients.Retract]
Retract [record, in FinSet.Quotients.Retract]
Retract [library]
RetractNListNat [module, in FinSet.Quotients.Retract]
RetractNListNat.decode [definition, in FinSet.Quotients.Retract]
RetractNListNat.decode_positive [definition, in FinSet.Quotients.Retract]
RetractNListNat.encode [definition, in FinSet.Quotients.Retract]
RetractNListNat.encode_nat [definition, in FinSet.Quotients.Retract]
RetractNListNat.retract [lemma, in FinSet.Quotients.Retract]
retract_N_list_nat [definition, in FinSet.Quotients.Retract]
retract_nat_N [definition, in FinSet.Quotients.Retract]
retract_nat_inh [definition, in FinSet.Quotients.Retract]
retract_nat_opt [definition, in FinSet.Quotients.Retract]

S

SetNotations [module, in FinSet.FinSet]
_ ⊆ _ [notation, in FinSet.FinSet]
_ ∩ _ [notation, in FinSet.FinSet]
_ ∪ _ [notation, in FinSet.FinSet]
∅ [notation, in FinSet.FinSet]
SetOperations [section, in FinSet.FinSet]
set_ext [lemma, in FinSet.FinSet]
set_unique [lemma, in FinSet.FinSet]
set_quotient [lemma, in FinSet.FinSet]
set_countable [instance, in FinSet.FinSet]
singleton [definition, in FinSet.FinSet]
singleton_self [lemma, in FinSet.FinSet]
singleton_spec [lemma, in FinSet.FinSet]
subset [definition, in FinSet.FinSet]

T

T [definition, in FinSet.FinSet]
tail [constructor, in FinSet.Lib.ListSet]
to_nat [definition, in FinSet.Quotients.Countable]
true_is_true [constructor, in FinSet.Lib.DProp]

U

ulist [definition, in FinSet.Quotients.UList]
UList [definition, in FinSet.Quotients.UList]
UList [library]
ulist_inhabited [instance, in FinSet.Quotients.UList]
ulist_countable [instance, in FinSet.Quotients.UList]
ulist_proper [instance, in FinSet.Quotients.UList]
ulist_eq_set [lemma, in FinSet.Quotients.UList]
ulist_nodup [lemma, in FinSet.Quotients.UList]
ulist_ext [lemma, in FinSet.Quotients.UList]
Union [definition, in FinSet.FinSet]
union [definition, in FinSet.FinSet]
union_sup [lemma, in FinSet.FinSet]
union_inter_distr [lemma, in FinSet.FinSet]
union_idempotent [lemma, in FinSet.FinSet]
union_commutative [lemma, in FinSet.FinSet]
union_empty_right_unit [lemma, in FinSet.FinSet]
union_empty_left_unit [lemma, in FinSet.FinSet]
union_assoc [lemma, in FinSet.FinSet]
Union_spec [lemma, in FinSet.FinSet]
union_spec [lemma, in FinSet.FinSet]
universal [lemma, in FinSet.Quotients.Quotient]

other

_ || _ [notation, in FinSet.Lib.DProp]
_ && _ [notation, in FinSet.Lib.DProp]

Notation Index

C

Π _ _ : _ , _ [in FinSet.Quotients.Countable]
Π _ _ : _ , _ [in FinSet.Lib.CEExt]
_ \ (comprehension) [in FinSet.FinSet]
_ ﬆ _ (comprehension) [in FinSet.FinSet]
_ ⍪ _ ∈ _ (comprehension) [in FinSet.FinSet]
⦃ _ ⦄ [in FinSet.FinSet]

M

_ ∈ _ [in FinSet.FinSet]

Q

_ ∈ _ [in FinSet.FinSet]

S

_ ⊆ _ [in FinSet.FinSet]
_ ∩ _ [in FinSet.FinSet]
_ ∪ _ [in FinSet.FinSet]
∅ [in FinSet.FinSet]

other

_ || _ [in FinSet.Lib.DProp]
_ && _ [in FinSet.Lib.DProp]

Module Index

C

ComprehensionNotations [in FinSet.FinSet]

M

MembershipNotation [in FinSet.FinSet]

N

Notations [in FinSet.FinSet]

R

RetractNListNat [in FinSet.Quotients.Retract]

S

SetNotations [in FinSet.FinSet]

Library Index

C

CEExt
Countable

D

DProp

F

FinSet

L

Q

R

U

UList

Lemma Index

C

canonize_spec [in FinSet.Lib.DProp]
choose_ext [in FinSet.Quotients.Countable]
choose_spec [in FinSet.Quotients.Countable]
choose_ext [in FinSet.Lib.CEExt]
choose_spec [in FinSet.Lib.CEExt]

D

dec_irrelevant [in FinSet.Lib.DProp]
deduplicate_eq_set_list [in FinSet.Lib.ListSet]
deduplicate_nodup [in FinSet.Lib.ListSet]
denies_spec [in FinSet.Lib.DProp]
dnot_spec [in FinSet.Lib.DProp]
double_inclusion [in FinSet.FinSet]
dsigma_ext [in FinSet.Lib.DProp]

E

empty_bottom [in FinSet.FinSet]
empty_spec_iff [in FinSet.FinSet]
empty_spec [in FinSet.FinSet]

F

filter_nodup [in FinSet.Lib.ListSet]
filter_sub [in FinSet.Lib.ListSet]

G

guard_Union [in FinSet.FinSet]
guard_spec [in FinSet.FinSet]
guard_spec_tt [in FinSet.FinSet]

I

inter_inf [in FinSet.FinSet]
inter_union_distr [in FinSet.FinSet]
inter_idempotent [in FinSet.FinSet]
inter_commutative [in FinSet.FinSet]
inter_assoc [in FinSet.FinSet]
inter_spec [in FinSet.FinSet]
in_is_mem [in FinSet.Lib.ListSet]
irrelevant_is_true [in FinSet.Lib.DProp]
irrelevant_canonize [in FinSet.Lib.DProp]

L

liftp_extract_ext [in FinSet.Quotients.Countable]
Liftp_exists [in FinSet.Quotients.Countable]
linear_search_ext [in FinSet.Lib.CEExt]

M

mem_spec_in [in FinSet.FinSet]
mem_spec [in FinSet.FinSet]
mem_eq_set_list [in FinSet.Lib.ListSet]
mem_included_list [in FinSet.Lib.ListSet]
mem_of_mem_list_spec [in FinSet.Lib.ListSet]
mem_list_app [in FinSet.Lib.ListSet]
mem_list_cons [in FinSet.Lib.ListSet]
mem_list_left [in FinSet.Lib.ListSet]
mem_list_right [in FinSet.Lib.ListSet]

N

nat_retract [in FinSet.Quotients.Countable]
no_mem_list_empty [in FinSet.Lib.ListSet]

Q

quotient_ext [in FinSet.Quotients.Quotient]

R

RetractNListNat.retract [in FinSet.Quotients.Retract]

S

set_ext [in FinSet.FinSet]
set_unique [in FinSet.FinSet]
set_quotient [in FinSet.FinSet]
singleton_self [in FinSet.FinSet]
singleton_spec [in FinSet.FinSet]

U

ulist_eq_set [in FinSet.Quotients.UList]
ulist_nodup [in FinSet.Quotients.UList]
ulist_ext [in FinSet.Quotients.UList]
union_sup [in FinSet.FinSet]
union_inter_distr [in FinSet.FinSet]
union_idempotent [in FinSet.FinSet]
union_commutative [in FinSet.FinSet]
union_empty_right_unit [in FinSet.FinSet]
union_empty_left_unit [in FinSet.FinSet]
union_assoc [in FinSet.FinSet]
Union_spec [in FinSet.FinSet]
union_spec [in FinSet.FinSet]
universal [in FinSet.Quotients.Quotient]

Constructor Index

C

countable [in FinSet.Quotients.Countable]

H

head [in FinSet.Lib.ListSet]

I

inhabitant [in FinSet.Quotients.Countable]

T

tail [in FinSet.Lib.ListSet]
true_is_true [in FinSet.Lib.DProp]

Inductive Index

C

Countable [in FinSet.Quotients.Countable]

I

Inhabited [in FinSet.Quotients.Countable]
Is_true [in FinSet.Lib.DProp]

M

Mem [in FinSet.Lib.ListSet]

Projection Index

C

contradictory [in FinSet.Lib.DProp]
countable [in FinSet.Quotients.Countable]

D

dec [in FinSet.Lib.DProp]
Denies [in FinSet.Lib.DProp]

H

Holds [in FinSet.Lib.DProp]

I

inhabitant [in FinSet.Quotients.Countable]
inj [in FinSet.Quotients.Retract]

P

proj [in FinSet.Quotients.Retract]

R

retract [in FinSet.Quotients.Retract]

Instance Index

C

countable_sum [in FinSet.Quotients.Countable]
countable_pair [in FinSet.Quotients.Countable]
countable_option [in FinSet.Quotients.Countable]
countable_unit [in FinSet.Quotients.Countable]
countable_list [in FinSet.Quotients.Countable]
countable_empty_set [in FinSet.Quotients.Countable]
countable_n [in FinSet.Quotients.Countable]
countable_nat [in FinSet.Quotients.Countable]

D

dand_proper [in FinSet.Lib.DProp]
denies_proper [in FinSet.Lib.DProp]
dnot_proper [in FinSet.Lib.DProp]
dor_proper [in FinSet.Lib.DProp]
dprop_proper [in FinSet.Lib.DProp]

E

equivalence_preorder [in FinSet.Lib.ListSet]
eq_dprop_eq [in FinSet.Lib.DProp]
eq_countable_eq [in FinSet.Quotients.Countable]
eq_set_eq [in FinSet.Quotients.UList]
eq_set_list_eq [in FinSet.Lib.ListSet]

H

holds_proper [in FinSet.Lib.DProp]

I

included_list_preorder [in FinSet.Lib.ListSet]
inhabited_sum_right [in FinSet.Quotients.Countable]
inhabited_sum_left [in FinSet.Quotients.Countable]
inhabited_pair [in FinSet.Quotients.Countable]
inhabited_list [in FinSet.Quotients.Countable]
inhabited_option [in FinSet.Quotients.Countable]
inhabited_unit [in FinSet.Quotients.Countable]
in_eq_set [in FinSet.FinSet]

M

mem_eq_set_list_proper [in FinSet.Lib.ListSet]

P

PreOrder [in FinSet.FinSet]
proj_proper [in FinSet.Quotients.Quotient]

Q

quotient_inhabited [in FinSet.Quotients.Quotient]
quotient_countable [in FinSet.Quotients.Quotient]

S

set_countable [in FinSet.FinSet]

U

ulist_inhabited [in FinSet.Quotients.UList]
ulist_countable [in FinSet.Quotients.UList]
ulist_proper [in FinSet.Quotients.UList]

Section Index

A

Algebraic [in FinSet.FinSet]

C

Choice [in FinSet.Quotients.Countable]
Choice [in FinSet.Lib.CEExt]
ChoiceExt [in FinSet.Quotients.Countable]
ChoiceExt [in FinSet.Lib.CEExt]

Q

Quantifiers [in FinSet.FinSet]

S

SetOperations [in FinSet.FinSet]

Abbreviation Index

D

dec_lift [in FinSet.Lib.DProp]

Definition Index

C

Canonize [in FinSet.Lib.DProp]
choice [in FinSet.Quotients.Countable]
choice [in FinSet.Lib.CEExt]
choose [in FinSet.Quotients.Countable]
choose [in FinSet.Lib.CEExt]
compose [in FinSet.Quotients.Retract]
countable_eq_dec [in FinSet.Quotients.Countable]
countable_of_opt_retract [in FinSet.Quotients.Countable]
countable_of_retract [in FinSet.Quotients.Countable]

D

DAnd [in FinSet.Lib.DProp]
dec_alt [in FinSet.Lib.DProp]
deduplicate [in FinSet.Lib.ListSet]
dexists [in FinSet.FinSet]
dexists [in FinSet.Lib.ListSet]
DFalse [in FinSet.Lib.DProp]
dforall [in FinSet.FinSet]
dforall [in FinSet.Lib.ListSet]
DNot [in FinSet.Lib.DProp]
DOr [in FinSet.Lib.DProp]
dprop_of_bool [in FinSet.Lib.DProp]
DTrue [in FinSet.Lib.DProp]

E

elim_is_true_false [in FinSet.Lib.DProp]
empty [in FinSet.FinSet]
eq_dprop [in FinSet.Lib.DProp]
eq_countable [in FinSet.Quotients.Countable]
eq_set_ulist [in FinSet.Quotients.UList]
eq_set_list [in FinSet.Lib.ListSet]
exists_dec [in FinSet.Lib.ListSet]

G

guard [in FinSet.FinSet]

I

id [in FinSet.Quotients.Retract]
included_list [in FinSet.Lib.ListSet]
inter [in FinSet.FinSet]

J

join [in FinSet.FinSet]

L

Liftp [in FinSet.Quotients.Countable]
liftp_extract [in FinSet.Quotients.Countable]
listset [in FinSet.FinSet]

M

map [in FinSet.FinSet]
mem [in FinSet.FinSet]
mem_of_mem_list [in FinSet.Lib.ListSet]
mem_list [in FinSet.Lib.ListSet]

N

nodup [in FinSet.Lib.ListSet]
no_mem_empty [in FinSet.Lib.ListSet]

O

of_nat [in FinSet.Quotients.Countable]
of_mem [in FinSet.Lib.ListSet]
opt_lift [in FinSet.Quotients.Retract]
opt_compose [in FinSet.Quotients.Retract]

Q

quotient [in FinSet.Quotients.Quotient]
Quotient [in FinSet.Quotients.Quotient]

R

RetractNListNat.decode [in FinSet.Quotients.Retract]
RetractNListNat.decode_positive [in FinSet.Quotients.Retract]
RetractNListNat.encode [in FinSet.Quotients.Retract]
RetractNListNat.encode_nat [in FinSet.Quotients.Retract]
retract_N_list_nat [in FinSet.Quotients.Retract]
retract_nat_N [in FinSet.Quotients.Retract]
retract_nat_inh [in FinSet.Quotients.Retract]
retract_nat_opt [in FinSet.Quotients.Retract]

S

singleton [in FinSet.FinSet]
subset [in FinSet.FinSet]

T

T [in FinSet.FinSet]
to_nat [in FinSet.Quotients.Countable]

U

ulist [in FinSet.Quotients.UList]
UList [in FinSet.Quotients.UList]
Union [in FinSet.FinSet]
union [in FinSet.FinSet]

Record Index

C

Countable [in FinSet.Quotients.Countable]

D

DProp [in FinSet.Lib.DProp]

I

Inhabited [in FinSet.Quotients.Countable]

R

Retract [in FinSet.Quotients.Retract]

Global Index

B

K

V

W

X

Y

Z

_

(220 entries)

Notation Index

A

B

D

E

F

G

H

I

J

K

L

N

O

P

R

T

U

V

W

X

Y

Z

_

(14 entries)

Module Index

A

B

D

E

F

G

H

I

J

K

L

O

P

Q

T

U

V

W

X

Y

Z

_

other

(5 entries)

Library Index

A

B

E

G

H

I

J

K

M

N

O

P

S

T

V

W

X

Y

Z

_

other

(8 entries)

Lemma Index

A

B

H

J

K

O

P

T

V

W

X

Y

Z

_

other

(63 entries)

Constructor Index

A

B

D

E

F

G

J

K

L

M

N

O

P

Q

R

S

U

V

W

X

Y

Z

_

other

(5 entries)

Inductive Index

A

B

D

E

F

G

H

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Projection Index

A

B

E

F

G

J

K

L

M

N

O

Q

S

T

U

V

W

X

Y

Z

_

other

(9 entries)

Instance Index

A

B

F

G

J

K

L

N

O

R

T

V

W

X

Y

Z

_

other

(36 entries)

Section Index

B

D

E

F

G

H

I

J

K

L

M

N

O

P

R

T

U

V

W

X

Y

Z

_

other

(7 entries)

Abbreviation Index

A

B

C

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

F

H

K

P

V

W

X

Y

Z

_

other

(64 entries)

Record Index

A

B

E

F

G

H

J

K

L

M

N

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

This page has been generated by coqdoc