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

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

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

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

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

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

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

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

(2 entries)

---

Global Index

C

completeness [lemma, in DProp.Prop]
completeness [lemma, in DProp.Prop_solutions]

D

denotation [definition, in DProp.Prop]
denotation [definition, in DProp.Prop_solutions]

E

entails [definition, in DProp.Prop]
entails [definition, in DProp.Prop_solutions]
equivalent [definition, in DProp.Prop]
equivalent [definition, in DProp.Prop_solutions]
excluded_middle [projection, in DProp.Prop]
excluded_middle [projection, in DProp.Prop_solutions]
exercise1 [lemma, in DProp.Prop]
exercise1 [lemma, in DProp.Prop_solutions]
exercise2 [lemma, in DProp.Prop]
exercise2 [lemma, in DProp.Prop_solutions]
exercise3 [lemma, in DProp.Prop]
exercise3 [lemma, in DProp.Prop_solutions]
exercise4 [lemma, in DProp.Prop]
exercise4 [lemma, in DProp.Prop_solutions]
exercise5 [lemma, in DProp.Prop]
exercise5 [lemma, in DProp.Prop_solutions]

F

full_lem [lemma, in DProp.Prop]
full_lem [lemma, in DProp.Prop_solutions]

J

j_top_intro [constructor, in DProp.Prop]
j_raa [constructor, in DProp.Prop]
j_neg_elim [constructor, in DProp.Prop]
j_neg_intro [constructor, in DProp.Prop]
j_conj_elim2 [constructor, in DProp.Prop]
j_conj_elim1 [constructor, in DProp.Prop]
j_conj_intro [constructor, in DProp.Prop]
j_var [constructor, in DProp.Prop]
j_top_intro [constructor, in DProp.Prop_solutions]
j_dne [constructor, in DProp.Prop_solutions]
j_neg_elim [constructor, in DProp.Prop_solutions]
j_neg_intro [constructor, in DProp.Prop_solutions]
j_conj_elim2 [constructor, in DProp.Prop_solutions]
j_conj_elim1 [constructor, in DProp.Prop_solutions]
j_conj_intro [constructor, in DProp.Prop_solutions]
j_var [constructor, in DProp.Prop_solutions]

M

model [definition, in DProp.Prop]
model [definition, in DProp.Prop_solutions]
models [definition, in DProp.Prop]
models [definition, in DProp.Prop_solutions]

P

Prop [library]
Prop_solutions [library]
provable [inductive, in DProp.Prop]
provable [inductive, in DProp.Prop_solutions]
p_neg [constructor, in DProp.Prop]
p_conj [constructor, in DProp.Prop]
p_var [constructor, in DProp.Prop]
p_top [constructor, in DProp.Prop]
p_neg [constructor, in DProp.Prop_solutions]
p_conj [constructor, in DProp.Prop_solutions]
p_var [constructor, in DProp.Prop_solutions]
p_top [constructor, in DProp.Prop_solutions]

S

sentence [inductive, in DProp.Prop]
sentence [inductive, in DProp.Prop_solutions]
soundness [lemma, in DProp.Prop]
soundness [lemma, in DProp.Prop_solutions]
substitution [lemma, in DProp.Prop]
substitution [lemma, in DProp.Prop_solutions]
syntactical_incompleteness [lemma, in DProp.Prop]
syntactical_incompleteness [lemma, in DProp.Prop]
syntactical_incompleteness [lemma, in DProp.Prop_solutions]
syntactical_incompleteness [lemma, in DProp.Prop_solutions]

T

Tactics [library]
tautology [definition, in DProp.Prop]
tautology [definition, in DProp.Prop_solutions]

U

Unnamed_thm0 [definition, in DProp.Prop]
Unnamed_thm [definition, in DProp.Prop]
Unnamed_thm0 [definition, in DProp.Prop_solutions]
Unnamed_thm [definition, in DProp.Prop_solutions]

V

val [projection, in DProp.Prop]
val [projection, in DProp.Prop_solutions]
valuation [record, in DProp.Prop]
valuation [record, in DProp.Prop_solutions]
vfalse [definition, in DProp.Prop]
vfalse [definition, in DProp.Prop_solutions]
vtrue [definition, in DProp.Prop]
vtrue [definition, in DProp.Prop_solutions]

W

weakening [lemma, in DProp.Prop]
weakening [lemma, in DProp.Prop_solutions]

other

_ ⊢ _ [notation, in DProp.Prop]
_ ⊧ _ [notation, in DProp.Prop]
_ ⇒ _ [notation, in DProp.Prop]
_ ∨ _ [notation, in DProp.Prop]
_ ∧ _ [notation, in DProp.Prop]
_ ⊢ _ [notation, in DProp.Prop_solutions]
_ ⊧ _ [notation, in DProp.Prop_solutions]
_ ⇒ _ [notation, in DProp.Prop_solutions]
_ ∨ _ [notation, in DProp.Prop_solutions]
_ ∧ _ [notation, in DProp.Prop_solutions]
P [notation, in DProp.Prop]
P [notation, in DProp.Prop_solutions]
Q [notation, in DProp.Prop]
Q [notation, in DProp.Prop_solutions]
R [notation, in DProp.Prop]
R [notation, in DProp.Prop_solutions]
¬ _ [notation, in DProp.Prop]
¬ _ [notation, in DProp.Prop_solutions]
⊤ [notation, in DProp.Prop]
⊤ [notation, in DProp.Prop_solutions]
⊥ [notation, in DProp.Prop]
⊥ [notation, in DProp.Prop_solutions]
⟦ _ ⟧ [notation, in DProp.Prop]
⟦ _ ⟧ [notation, in DProp.Prop_solutions]

