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

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

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

(17 entries)

Variable 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

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

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

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

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

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

(8 entries)

Instance 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

(16 entries)

Section 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

(9 entries)

Abbreviation 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)

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

(56 entries)

---

Global Index

A

AutosubstSsr [library]

B

Bot [definition, in Facts]
bot [definition, in Facts]

C

cap [definition, in Facts]
chain [definition, in Facts]
chain_maxr [lemma, in Facts]
chain_maxl [lemma, in Facts]
chain_le [lemma, in Facts]
Compiler [module, in Compiler]
Compiler [library]
Compiler.abort [definition, in Compiler]
Compiler.comp [definition, in Compiler]
Compiler.compile [abbreviation, in Compiler]
Compiler.compile_correct [lemma, in Compiler]
Compiler.compile_correct' [lemma, in Compiler]
Compiler.fix_weaken [lemma, in Compiler]
Compiler.flatmap [definition, in Compiler]
Compiler.flatmap_soundF [lemma, in Compiler]
Compiler.flatmap_soundT [lemma, in Compiler]
Compiler.flatmap_sound [lemma, in Compiler]
Compiler.Flatten [section, in Compiler]
Compiler.Flatten.f [variable, in Compiler]
Compiler.Flatten.Q [variable, in Compiler]
Compiler.Flatten.u [variable, in Compiler]
Compiler.Flatten.x [variable, in Compiler]
Compiler.GCSem [module, in Compiler]
Compiler.ICSem [module, in Compiler]
Compiler.LetDef [definition, in Compiler]
Compiler.simple [definition, in Compiler]
Compiler.wp_let [lemma, in Compiler]
continuous [definition, in Facts]
cup [definition, in Facts]

D

Definitions [section, in Facts]
Definitions.X [variable, in Facts]

E

EqState [module, in States]
EqState.state_eqType [definition, in States]
EqState.state_eqMixin [definition, in States]
EqState.to_testT [lemma, in States]
EqState.to_testP [axiom, in States]
EqState.to_test [axiom, in States]

F

Facts [library]
Fix [inductive, in Facts]
FixContinuity [section, in Facts]
FixContinuity.F [variable, in Facts]
FixContinuity.mono [variable, in Facts]
FixContinuity.X [variable, in Facts]
FixI [constructor, in Facts]
fixk [definition, in Facts]
fixk_unfold [lemma, in Facts]
fixk_fold [lemma, in Facts]
fixk_ind [lemma, in Facts]
Fixpoints [section, in Facts]
Fixpoints.F [variable, in Facts]
Fixpoints.G [variable, in Facts]
Fixpoints.X [variable, in Facts]
fix_continuous [lemma, in Facts]
fix_f_mono [lemma, in Facts]
fix_fixk [lemma, in Facts]
fix_ext [lemma, in Facts]
fix_unfold [lemma, in Facts]
fix_mono [lemma, in Facts]
fix_fold [lemma, in Facts]

G

