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

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

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

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

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

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

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

(11 entries)

---

Global Index

A

assertion [definition, in Hoare]
Assign [constructor, in ImpSimpl]

B

beval [definition, in ImpSimpl]
bexp [inductive, in ImpSimpl]

C

cmd [inductive, in ImpSimpl]
completeness [lemma, in Hoare]
Const [constructor, in ImpSimpl]

E

Equal [constructor, in ImpSimpl]
eval [definition, in ImpSimpl]
ExAssign [constructor, in ImpSimpl]
exec [inductive, in ImpSimpl]
ExIfFalse [constructor, in ImpSimpl]
ExIfTrue [constructor, in ImpSimpl]
exp [inductive, in ImpSimpl]
ExSeq [constructor, in ImpSimpl]
ExSkip [constructor, in ImpSimpl]
ExWhileFalse [constructor, in ImpSimpl]
ExWhileTrue [constructor, in ImpSimpl]

H

himpl [definition, in Hoare]
Hoare [library]
hoare_triple_sound [lemma, in Hoare]
hoare_triple_big_step_while [lemma, in Hoare]
hoare_triple [inductive, in Hoare]
hoare_valid [definition, in Hoare]
hoare_interp [definition, in Hoare]
HtAssign [constructor, in Hoare]
HtConsequence [constructor, in Hoare]
HtExists [constructor, in Hoare]
HtIf [constructor, in Hoare]
HtSeq [constructor, in Hoare]
HtSkip [constructor, in Hoare]
HtStrengthenPost [lemma, in Hoare]
HtWeakenPre [lemma, in Hoare]
HtWhileInv [constructor, in Hoare]

I

If_ [constructor, in ImpSimpl]
ImpSimpl [library]

L

Less [constructor, in ImpSimpl]

M

Minus [constructor, in ImpSimpl]
Mult [constructor, in ImpSimpl]

P

Plus [constructor, in ImpSimpl]

S

Seq [constructor, in ImpSimpl]
set [definition, in ImpSimpl]
Skip [constructor, in ImpSimpl]

V

valuation [definition, in ImpSimpl]
var [definition, in ImpSimpl]
Var [constructor, in ImpSimpl]

W

WeP [definition, in Hoare]
While_ [constructor, in ImpSimpl]
wpl [definition, in Hoare]
wpl_soundness_synt [lemma, in Hoare]
wpl_mon [lemma, in Hoare]
wpl_entailment' [lemma, in Hoare]
wpl_entailment [lemma, in Hoare]
wpl_complete_sem' [lemma, in Hoare]
wpl_complete_sem [lemma, in Hoare]
wpl_sound_sem [lemma, in Hoare]

other

_ ;; _ (cmd_scope) [notation, in ImpSimpl]
_ <- _ (cmd_scope) [notation, in ImpSimpl]
_ < _ (cmd_scope) [notation, in ImpSimpl]
_ = _ (cmd_scope) [notation, in ImpSimpl]
_ * _ (cmd_scope) [notation, in ImpSimpl]
_ - _ (cmd_scope) [notation, in ImpSimpl]
_ + _ (cmd_scope) [notation, in ImpSimpl]
_ < _ (reset_scope) [notation, in ImpSimpl]
_ = _ (reset_scope) [notation, in ImpSimpl]
_ * _ (reset_scope) [notation, in ImpSimpl]
_ - _ (reset_scope) [notation, in ImpSimpl]
_ + _ (reset_scope) [notation, in ImpSimpl]
_ $! _ [notation, in ImpSimpl]
_ ==> _ [notation, in Hoare]
when _ then _ else _ done [notation, in ImpSimpl]
{{ _ }} while _ loop _ done [notation, in ImpSimpl]
{{ _ }} _ {{ _ }} [notation, in Hoare]

---

Notation Index

other

_ ;; _ (cmd_scope) [in ImpSimpl]
_ <- _ (cmd_scope) [in ImpSimpl]
_ < _ (cmd_scope) [in ImpSimpl]
_ = _ (cmd_scope) [in ImpSimpl]
_ * _ (cmd_scope) [in ImpSimpl]
_ - _ (cmd_scope) [in ImpSimpl]
_ + _ (cmd_scope) [in ImpSimpl]
_ < _ (reset_scope) [in ImpSimpl]
_ = _ (reset_scope) [in ImpSimpl]
_ * _ (reset_scope) [in ImpSimpl]
_ - _ (reset_scope) [in ImpSimpl]
_ + _ (reset_scope) [in ImpSimpl]
_ $! _ [in ImpSimpl]
_ ==> _ [in Hoare]
when _ then _ else _ done [in ImpSimpl]
{{ _ }} while _ loop _ done [in ImpSimpl]
{{ _ }} _ {{ _ }} [in Hoare]

---

Library Index

H

Hoare

I

ImpSimpl

---

Constructor Index

A

Assign [in ImpSimpl]

C

Const [in ImpSimpl]

E

Equal [in ImpSimpl]
ExAssign [in ImpSimpl]
ExIfFalse [in ImpSimpl]
ExIfTrue [in ImpSimpl]
ExSeq [in ImpSimpl]
ExSkip [in ImpSimpl]
ExWhileFalse [in ImpSimpl]
ExWhileTrue [in ImpSimpl]

H

HtAssign [in Hoare]
HtConsequence [in Hoare]
HtExists [in Hoare]
HtIf [in Hoare]
HtSeq [in Hoare]
HtSkip [in Hoare]
HtWhileInv [in Hoare]

I

If_ [in ImpSimpl]

L

Less [in ImpSimpl]

M

Minus [in ImpSimpl]
Mult [in ImpSimpl]

P

Plus [in ImpSimpl]

S

Seq [in ImpSimpl]
Skip [in ImpSimpl]

V

Var [in ImpSimpl]

W

While_ [in ImpSimpl]

---

Lemma Index

C

completeness [in Hoare]

H

hoare_triple_sound [in Hoare]
hoare_triple_big_step_while [in Hoare]
HtStrengthenPost [in Hoare]
HtWeakenPre [in Hoare]

W

wpl_soundness_synt [in Hoare]
wpl_mon [in Hoare]
wpl_entailment' [in Hoare]
wpl_entailment [in Hoare]
wpl_complete_sem' [in Hoare]
wpl_complete_sem [in Hoare]
wpl_sound_sem [in Hoare]

---

Inductive Index

B

bexp [in ImpSimpl]

C

cmd [in ImpSimpl]

E

exec [in ImpSimpl]
exp [in ImpSimpl]

H

hoare_triple [in Hoare]

---

Definition Index

A

assertion [in Hoare]

B

beval [in ImpSimpl]

E

eval [in ImpSimpl]

H

himpl [in Hoare]
hoare_valid [in Hoare]
hoare_interp [in Hoare]

S

set [in ImpSimpl]

V

valuation [in ImpSimpl]
var [in ImpSimpl]

W

WeP [in Hoare]
wpl [in Hoare]

---

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

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

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

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

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

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

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

(11 entries)

---

This page has been generated by coqdoc