---

Notation Index

other

_ ⊢ _ [in DProp.Prop]
_ ⊧ _ [in DProp.Prop]
_ ⇒ _ [in DProp.Prop]
_ ∨ _ [in DProp.Prop]
_ ∧ _ [in DProp.Prop]
_ ⊢ _ [in DProp.Prop_solutions]
_ ⊧ _ [in DProp.Prop_solutions]
_ ⇒ _ [in DProp.Prop_solutions]
_ ∨ _ [in DProp.Prop_solutions]
_ ∧ _ [in DProp.Prop_solutions]
P [in DProp.Prop]
P [in DProp.Prop_solutions]
Q [in DProp.Prop]
Q [in DProp.Prop_solutions]
R [in DProp.Prop]
R [in DProp.Prop_solutions]
¬ _ [in DProp.Prop]
¬ _ [in DProp.Prop_solutions]
⊤ [in DProp.Prop]
⊤ [in DProp.Prop_solutions]
⊥ [in DProp.Prop]
⊥ [in DProp.Prop_solutions]
⟦ _ ⟧ [in DProp.Prop]
⟦ _ ⟧ [in DProp.Prop_solutions]

---

Library Index

P

Prop
Prop_solutions

T

Tactics

---

Lemma Index

C

completeness [in DProp.Prop]
completeness [in DProp.Prop_solutions]

E

exercise1 [in DProp.Prop]
exercise1 [in DProp.Prop_solutions]
exercise2 [in DProp.Prop]
exercise2 [in DProp.Prop_solutions]
exercise3 [in DProp.Prop]
exercise3 [in DProp.Prop_solutions]
exercise4 [in DProp.Prop]
exercise4 [in DProp.Prop_solutions]
exercise5 [in DProp.Prop]
exercise5 [in DProp.Prop_solutions]

F

full_lem [in DProp.Prop]
full_lem [in DProp.Prop_solutions]

S

soundness [in DProp.Prop]
soundness [in DProp.Prop_solutions]
substitution [in DProp.Prop]
substitution [in DProp.Prop_solutions]
syntactical_incompleteness [in DProp.Prop]
syntactical_incompleteness [in DProp.Prop]
syntactical_incompleteness [in DProp.Prop_solutions]
syntactical_incompleteness [in DProp.Prop_solutions]

W

weakening [in DProp.Prop]
weakening [in DProp.Prop_solutions]

---

Constructor Index

J

j_top_intro [in DProp.Prop]
j_raa [in DProp.Prop]
j_neg_elim [in DProp.Prop]
j_neg_intro [in DProp.Prop]
j_conj_elim2 [in DProp.Prop]
j_conj_elim1 [in DProp.Prop]
j_conj_intro [in DProp.Prop]
j_var [in DProp.Prop]
j_top_intro [in DProp.Prop_solutions]
j_dne [in DProp.Prop_solutions]
j_neg_elim [in DProp.Prop_solutions]
j_neg_intro [in DProp.Prop_solutions]
j_conj_elim2 [in DProp.Prop_solutions]
j_conj_elim1 [in DProp.Prop_solutions]
j_conj_intro [in DProp.Prop_solutions]
j_var [in DProp.Prop_solutions]

P

p_neg [in DProp.Prop]
p_conj [in DProp.Prop]
p_var [in DProp.Prop]
p_top [in DProp.Prop]
p_neg [in DProp.Prop_solutions]
p_conj [in DProp.Prop_solutions]
p_var [in DProp.Prop_solutions]
p_top [in DProp.Prop_solutions]

---

Inductive Index

P

provable [in DProp.Prop]
provable [in DProp.Prop_solutions]

S

sentence [in DProp.Prop]
sentence [in DProp.Prop_solutions]

---

Projection Index

E

excluded_middle [in DProp.Prop]
excluded_middle [in DProp.Prop_solutions]

V

val [in DProp.Prop]
val [in DProp.Prop_solutions]

---

Definition Index

D

denotation [in DProp.Prop]
denotation [in DProp.Prop_solutions]

E

entails [in DProp.Prop]
entails [in DProp.Prop_solutions]
equivalent [in DProp.Prop]
equivalent [in DProp.Prop_solutions]

M

model [in DProp.Prop]
model [in DProp.Prop_solutions]
models [in DProp.Prop]
models [in DProp.Prop_solutions]

T

tautology [in DProp.Prop]
tautology [in DProp.Prop_solutions]

U

Unnamed_thm0 [in DProp.Prop]
Unnamed_thm [in DProp.Prop]
Unnamed_thm0 [in DProp.Prop_solutions]
Unnamed_thm [in DProp.Prop_solutions]

V

vfalse [in DProp.Prop]
vfalse [in DProp.Prop_solutions]
vtrue [in DProp.Prop]
vtrue [in DProp.Prop_solutions]

---

Record Index

V

valuation [in DProp.Prop]
valuation [in DProp.Prop_solutions]

---

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

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

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

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

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

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

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

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

(2 entries)

Generated by coqdoc and improved with CoqdocJS