GCContinuity [module, in GCContinuity]
GCContinuity [library]
GCContinuity.dijkstra_equiv [lemma, in GCContinuity]
GCContinuity.dijkstra_wpg [definition, in GCContinuity]
GCContinuity.GCSem [module, in GCContinuity]
GCContinuity.gc_continuous [lemma, in GCContinuity]
GCContinuity.gc_continuous' [lemma, in GCContinuity]
GCContinuity.wpG_continuous [lemma, in GCContinuity]
GCSemantics [module, in GCSemantics]
GCSemantics [library]
GCSemantics.GCSyn [module, in GCSemantics]
GCSemantics.gtest [definition, in GCSemantics]
GCSemantics.gtestP [lemma, in GCSemantics]
GCSemantics.gtest_contra [lemma, in GCSemantics]
GCSemantics.gtest_cons [lemma, in GCSemantics]
GCSemantics.wpG [abbreviation, in GCSemantics]
GCSemantics.wpg [definition, in GCSemantics]
GCSemantics.wpgG_wps [lemma, in GCSemantics]
GCSemantics.wpgG_mono [lemma, in GCSemantics]
GCSemantics.wpg_wps [lemma, in GCSemantics]
GCSemantics.wpG_mono [lemma, in GCSemantics]
GCSemantics.wpg_mono [lemma, in GCSemantics]
GCSemantics.wpG' [definition, in GCSemantics]
GCSemantics.wps [inductive, in GCSemantics]
GCSemantics.wps_wpg [lemma, in GCSemantics]
GCSemantics.wps_wpG [lemma, in GCSemantics]
GCSemantics.wps_loop_false [constructor, in GCSemantics]
GCSemantics.wps_loop_true [constructor, in GCSemantics]
GCSemantics.wps_case [constructor, in GCSemantics]
GCSemantics.wps_seq [constructor, in GCSemantics]
GCSemantics.wps_assn [constructor, in GCSemantics]
GCSemantics.wps_skip [constructor, in GCSemantics]
GCSyntax [module, in GCSyntax]
GCSyntax [library]
GCSyntax.all2 [definition, in GCSyntax]
GCSyntax.all2P [lemma, in GCSyntax]
GCSyntax.Assn [constructor, in GCSyntax]
GCSyntax.Case [constructor, in GCSyntax]
GCSyntax.cmd [inductive, in GCSyntax]
GCSyntax.CmdEqType [section, in GCSyntax]
GCSyntax.cmd_eqType [definition, in GCSyntax]
GCSyntax.cmd_eqMixin [definition, in GCSyntax]
GCSyntax.cmd_eqP [lemma, in GCSyntax]
GCSyntax.cmd_eq [definition, in GCSyntax]
GCSyntax.cmd_ind [definition, in GCSyntax]
GCSyntax.Do [constructor, in GCSyntax]
GCSyntax.gc [definition, in GCSyntax]
GCSyntax.GCInduction [section, in GCSyntax]
GCSyntax.GCInduction.P [variable, in GCSyntax]
GCSyntax.GCInduction.p_do [variable, in GCSyntax]
GCSyntax.GCInduction.p_case [variable, in GCSyntax]
GCSyntax.GCInduction.p_seq [variable, in GCSyntax]
GCSyntax.GCInduction.p_assn [variable, in GCSyntax]
GCSyntax.GCInduction.p_skip [variable, in GCSyntax]
GCSyntax.GCInduction.Q [variable, in GCSyntax]
GCSyntax.GCInduction.q_cons [variable, in GCSyntax]
GCSyntax.GCInduction.q_nil [variable, in GCSyntax]
GCSyntax.gc_ind [definition, in GCSyntax]
GCSyntax.gc_ind' [definition, in GCSyntax]
GCSyntax.injP [lemma, in GCSyntax]
GCSyntax.Seq [constructor, in GCSyntax]
GCSyntax.Skip [constructor, in GCSyntax]

I

ICContinuity [module, in ICContinuity]
ICContinuity [library]
ICContinuity.fix_step [definition, in ICContinuity]
ICContinuity.ICSem [module, in ICContinuity]
ICContinuity.wp_defn [lemma, in ICContinuity]
ICContinuity.wp_fix_kleene [lemma, in ICContinuity]
ICContinuity.wp_cons_continuous [lemma, in ICContinuity]
ICContinuity.wp_continuous [lemma, in ICContinuity]
ICEquivalence [module, in ICEquivalence]
ICEquivalence [library]
ICEquivalence.appc [definition, in ICEquivalence]
ICEquivalence.approximates [definition, in ICEquivalence]
ICEquivalence.approximatesI [lemma, in ICEquivalence]
ICEquivalence.approximates_refines [lemma, in ICEquivalence]
ICEquivalence.approximates_ss [lemma, in ICEquivalence]
ICEquivalence.approximates_compatible [lemma, in ICEquivalence]
ICEquivalence.approximates_consistent [lemma, in ICEquivalence]
ICEquivalence.approximation [definition, in ICEquivalence]
ICEquivalence.compatible [definition, in ICEquivalence]
ICEquivalence.consistent [definition, in ICEquivalence]
ICEquivalence.ctx [inductive, in ICEquivalence]
ICEquivalence.ctx_let [definition, in ICEquivalence]
ICEquivalence.ctx_def2 [constructor, in ICEquivalence]
ICEquivalence.ctx_def1 [constructor, in ICEquivalence]
ICEquivalence.ctx_if2 [constructor, in ICEquivalence]
ICEquivalence.ctx_if1 [constructor, in ICEquivalence]
ICEquivalence.ctx_act [constructor, in ICEquivalence]
ICEquivalence.ctx_hole [constructor, in ICEquivalence]
ICEquivalence.fill [definition, in ICEquivalence]
ICEquivalence.fill_fill [lemma, in ICEquivalence]
ICEquivalence.fix_n_fix [lemma, in ICEquivalence]
ICEquivalence.fix_nP [lemma, in ICEquivalence]
ICEquivalence.fix_n [definition, in ICEquivalence]
ICEquivalence.ICCont [module, in ICEquivalence]
ICEquivalence.least_upper_bound [lemma, in ICEquivalence]
ICEquivalence.let_ctxP [lemma, in ICEquivalence]
ICEquivalence.Omega [definition, in ICEquivalence]
ICEquivalence.point_terminatesD [lemma, in ICEquivalence]
ICEquivalence.point_terminatesI [lemma, in ICEquivalence]
ICEquivalence.point_wp [lemma, in ICEquivalence]
ICEquivalence.point_ctx [definition, in ICEquivalence]
ICEquivalence.pushn [definition, in ICEquivalence]
ICEquivalence.refines [definition, in ICEquivalence]
ICEquivalence.refines_approximates [lemma, in ICEquivalence]
ICEquivalence.refines_compatible [lemma, in ICEquivalence]
ICEquivalence.refines_consistent [lemma, in ICEquivalence]
ICEquivalence.refines_def [lemma, in ICEquivalence]
ICEquivalence.refines_if [lemma, in ICEquivalence]
ICEquivalence.refines_act [lemma, in ICEquivalence]
ICEquivalence.refines_trans [lemma, in ICEquivalence]
ICEquivalence.refines_refl [lemma, in ICEquivalence]
ICEquivalence.skip_wp [lemma, in ICEquivalence]
ICEquivalence.skip_ctxP [lemma, in ICEquivalence]
ICEquivalence.skip_ctx [definition, in ICEquivalence]
ICEquivalence.test_ctx [definition, in ICEquivalence]
ICEquivalence.wp_safe [lemma, in ICEquivalence]
_ <~ _ [notation, in ICEquivalence]
ICSemantics [module, in ICSemantics]
ICSemantics [library]
ICSemantics.coincidence [lemma, in ICSemantics]
ICSemantics.conf [definition, in ICSemantics]
ICSemantics.correspondence [lemma, in ICSemantics]
ICSemantics.eval [inductive, in ICSemantics]
ICSemantics.eval_terminates_id [lemma, in ICSemantics]
ICSemantics.eval_terminates [lemma, in ICSemantics]
ICSemantics.eval_wp [lemma, in ICSemantics]
ICSemantics.eval_def [constructor, in ICSemantics]
ICSemantics.eval_jump [constructor, in ICSemantics]
ICSemantics.eval_if_false [constructor, in ICSemantics]
ICSemantics.eval_if_true [constructor, in ICSemantics]
ICSemantics.eval_act [constructor, in ICSemantics]
ICSemantics.ICSyn [module, in ICSemantics]
ICSemantics.mstep [abbreviation, in ICSemantics]
ICSemantics.mstep_admissible [lemma, in ICSemantics]
ICSemantics.point_pred [definition, in ICSemantics]
ICSemantics.step [inductive, in ICSemantics]
ICSemantics.step_terminates [lemma, in ICSemantics]
ICSemantics.step_admissible [lemma, in ICSemantics]
ICSemantics.step_if_false [constructor, in ICSemantics]
ICSemantics.step_if_true [constructor, in ICSemantics]
ICSemantics.step_def [constructor, in ICSemantics]
ICSemantics.step_act [constructor, in ICSemantics]
ICSemantics.terminates [definition, in ICSemantics]
ICSemantics.wp [definition, in ICSemantics]
ICSemantics.wp_det [lemma, in ICSemantics]
ICSemantics.wp_terminates [lemma, in ICSemantics]
ICSemantics.wp_step_equiv [lemma, in ICSemantics]
ICSemantics.wp_subst [lemma, in ICSemantics]
ICSemantics.wp_weaken [lemma, in ICSemantics]
ICSemantics.wp_ren [lemma, in ICSemantics]
ICSemantics.wp_eval [lemma, in ICSemantics]
ICSemantics.wp_fix [lemma, in ICSemantics]
ICSemantics.wp_cons_mono [lemma, in ICSemantics]
ICSemantics.wp_equiv [lemma, in ICSemantics]
ICSemantics.wp_mono [lemma, in ICSemantics]
ICSyntax [module, in ICSyntax]
ICSyntax [library]
ICSyntax.Act [constructor, in ICSyntax]
ICSyntax.Def [constructor, in ICSyntax]
ICSyntax.Ids_term [instance, in ICSyntax]
ICSyntax.If [constructor, in ICSyntax]
ICSyntax.Jump [constructor, in ICSyntax]
ICSyntax.Rename_term [instance, in ICSyntax]
ICSyntax.SubstLemmas_term [instance, in ICSyntax]
ICSyntax.Subst_term [instance, in ICSyntax]
ICSyntax.term [inductive, in ICSyntax]

M

MMapExt_fun [instance, in AutosubstSsr]
mmapExt_seq [instance, in AutosubstSsr]
MMapExt_pair [instance, in AutosubstSsr]
MMapExt_option [instance, in AutosubstSsr]
MMapInstances [section, in AutosubstSsr]
MMapInstances.A [variable, in AutosubstSsr]
MMapInstances.B [variable, in AutosubstSsr]
MMapInstances.C [variable, in AutosubstSsr]
MMapInstances.MMapExt_A_C [variable, in AutosubstSsr]
MMapInstances.MMapExt_A_B [variable, in AutosubstSsr]
MMapInstances.MMapLemmas_A_C [variable, in AutosubstSsr]
MMapInstances.MMapLemmas_A_B [variable, in AutosubstSsr]
MMapInstances.MMap_A_C [variable, in AutosubstSsr]
MMapInstances.MMap_A_B [variable, in AutosubstSsr]
MMapLemmas_fun [instance, in AutosubstSsr]
mmapLemmas_seq [instance, in AutosubstSsr]
MMapLemmas_pair [instance, in AutosubstSsr]
MMapLemmas_option [instance, in AutosubstSsr]
MMap_fun [instance, in AutosubstSsr]
mmap_seq [instance, in AutosubstSsr]
MMap_pair [instance, in AutosubstSsr]
MMap_option [instance, in AutosubstSsr]
monotone [definition, in Facts]

N

NPred [definition, in Facts]

O

OmegaIteration [section, in Facts]
OmegaIteration.continuity [variable, in Facts]
OmegaIteration.F [variable, in Facts]
OmegaIteration.monotonicity [variable, in Facts]
OmegaIteration.X [variable, in Facts]

P

Pred [definition, in Facts]
PredT [definition, in Facts]

S

star [inductive, in Facts]
Star [section, in Facts]
starRS [lemma, in Facts]
starSR [constructor, in Facts]
starxx [constructor, in Facts]
star_trans [lemma, in Facts]
Star.R [variable, in Facts]
Star.X [variable, in Facts]
star1 [lemma, in Facts]
State [module, in States]
States [library]
State.action [axiom, in States]
State.actionE [axiom, in States]
State.action_eqType [definition, in States]
State.action_eqMixin [definition, in States]
State.action_eqP [axiom, in States]
State.action_eq [axiom, in States]
State.guard [axiom, in States]
State.guardE [axiom, in States]
State.guard_eqType [definition, in States]
State.guard_eqMixin [definition, in States]
State.guard_eqP [axiom, in States]
State.guard_eq [axiom, in States]
State.state [axiom, in States]
sup [definition, in Facts]

T

Top [definition, in Facts]
top [definition, in Facts]

other

_ <<= _ [notation, in Facts]

---

Notation Index

I

_ <~ _ [in ICEquivalence]

other

_ <<= _ [in Facts]

---

Module Index

C

Compiler [in Compiler]
Compiler.GCSem [in Compiler]
Compiler.ICSem [in Compiler]

E

EqState [in States]

G

GCContinuity [in GCContinuity]
GCContinuity.GCSem [in GCContinuity]
GCSemantics [in GCSemantics]
GCSemantics.GCSyn [in GCSemantics]
GCSyntax [in GCSyntax]

I

ICContinuity [in ICContinuity]
ICContinuity.ICSem [in ICContinuity]
ICEquivalence [in ICEquivalence]
ICEquivalence.ICCont [in ICEquivalence]
ICSemantics [in ICSemantics]
ICSemantics.ICSyn [in ICSemantics]
ICSyntax [in ICSyntax]

S

State [in States]

---

Variable Index

C

Compiler.Flatten.f [in Compiler]
Compiler.Flatten.Q [in Compiler]
Compiler.Flatten.u [in Compiler]
Compiler.Flatten.x [in Compiler]

D

Definitions.X [in Facts]

F

FixContinuity.F [in Facts]
FixContinuity.mono [in Facts]
FixContinuity.X [in Facts]
Fixpoints.F [in Facts]
Fixpoints.G [in Facts]
Fixpoints.X [in Facts]

G

GCSyntax.GCInduction.P [in GCSyntax]
GCSyntax.GCInduction.p_do [in GCSyntax]
GCSyntax.GCInduction.p_case [in GCSyntax]
GCSyntax.GCInduction.p_seq [in GCSyntax]
GCSyntax.GCInduction.p_assn [in GCSyntax]
GCSyntax.GCInduction.p_skip [in GCSyntax]
GCSyntax.GCInduction.Q [in GCSyntax]
GCSyntax.GCInduction.q_cons [in GCSyntax]
GCSyntax.GCInduction.q_nil [in GCSyntax]

M

MMapInstances.A [in AutosubstSsr]
MMapInstances.B [in AutosubstSsr]
MMapInstances.C [in AutosubstSsr]
MMapInstances.MMapExt_A_C [in AutosubstSsr]
MMapInstances.MMapExt_A_B [in AutosubstSsr]
MMapInstances.MMapLemmas_A_C [in AutosubstSsr]
MMapInstances.MMapLemmas_A_B [in AutosubstSsr]
MMapInstances.MMap_A_C [in AutosubstSsr]
MMapInstances.MMap_A_B [in AutosubstSsr]

O

OmegaIteration.continuity [in Facts]
OmegaIteration.F [in Facts]
OmegaIteration.monotonicity [in Facts]
OmegaIteration.X [in Facts]

S

Star.R [in Facts]
Star.X [in Facts]

---

Library Index

A

AutosubstSsr

C

Compiler

F

Facts

G

GCContinuity
GCSemantics
GCSyntax

I

ICContinuity
ICEquivalence
ICSemantics
ICSyntax

S

States

---

Lemma Index

C

chain_maxr [in Facts]
chain_maxl [in Facts]
chain_le [in Facts]
Compiler.compile_correct [in Compiler]
Compiler.compile_correct' [in Compiler]
Compiler.fix_weaken [in Compiler]
Compiler.flatmap_soundF [in Compiler]
Compiler.flatmap_soundT [in Compiler]
Compiler.flatmap_sound [in Compiler]
Compiler.wp_let [in Compiler]

E

EqState.to_testT [in States]

F

fixk_unfold [in Facts]
fixk_fold [in Facts]
fixk_ind [in Facts]
fix_continuous [in Facts]
fix_f_mono [in Facts]
fix_fixk [in Facts]
fix_ext [in Facts]
fix_unfold [in Facts]
fix_mono [in Facts]
fix_fold [in Facts]

G

GCContinuity.dijkstra_equiv [in GCContinuity]
GCContinuity.gc_continuous [in GCContinuity]
GCContinuity.gc_continuous' [in GCContinuity]
GCContinuity.wpG_continuous [in GCContinuity]
GCSemantics.gtestP [in GCSemantics]
GCSemantics.gtest_contra [in GCSemantics]
GCSemantics.gtest_cons [in GCSemantics]
GCSemantics.wpgG_wps [in GCSemantics]
GCSemantics.wpgG_mono [in GCSemantics]
GCSemantics.wpg_wps [in GCSemantics]
GCSemantics.wpG_mono [in GCSemantics]
GCSemantics.wpg_mono [in GCSemantics]
GCSemantics.wps_wpg [in GCSemantics]
GCSemantics.wps_wpG [in GCSemantics]
GCSyntax.all2P [in GCSyntax]
GCSyntax.cmd_eqP [in GCSyntax]
GCSyntax.injP [in GCSyntax]

I

ICContinuity.wp_defn [in ICContinuity]
ICContinuity.wp_fix_kleene [in ICContinuity]
ICContinuity.wp_cons_continuous [in ICContinuity]
ICContinuity.wp_continuous [in ICContinuity]
ICEquivalence.approximatesI [in ICEquivalence]
ICEquivalence.approximates_refines [in ICEquivalence]
ICEquivalence.approximates_ss [in ICEquivalence]
ICEquivalence.approximates_compatible [in ICEquivalence]
ICEquivalence.approximates_consistent [in ICEquivalence]
ICEquivalence.fill_fill [in ICEquivalence]
ICEquivalence.fix_n_fix [in ICEquivalence]
ICEquivalence.fix_nP [in ICEquivalence]
ICEquivalence.least_upper_bound [in ICEquivalence]
ICEquivalence.let_ctxP [in ICEquivalence]
ICEquivalence.point_terminatesD [in ICEquivalence]
ICEquivalence.point_terminatesI [in ICEquivalence]
ICEquivalence.point_wp [in ICEquivalence]
ICEquivalence.refines_approximates [in ICEquivalence]
ICEquivalence.refines_compatible [in ICEquivalence]
ICEquivalence.refines_consistent [in ICEquivalence]
ICEquivalence.refines_def [in ICEquivalence]
ICEquivalence.refines_if [in ICEquivalence]
ICEquivalence.refines_act [in ICEquivalence]
ICEquivalence.refines_trans [in ICEquivalence]
ICEquivalence.refines_refl [in ICEquivalence]
ICEquivalence.skip_wp [in ICEquivalence]
ICEquivalence.skip_ctxP [in ICEquivalence]
ICEquivalence.wp_safe [in ICEquivalence]
ICSemantics.coincidence [in ICSemantics]
ICSemantics.correspondence [in ICSemantics]
ICSemantics.eval_terminates_id [in ICSemantics]
ICSemantics.eval_terminates [in ICSemantics]
ICSemantics.eval_wp [in ICSemantics]
ICSemantics.mstep_admissible [in ICSemantics]
ICSemantics.step_terminates [in ICSemantics]
ICSemantics.step_admissible [in ICSemantics]
ICSemantics.wp_det [in ICSemantics]
ICSemantics.wp_terminates [in ICSemantics]
ICSemantics.wp_step_equiv [in ICSemantics]
ICSemantics.wp_subst [in ICSemantics]
ICSemantics.wp_weaken [in ICSemantics]
ICSemantics.wp_ren [in ICSemantics]
ICSemantics.wp_eval [in ICSemantics]
ICSemantics.wp_fix [in ICSemantics]
ICSemantics.wp_cons_mono [in ICSemantics]
ICSemantics.wp_equiv [in ICSemantics]
ICSemantics.wp_mono [in ICSemantics]

S

starRS [in Facts]
star_trans [in Facts]
star1 [in Facts]

---

Constructor Index

F

FixI [in Facts]

G

GCSemantics.wps_loop_false [in GCSemantics]
GCSemantics.wps_loop_true [in GCSemantics]
GCSemantics.wps_case [in GCSemantics]
GCSemantics.wps_seq [in GCSemantics]
GCSemantics.wps_assn [in GCSemantics]
GCSemantics.wps_skip [in GCSemantics]
GCSyntax.Assn [in GCSyntax]
GCSyntax.Case [in GCSyntax]
GCSyntax.Do [in GCSyntax]
GCSyntax.Seq [in GCSyntax]
GCSyntax.Skip [in GCSyntax]

I

ICEquivalence.ctx_def2 [in ICEquivalence]
ICEquivalence.ctx_def1 [in ICEquivalence]
ICEquivalence.ctx_if2 [in ICEquivalence]
ICEquivalence.ctx_if1 [in ICEquivalence]
ICEquivalence.ctx_act [in ICEquivalence]
ICEquivalence.ctx_hole [in ICEquivalence]
ICSemantics.eval_def [in ICSemantics]
ICSemantics.eval_jump [in ICSemantics]
ICSemantics.eval_if_false [in ICSemantics]
ICSemantics.eval_if_true [in ICSemantics]
ICSemantics.eval_act [in ICSemantics]
ICSemantics.step_if_false [in ICSemantics]
ICSemantics.step_if_true [in ICSemantics]
ICSemantics.step_def [in ICSemantics]
ICSemantics.step_act [in ICSemantics]
ICSyntax.Act [in ICSyntax]
ICSyntax.Def [in ICSyntax]
ICSyntax.If [in ICSyntax]
ICSyntax.Jump [in ICSyntax]

S

starSR [in Facts]
starxx [in Facts]

---

Axiom Index

E

EqState.to_testP [in States]
EqState.to_test [in States]

S

State.action [in States]
State.actionE [in States]
State.action_eqP [in States]
State.action_eq [in States]
State.guard [in States]
State.guardE [in States]
State.guard_eqP [in States]
State.guard_eq [in States]
State.state [in States]

---

Inductive Index

F

Fix [in Facts]

G

GCSemantics.wps [in GCSemantics]
GCSyntax.cmd [in GCSyntax]

I

ICEquivalence.ctx [in ICEquivalence]
ICSemantics.eval [in ICSemantics]
ICSemantics.step [in ICSemantics]
ICSyntax.term [in ICSyntax]

S

star [in Facts]

---

Instance Index

I

ICSyntax.Ids_term [in ICSyntax]
ICSyntax.Rename_term [in ICSyntax]
ICSyntax.SubstLemmas_term [in ICSyntax]
ICSyntax.Subst_term [in ICSyntax]

M

MMapExt_fun [in AutosubstSsr]
mmapExt_seq [in AutosubstSsr]
MMapExt_pair [in AutosubstSsr]
MMapExt_option [in AutosubstSsr]
MMapLemmas_fun [in AutosubstSsr]
mmapLemmas_seq [in AutosubstSsr]
MMapLemmas_pair [in AutosubstSsr]
MMapLemmas_option [in AutosubstSsr]
MMap_fun [in AutosubstSsr]
mmap_seq [in AutosubstSsr]
MMap_pair [in AutosubstSsr]
MMap_option [in AutosubstSsr]

---

Section Index

C

Compiler.Flatten [in Compiler]

D

Definitions [in Facts]

F

FixContinuity [in Facts]
Fixpoints [in Facts]

G

GCSyntax.CmdEqType [in GCSyntax]
GCSyntax.GCInduction [in GCSyntax]

M

MMapInstances [in AutosubstSsr]

O

OmegaIteration [in Facts]

S

Star [in Facts]

---

Abbreviation Index

C

Compiler.compile [in Compiler]

G

GCSemantics.wpG [in GCSemantics]

I

ICSemantics.mstep [in ICSemantics]

---

Definition Index

B

Bot [in Facts]
bot [in Facts]

C

cap [in Facts]
chain [in Facts]
Compiler.abort [in Compiler]
Compiler.comp [in Compiler]
Compiler.flatmap [in Compiler]
Compiler.LetDef [in Compiler]
Compiler.simple [in Compiler]
continuous [in Facts]
cup [in Facts]

E

EqState.state_eqType [in States]
EqState.state_eqMixin [in States]

F

fixk [in Facts]

G

GCContinuity.dijkstra_wpg [in GCContinuity]
GCSemantics.gtest [in GCSemantics]
GCSemantics.wpg [in GCSemantics]
GCSemantics.wpG' [in GCSemantics]
GCSyntax.all2 [in GCSyntax]
GCSyntax.cmd_eqType [in GCSyntax]
GCSyntax.cmd_eqMixin [in GCSyntax]
GCSyntax.cmd_eq [in GCSyntax]
GCSyntax.cmd_ind [in GCSyntax]
GCSyntax.gc [in GCSyntax]
GCSyntax.gc_ind [in GCSyntax]
GCSyntax.gc_ind' [in GCSyntax]

I

ICContinuity.fix_step [in ICContinuity]
ICEquivalence.appc [in ICEquivalence]
ICEquivalence.approximates [in ICEquivalence]
ICEquivalence.approximation [in ICEquivalence]
ICEquivalence.compatible [in ICEquivalence]
ICEquivalence.consistent [in ICEquivalence]
ICEquivalence.ctx_let [in ICEquivalence]
ICEquivalence.fill [in ICEquivalence]
ICEquivalence.fix_n [in ICEquivalence]
ICEquivalence.Omega [in ICEquivalence]
ICEquivalence.point_ctx [in ICEquivalence]
ICEquivalence.pushn [in ICEquivalence]
ICEquivalence.refines [in ICEquivalence]
ICEquivalence.skip_ctx [in ICEquivalence]
ICEquivalence.test_ctx [in ICEquivalence]
ICSemantics.conf [in ICSemantics]
ICSemantics.point_pred [in ICSemantics]
ICSemantics.terminates [in ICSemantics]
ICSemantics.wp [in ICSemantics]

M

monotone [in Facts]

N

NPred [in Facts]

P

Pred [in Facts]
PredT [in Facts]

S

State.action_eqType [in States]
State.action_eqMixin [in States]
State.guard_eqType [in States]
State.guard_eqMixin [in States]
sup [in Facts]

T

Top [in Facts]
top [in Facts]

---

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

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

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

(17 entries)

Variable 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

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

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

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

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

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

(8 entries)

Instance 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

(16 entries)

Section 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

(9 entries)

Abbreviation 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)

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

(56 entries)

---

This page has been generated by coqdoc