Global Index

J

K

Q

Y

Z

_

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

_

(3 entries)

Module Index

A

C

E

F

G

H

I

J

K

L

M

P

Q

T

U

W

Y

Z

_

other

(20 entries)

Library Index

C

E

F

G

I

J

K

L

M

Q

T

U

W

X

Y

Z

_

other

(20 entries)

Lemma Index

A

F

G

J

K

L

O

Q

U

V

W

X

Y

Z

_

other

(64 entries)

Constructor Index

A

G

H

J

K

L

N

O

P

Q

T

X

Y

Z

_

other

(35 entries)

Axiom Index

A

C

D

E

F

I

J

K

L

M

P

Q

T

U

X

Y

Z

_

other

(97 entries)

Inductive Index

A

B

C

D

F

G

H

J

K

L

M

N

O

Q

S

T

U

W

X

Y

Z

_

other

(12 entries)

Projection Index

B

C

F

G

H

I

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(15 entries)

Instance Index

A

C

D

F

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

F

H

J

K

Q

U

V

X

Y

Z

_

other

(88 entries)

Record Index

A

B

C

D

F

G

H

I

J

K

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(7 entries)

Global Index

A

Abstraction [definition, in POCS.Spec.Abstraction]
abstraction [projection, in POCS.Spec.Abstraction]
Abstraction [library]
abstraction_compose [definition, in POCS.Spec.Abstraction]
addr [definition, in POCS.Helpers.Disk]
add_spec [definition, in POCS.Lab1.StatDbAPI]

B

BadBlockAPI [module, in POCS.Lab2.BadBlockAPI]
BadBlockAPI [library]
BadBlockAPI.abstr [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover_noop [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write_ok [axiom, in POCS.Lab2.BadBlockAPI]
BadBlockDisk [module, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.abstr [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover_noop [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write_ok [axiom, in POCS.Lab2.BadBlockImpl]
BadBlockImpl [library]
bappend [axiom, in POCS.Helpers.Disk]
BaseOp [constructor, in POCS.Spec.Proc]
baseOpT [axiom, in POCS.Spec.Proc]
base_step [axiom, in POCS.Spec.Proc]
Bind [constructor, in POCS.Spec.Proc]
block [definition, in POCS.Helpers.Disk]
blockbytes [definition, in POCS.Helpers.Disk]
block0 [definition, in POCS.Helpers.Disk]
block0_block1_differ [lemma, in POCS.Helpers.Disk]
block1 [definition, in POCS.Helpers.Disk]
bnull [definition, in POCS.Helpers.Disk]
bool_equal_dec [instance, in POCS.Helpers.Helpers]
bsplit [axiom, in POCS.Helpers.Disk]
bsplit_list [definition, in POCS.Helpers.Disk]
bsplit_bappend [axiom, in POCS.Helpers.Disk]
bytes [axiom, in POCS.Helpers.Disk]
bytes_differ [axiom, in POCS.Helpers.Disk]
bytes_dec [axiom, in POCS.Helpers.Disk]
bytes0 [axiom, in POCS.Helpers.Disk]
bytes1 [axiom, in POCS.Helpers.Disk]

C

cli [definition, in POCS.Lab1.StatDbCli]
clos_refl_trans_1n_unit_tuple [lemma, in POCS.Spec.Recovery]
compose_recovery [lemma, in POCS.Spec.Recovery]
Crashed [constructor, in POCS.Spec.Proc]

D

d [module, in POCS.Lab2.RemappedServer]
data [projection, in POCS.Common.NbdAPI]
data_len [projection, in POCS.Common.NbdAPI]
DeexTests [module, in POCS.Helpers.Helpers]
DeexTests.chooses_fresh_name [lemma, in POCS.Helpers.Helpers]
DeexTests.chooses_name [lemma, in POCS.Helpers.Helpers]
DestructMatchesTests [module, in POCS.Helpers.Helpers]
DestructMatchesTests.destructs_innermost_match [lemma, in POCS.Helpers.Helpers]
DestructMatchesTests.removes_absurdities [lemma, in POCS.Helpers.Helpers]
Disconnect [constructor, in POCS.Common.NbdAPI]
disk [definition, in POCS.Helpers.Disk]
Disk [library]
diskGet [definition, in POCS.Helpers.Disk]
diskShrink [definition, in POCS.Helpers.Disk]
diskShrink_diskUpd_notlast [lemma, in POCS.Helpers.Disk]
diskShrink_diskUpd_last [lemma, in POCS.Helpers.Disk]
diskShrink_preserves [lemma, in POCS.Helpers.Disk]
diskShrink_size [lemma, in POCS.Helpers.Disk]
diskSize [definition, in POCS.Helpers.Disk]
diskUpd [definition, in POCS.Helpers.Disk]
diskUpd_oob_noop [lemma, in POCS.Helpers.Disk]
diskUpd_twice [lemma, in POCS.Helpers.Disk]
diskUpd_same [lemma, in POCS.Helpers.Disk]
diskUpd_none [lemma, in POCS.Helpers.Disk]
diskUpd_neq [lemma, in POCS.Helpers.Disk]
diskUpd_oob_eq [lemma, in POCS.Helpers.Disk]
diskUpd_size [lemma, in POCS.Helpers.Disk]
diskUpd_eq [lemma, in POCS.Helpers.Disk]
diskUpd_eq_some [lemma, in POCS.Helpers.Disk]
disk_ext_inbounds_eq [lemma, in POCS.Helpers.Disk]
disk_ext_eq [lemma, in POCS.Helpers.Disk]
disk_oob_eq [lemma, in POCS.Helpers.Disk]
disk_none_oob [lemma, in POCS.Helpers.Disk]
disk_inbounds_not_none [lemma, in POCS.Helpers.Disk]
disk_inbounds_exists [lemma, in POCS.Helpers.Disk]

E

EInvalid [constructor, in POCS.Common.NbdAPI]
empty_disk [definition, in POCS.Helpers.Disk]
ENospc [constructor, in POCS.Common.NbdAPI]
EqualDec [record, in POCS.Helpers.Helpers]
EqualDec [inductive, in POCS.Helpers.Helpers]
equal_dec [projection, in POCS.Helpers.Helpers]
equal_dec [constructor, in POCS.Helpers.Helpers]
error [projection, in POCS.Common.NbdAPI]
ErrorCode [inductive, in POCS.Common.NbdAPI]
ESuccess [constructor, in POCS.Common.NbdAPI]
exec [inductive, in POCS.Spec.Proc]
ExecBindCrashed [constructor, in POCS.Spec.Proc]
ExecBindFinished [constructor, in POCS.Spec.Proc]
ExecCrashBegin [constructor, in POCS.Spec.Proc]
ExecCrashEnd [constructor, in POCS.Spec.Proc]
ExecOp [constructor, in POCS.Spec.Proc]
ExecRecoverCrashDuringRecovery [constructor, in POCS.Spec.Proc]
ExecRecoverExec [constructor, in POCS.Spec.Proc]
ExecRet [constructor, in POCS.Spec.Proc]
exec_recover [inductive, in POCS.Spec.Proc]
exec_recover_bind_inv [lemma, in POCS.Spec.ProcTheorems]
exec_equiv_equiv [instance, in POCS.Spec.ProcTheorems]
exec_equiv [definition, in POCS.Spec.ProcTheorems]
exec_ret [lemma, in POCS.Spec.ProcTheorems]

F

Finished [constructor, in POCS.Spec.Proc]
Flush [constructor, in POCS.Common.NbdAPI]

G

getBadBlock_spec [definition, in POCS.Lab2.BadBlockAPI]
getRequest_spec [definition, in POCS.Common.NbdAPI]
get_new_item [axiom, in POCS.Lab1.StatDbCli]

H

Handle [axiom, in POCS.Common.NbdAPI]
Helpers [library]
holds_some_inv_eq [lemma, in POCS.Helpers.Helpers]
holds_in_some_eq [lemma, in POCS.Helpers.Helpers]
holds_in_some [lemma, in POCS.Helpers.Helpers]
holds_in_none_eq [lemma, in POCS.Helpers.Helpers]

I

IdAbstraction [definition, in POCS.Spec.Abstraction]
idempotent [definition, in POCS.Spec.Recovery]
idempotent_loopspec [lemma, in POCS.Spec.Recovery]
init [definition, in POCS.Lab2.RemappedServer]
inited [definition, in POCS.Lab1.StatDbAPI]
inited [definition, in POCS.Common.NbdAPI]
inited_any [definition, in POCS.Spec.Abstraction]
InitFailed [constructor, in POCS.Spec.Abstraction]
Initialized [constructor, in POCS.Spec.Abstraction]
InitResult [inductive, in POCS.Spec.Abstraction]
init_abstraction_any_rec [lemma, in POCS.Spec.Abstraction]
init_abstraction [definition, in POCS.Spec.Abstraction]

L

LayerAbstraction [record, in POCS.Spec.Abstraction]
loop [definition, in POCS.Lab1.StatDbCli]

M

maybe_holds [definition, in POCS.Helpers.Helpers]
mean_spec [definition, in POCS.Lab1.StatDbAPI]
missing [definition, in POCS.Helpers.Helpers]
mkState [constructor, in POCS.Lab2.BadBlockAPI]
mkState [constructor, in POCS.Common.NbdAPI]
mkState [constructor, in POCS.Lab1.VariablesAPI]
monad_assoc [lemma, in POCS.Spec.ProcTheorems]
monad_left_id [lemma, in POCS.Spec.ProcTheorems]

N

nat_equal_dec [instance, in POCS.Helpers.Helpers]
nbd [module, in POCS.Common.NbdServer]
NbdAPI [module, in POCS.Common.NbdAPI]
NbdAPI [library]
NbdAPI.abstr [axiom, in POCS.Common.NbdAPI]
NbdAPI.getRequest [axiom, in POCS.Common.NbdAPI]
NbdAPI.getRequest_ok [axiom, in POCS.Common.NbdAPI]
NbdAPI.init [axiom, in POCS.Common.NbdAPI]
NbdAPI.init_ok [axiom, in POCS.Common.NbdAPI]
NbdAPI.recover [axiom, in POCS.Common.NbdAPI]
NbdAPI.recover_noop [axiom, in POCS.Common.NbdAPI]
NbdAPI.sendResponse [axiom, in POCS.Common.NbdAPI]
NbdAPI.sendResponse_ok [axiom, in POCS.Common.NbdAPI]
NbdImpl [module, in POCS.Common.NbdImpl]
NbdImpl [library]
NbdImpl.abstr [axiom, in POCS.Common.NbdImpl]
NbdImpl.getRequest [axiom, in POCS.Common.NbdImpl]
NbdImpl.getRequest_ok [axiom, in POCS.Common.NbdImpl]
NbdImpl.init [axiom, in POCS.Common.NbdImpl]
NbdImpl.init_ok [axiom, in POCS.Common.NbdImpl]
NbdImpl.recover [axiom, in POCS.Common.NbdImpl]
NbdImpl.recover_noop [axiom, in POCS.Common.NbdImpl]
NbdImpl.sendResponse [axiom, in POCS.Common.NbdImpl]
NbdImpl.sendResponse_ok [axiom, in POCS.Common.NbdImpl]
NBDServer [module, in POCS.Common.NbdServer]
NbdServer [library]
NBDServer.handle [definition, in POCS.Common.NbdServer]
NBDServer.init [definition, in POCS.Common.NbdServer]
NBDServer.read [definition, in POCS.Common.NbdServer]
NBDServer.read_ok [lemma, in POCS.Common.NbdServer]
NBDServer.serverLoop [definition, in POCS.Common.NbdServer]
NBDServer.size [definition, in POCS.Common.NbdServer]
NBDServer.write [definition, in POCS.Common.NbdServer]
NBDServer.write_ok [lemma, in POCS.Common.NbdServer]
no_crash [definition, in POCS.Spec.Recovery]
no_wipe [definition, in POCS.Spec.Recovery]

O

OneDiskAPI [module, in POCS.Common.OneDiskAPI]
OneDiskAPI [library]
OneDiskAPI.abstr [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.init [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.init_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.read [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.read_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.recover [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.recover_noop [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.size [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.size_ok [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.write [axiom, in POCS.Common.OneDiskAPI]
OneDiskAPI.write_ok [axiom, in POCS.Common.OneDiskAPI]
op_spec [definition, in POCS.Spec.Recovery]

P

POCS [library]
post [projection, in POCS.Spec.Abstraction]
post_step [definition, in POCS.Spec.Recovery]
pre [projection, in POCS.Spec.Abstraction]
pred_missing [lemma, in POCS.Helpers.Helpers]
pred_weaken [lemma, in POCS.Helpers.Helpers]
pre_step [definition, in POCS.Spec.Recovery]
proc [inductive, in POCS.Spec.Proc]
Proc [library]
ProcTheorems [library]
proc_loopspec [definition, in POCS.Spec.Recovery]
proc_spec_rx [lemma, in POCS.Spec.Abstraction]
proc_spec_weaken [lemma, in POCS.Spec.Abstraction]
proc_spec [definition, in POCS.Spec.Abstraction]

R

Read [constructor, in POCS.Common.NbdAPI]
read_spec [definition, in POCS.Lab2.BadBlockAPI]
read_spec [definition, in POCS.Common.OneDiskAPI]
read_match' [definition, in POCS.Common.NbdAPI]
read_match [definition, in POCS.Common.NbdAPI]
read_spec [definition, in POCS.Lab1.VariablesAPI]
Recovered [constructor, in POCS.Spec.Proc]
recovered [projection, in POCS.Spec.Abstraction]
Recovery [library]
rec_noop_compose [lemma, in POCS.Spec.Recovery]
rec_noop [definition, in POCS.Spec.Abstraction]
RemappedDisk [module, in POCS.Lab2.RemappedDiskImpl]
RemappedDiskImpl [library]
RemappedDisk.abstr [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_5_nok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_4_nok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_3_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_2_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_1_ok [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init' [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover_noop [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.RemappedAbstraction [constructor, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_noremap [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_remap [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction [inductive, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write [definition, in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write_ok [lemma, in POCS.Lab2.RemappedDiskImpl]
RemappedServer [library]
report_mean [axiom, in POCS.Lab1.StatDbCli]
Request [inductive, in POCS.Common.NbdAPI]
Response [record, in POCS.Common.NbdAPI]
Result [inductive, in POCS.Spec.Proc]
Ret [constructor, in POCS.Spec.Proc]
ret_spec [lemma, in POCS.Spec.Abstraction]
RExec [constructor, in POCS.Spec.Proc]
rexec [inductive, in POCS.Spec.Proc]
RExecCrash [constructor, in POCS.Spec.Proc]
rexec_finish_any_rec [lemma, in POCS.Spec.ProcTheorems]
rexec_equiv [lemma, in POCS.Spec.ProcTheorems]
RFinished [constructor, in POCS.Spec.Proc]
rhandle [projection, in POCS.Common.NbdAPI]
RResult [inductive, in POCS.Spec.Proc]

S

s [module, in POCS.Lab2.RemappedServer]
Semantics [definition, in POCS.Spec.Recovery]
sendResponse_spec [definition, in POCS.Common.NbdAPI]
serverLoop [definition, in POCS.Lab2.RemappedServer]
SimplMatchTests [module, in POCS.Helpers.Helpers]
SimplMatchTests.fails_on_hyp_if_match_not_removed [lemma, in POCS.Helpers.Helpers]
SimplMatchTests.fails_if_match_not_removed [lemma, in POCS.Helpers.Helpers]
SimplMatchTests.removes_match [lemma, in POCS.Helpers.Helpers]
size [definition, in POCS.Lab2.RemappedServer]
size_spec [definition, in POCS.Lab2.BadBlockAPI]
size_spec [definition, in POCS.Common.OneDiskAPI]
Spec [constructor, in POCS.Spec.Abstraction]
Specification [definition, in POCS.Spec.Abstraction]
SpecProps [record, in POCS.Spec.Abstraction]
spec_abstraction_compose [lemma, in POCS.Spec.Recovery]
spec_exec_equiv [lemma, in POCS.Spec.Abstraction]
spec_intros [lemma, in POCS.Spec.Abstraction]
spec_impl [definition, in POCS.Spec.Abstraction]
StatDB [module, in POCS.Lab1.StatDbImpl]
statdb [module, in POCS.Lab1.StatDbCli]
StatDbAPI [module, in POCS.Lab1.StatDbAPI]
StatDbAPI [library]
StatDbAPI.abstr [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.add [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.add_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.init [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.init_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.mean [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.mean_ok [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.recover [axiom, in POCS.Lab1.StatDbAPI]
StatDbAPI.recover_noop [axiom, in POCS.Lab1.StatDbAPI]
StatDbCli [library]
StatDBImpl [module, in POCS.Lab1.StatDbImpl]
StatDbImpl [library]
StatDB.abstr [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_3_ok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_2_nok [definition, in POCS.Lab1.StatDbImpl]
StatDB.abstr_1_ok [definition, in POCS.Lab1.StatDbImpl]
StatDB.add [definition, in POCS.Lab1.StatDbImpl]
StatDB.add_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.init [definition, in POCS.Lab1.StatDbImpl]
StatDB.init_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.init' [definition, in POCS.Lab1.StatDbImpl]
StatDB.mean [definition, in POCS.Lab1.StatDbImpl]
StatDB.mean_ok [lemma, in POCS.Lab1.StatDbImpl]
StatDB.recover [definition, in POCS.Lab1.StatDbImpl]
StatDB.recover_noop [lemma, in POCS.Lab1.StatDbImpl]
StatDB.statdb_abstraction [definition, in POCS.Lab1.StatDbImpl]
State [record, in POCS.Lab2.BadBlockAPI]
State [definition, in POCS.Lab1.StatDbAPI]
State [definition, in POCS.Common.OneDiskAPI]
State [record, in POCS.Common.NbdAPI]
State [record, in POCS.Lab1.VariablesAPI]
stateBadBlock [projection, in POCS.Lab2.BadBlockAPI]
StateCount [projection, in POCS.Lab1.VariablesAPI]
stateDisk [projection, in POCS.Lab2.BadBlockAPI]
StateDisk [projection, in POCS.Common.NbdAPI]
StateReq [projection, in POCS.Common.NbdAPI]
StateSum [projection, in POCS.Lab1.VariablesAPI]

T

then_init_compose [lemma, in POCS.Spec.Abstraction]
then_init [definition, in POCS.Spec.Abstraction]

U

UnknownOp [constructor, in POCS.Common.NbdAPI]

V

var [inductive, in POCS.Lab1.VariablesAPI]
VarCount [constructor, in POCS.Lab1.VariablesAPI]
VariablesAPI [library]
VariablesImpl [library]
Vars [module, in POCS.Lab1.VariablesImpl]
VarsAPI [module, in POCS.Lab1.VariablesAPI]
VarsAPI.abstr [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.init [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.init_ok [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.read [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.read_ok [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.recover [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.recover_noop [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.write [axiom, in POCS.Lab1.VariablesAPI]
VarsAPI.write_ok [axiom, in POCS.Lab1.VariablesAPI]
VarSum [constructor, in POCS.Lab1.VariablesAPI]
Vars.abstr [axiom, in POCS.Lab1.VariablesImpl]
Vars.init [axiom, in POCS.Lab1.VariablesImpl]
Vars.init_ok [axiom, in POCS.Lab1.VariablesImpl]
Vars.read [axiom, in POCS.Lab1.VariablesImpl]
Vars.read_ok [axiom, in POCS.Lab1.VariablesImpl]
Vars.recover [axiom, in POCS.Lab1.VariablesImpl]
Vars.recover_noop [axiom, in POCS.Lab1.VariablesImpl]
Vars.write [axiom, in POCS.Lab1.VariablesImpl]
Vars.write_ok [axiom, in POCS.Lab1.VariablesImpl]

W

wipe_req [definition, in POCS.Common.NbdAPI]
world [axiom, in POCS.Spec.Proc]
world_crash [axiom, in POCS.Spec.Proc]
Write [constructor, in POCS.Common.NbdAPI]
write_spec [definition, in POCS.Lab2.BadBlockAPI]
write_spec [definition, in POCS.Common.OneDiskAPI]
write_upd [definition, in POCS.Common.NbdAPI]
write_spec [definition, in POCS.Lab1.VariablesAPI]

X

x [module, in POCS.Lab2.RemappedDiskImpl]

other

_ <- _ ; _ [notation, in POCS.Spec.Proc]
_ ?|= _ [notation, in POCS.Helpers.Helpers]
_ == _ [notation, in POCS.Helpers.Helpers]

Notation Index

other

_ <- _ ; _ [in POCS.Spec.Proc]
_ ?|= _ [in POCS.Helpers.Helpers]
_ == _ [in POCS.Helpers.Helpers]

Module Index

B

BadBlockAPI [in POCS.Lab2.BadBlockAPI]
BadBlockDisk [in POCS.Lab2.BadBlockImpl]

D

d [in POCS.Lab2.RemappedServer]
DeexTests [in POCS.Helpers.Helpers]
DestructMatchesTests [in POCS.Helpers.Helpers]

N

nbd [in POCS.Common.NbdServer]
NbdAPI [in POCS.Common.NbdAPI]
NbdImpl [in POCS.Common.NbdImpl]
NBDServer [in POCS.Common.NbdServer]

O

OneDiskAPI [in POCS.Common.OneDiskAPI]

R

RemappedDisk [in POCS.Lab2.RemappedDiskImpl]

S

s [in POCS.Lab2.RemappedServer]
SimplMatchTests [in POCS.Helpers.Helpers]
StatDB [in POCS.Lab1.StatDbImpl]
statdb [in POCS.Lab1.StatDbCli]
StatDbAPI [in POCS.Lab1.StatDbAPI]
StatDBImpl [in POCS.Lab1.StatDbImpl]

V

Vars [in POCS.Lab1.VariablesImpl]
VarsAPI [in POCS.Lab1.VariablesAPI]

X

x [in POCS.Lab2.RemappedDiskImpl]

Library Index

A

B

BadBlockAPI
BadBlockImpl

D

Disk

H

N

NbdAPI
NbdImpl
NbdServer

O

P

POCS
Proc
ProcTheorems

R

Recovery
RemappedDiskImpl
RemappedServer

S

StatDbAPI
StatDbCli
StatDbImpl

V

VariablesAPI
VariablesImpl

Lemma Index

B

block0_block1_differ [in POCS.Helpers.Disk]

C

clos_refl_trans_1n_unit_tuple [in POCS.Spec.Recovery]
compose_recovery [in POCS.Spec.Recovery]

D

DeexTests.chooses_fresh_name [in POCS.Helpers.Helpers]
DeexTests.chooses_name [in POCS.Helpers.Helpers]
DestructMatchesTests.destructs_innermost_match [in POCS.Helpers.Helpers]
DestructMatchesTests.removes_absurdities [in POCS.Helpers.Helpers]
diskShrink_diskUpd_notlast [in POCS.Helpers.Disk]
diskShrink_diskUpd_last [in POCS.Helpers.Disk]
diskShrink_preserves [in POCS.Helpers.Disk]
diskShrink_size [in POCS.Helpers.Disk]
diskUpd_oob_noop [in POCS.Helpers.Disk]
diskUpd_twice [in POCS.Helpers.Disk]
diskUpd_same [in POCS.Helpers.Disk]
diskUpd_none [in POCS.Helpers.Disk]
diskUpd_neq [in POCS.Helpers.Disk]
diskUpd_oob_eq [in POCS.Helpers.Disk]
diskUpd_size [in POCS.Helpers.Disk]
diskUpd_eq [in POCS.Helpers.Disk]
diskUpd_eq_some [in POCS.Helpers.Disk]
disk_ext_inbounds_eq [in POCS.Helpers.Disk]
disk_ext_eq [in POCS.Helpers.Disk]
disk_oob_eq [in POCS.Helpers.Disk]
disk_none_oob [in POCS.Helpers.Disk]
disk_inbounds_not_none [in POCS.Helpers.Disk]
disk_inbounds_exists [in POCS.Helpers.Disk]

E

exec_recover_bind_inv [in POCS.Spec.ProcTheorems]
exec_ret [in POCS.Spec.ProcTheorems]

H

holds_some_inv_eq [in POCS.Helpers.Helpers]
holds_in_some_eq [in POCS.Helpers.Helpers]
holds_in_some [in POCS.Helpers.Helpers]
holds_in_none_eq [in POCS.Helpers.Helpers]

I

idempotent_loopspec [in POCS.Spec.Recovery]
init_abstraction_any_rec [in POCS.Spec.Abstraction]

M

monad_assoc [in POCS.Spec.ProcTheorems]
monad_left_id [in POCS.Spec.ProcTheorems]

N

NBDServer.read_ok [in POCS.Common.NbdServer]
NBDServer.write_ok [in POCS.Common.NbdServer]

P

pred_missing [in POCS.Helpers.Helpers]
pred_weaken [in POCS.Helpers.Helpers]
proc_spec_rx [in POCS.Spec.Abstraction]
proc_spec_weaken [in POCS.Spec.Abstraction]

R

rec_noop_compose [in POCS.Spec.Recovery]
RemappedDisk.init_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover_noop [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_noremap [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.remapped_abstraction_diskUpd_remap [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write_ok [in POCS.Lab2.RemappedDiskImpl]
ret_spec [in POCS.Spec.Abstraction]
rexec_finish_any_rec [in POCS.Spec.ProcTheorems]
rexec_equiv [in POCS.Spec.ProcTheorems]

S

SimplMatchTests.fails_on_hyp_if_match_not_removed [in POCS.Helpers.Helpers]
SimplMatchTests.fails_if_match_not_removed [in POCS.Helpers.Helpers]
SimplMatchTests.removes_match [in POCS.Helpers.Helpers]
spec_abstraction_compose [in POCS.Spec.Recovery]
spec_exec_equiv [in POCS.Spec.Abstraction]
spec_intros [in POCS.Spec.Abstraction]
StatDB.add_ok [in POCS.Lab1.StatDbImpl]
StatDB.init_ok [in POCS.Lab1.StatDbImpl]
StatDB.mean_ok [in POCS.Lab1.StatDbImpl]
StatDB.recover_noop [in POCS.Lab1.StatDbImpl]

T

then_init_compose [in POCS.Spec.Abstraction]

Constructor Index

B

BaseOp [in POCS.Spec.Proc]
Bind [in POCS.Spec.Proc]

C

Crashed [in POCS.Spec.Proc]

D

Disconnect [in POCS.Common.NbdAPI]

E

EInvalid [in POCS.Common.NbdAPI]
ENospc [in POCS.Common.NbdAPI]
equal_dec [in POCS.Helpers.Helpers]
ESuccess [in POCS.Common.NbdAPI]
ExecBindCrashed [in POCS.Spec.Proc]
ExecBindFinished [in POCS.Spec.Proc]
ExecCrashBegin [in POCS.Spec.Proc]
ExecCrashEnd [in POCS.Spec.Proc]
ExecOp [in POCS.Spec.Proc]
ExecRecoverCrashDuringRecovery [in POCS.Spec.Proc]
ExecRecoverExec [in POCS.Spec.Proc]
ExecRet [in POCS.Spec.Proc]

F

Finished [in POCS.Spec.Proc]
Flush [in POCS.Common.NbdAPI]

I

InitFailed [in POCS.Spec.Abstraction]
Initialized [in POCS.Spec.Abstraction]

M

mkState [in POCS.Lab2.BadBlockAPI]
mkState [in POCS.Common.NbdAPI]
mkState [in POCS.Lab1.VariablesAPI]

R

Read [in POCS.Common.NbdAPI]
Recovered [in POCS.Spec.Proc]
RemappedDisk.RemappedAbstraction [in POCS.Lab2.RemappedDiskImpl]
Ret [in POCS.Spec.Proc]
RExec [in POCS.Spec.Proc]
RExecCrash [in POCS.Spec.Proc]
RFinished [in POCS.Spec.Proc]

S

Spec [in POCS.Spec.Abstraction]

U

UnknownOp [in POCS.Common.NbdAPI]

V

VarCount [in POCS.Lab1.VariablesAPI]
VarSum [in POCS.Lab1.VariablesAPI]

W

Write [in POCS.Common.NbdAPI]

Axiom Index

B

BadBlockAPI.abstr [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.getBadBlock_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.init_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.read_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.recover_noop [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.size_ok [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write [in POCS.Lab2.BadBlockAPI]
BadBlockAPI.write_ok [in POCS.Lab2.BadBlockAPI]
BadBlockDisk.abstr [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.getBadBlock_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.init_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.read_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.recover_noop [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.size_ok [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write [in POCS.Lab2.BadBlockImpl]
BadBlockDisk.write_ok [in POCS.Lab2.BadBlockImpl]
bappend [in POCS.Helpers.Disk]
baseOpT [in POCS.Spec.Proc]
base_step [in POCS.Spec.Proc]
bsplit [in POCS.Helpers.Disk]
bsplit_bappend [in POCS.Helpers.Disk]
bytes [in POCS.Helpers.Disk]
bytes_differ [in POCS.Helpers.Disk]
bytes_dec [in POCS.Helpers.Disk]
bytes0 [in POCS.Helpers.Disk]
bytes1 [in POCS.Helpers.Disk]

G

get_new_item [in POCS.Lab1.StatDbCli]

H

Handle [in POCS.Common.NbdAPI]

N

NbdAPI.abstr [in POCS.Common.NbdAPI]
NbdAPI.getRequest [in POCS.Common.NbdAPI]
NbdAPI.getRequest_ok [in POCS.Common.NbdAPI]
NbdAPI.init [in POCS.Common.NbdAPI]
NbdAPI.init_ok [in POCS.Common.NbdAPI]
NbdAPI.recover [in POCS.Common.NbdAPI]
NbdAPI.recover_noop [in POCS.Common.NbdAPI]
NbdAPI.sendResponse [in POCS.Common.NbdAPI]
NbdAPI.sendResponse_ok [in POCS.Common.NbdAPI]
NbdImpl.abstr [in POCS.Common.NbdImpl]
NbdImpl.getRequest [in POCS.Common.NbdImpl]
NbdImpl.getRequest_ok [in POCS.Common.NbdImpl]
NbdImpl.init [in POCS.Common.NbdImpl]
NbdImpl.init_ok [in POCS.Common.NbdImpl]
NbdImpl.recover [in POCS.Common.NbdImpl]
NbdImpl.recover_noop [in POCS.Common.NbdImpl]
NbdImpl.sendResponse [in POCS.Common.NbdImpl]
NbdImpl.sendResponse_ok [in POCS.Common.NbdImpl]

O

OneDiskAPI.abstr [in POCS.Common.OneDiskAPI]
OneDiskAPI.init [in POCS.Common.OneDiskAPI]
OneDiskAPI.init_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.read [in POCS.Common.OneDiskAPI]
OneDiskAPI.read_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.recover [in POCS.Common.OneDiskAPI]
OneDiskAPI.recover_noop [in POCS.Common.OneDiskAPI]
OneDiskAPI.size [in POCS.Common.OneDiskAPI]
OneDiskAPI.size_ok [in POCS.Common.OneDiskAPI]
OneDiskAPI.write [in POCS.Common.OneDiskAPI]
OneDiskAPI.write_ok [in POCS.Common.OneDiskAPI]

R

report_mean [in POCS.Lab1.StatDbCli]

S

StatDbAPI.abstr [in POCS.Lab1.StatDbAPI]
StatDbAPI.add [in POCS.Lab1.StatDbAPI]
StatDbAPI.add_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.init [in POCS.Lab1.StatDbAPI]
StatDbAPI.init_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.mean [in POCS.Lab1.StatDbAPI]
StatDbAPI.mean_ok [in POCS.Lab1.StatDbAPI]
StatDbAPI.recover [in POCS.Lab1.StatDbAPI]
StatDbAPI.recover_noop [in POCS.Lab1.StatDbAPI]

V

VarsAPI.abstr [in POCS.Lab1.VariablesAPI]
VarsAPI.init [in POCS.Lab1.VariablesAPI]
VarsAPI.init_ok [in POCS.Lab1.VariablesAPI]
VarsAPI.read [in POCS.Lab1.VariablesAPI]
VarsAPI.read_ok [in POCS.Lab1.VariablesAPI]
VarsAPI.recover [in POCS.Lab1.VariablesAPI]
VarsAPI.recover_noop [in POCS.Lab1.VariablesAPI]
VarsAPI.write [in POCS.Lab1.VariablesAPI]
VarsAPI.write_ok [in POCS.Lab1.VariablesAPI]
Vars.abstr [in POCS.Lab1.VariablesImpl]
Vars.init [in POCS.Lab1.VariablesImpl]
Vars.init_ok [in POCS.Lab1.VariablesImpl]
Vars.read [in POCS.Lab1.VariablesImpl]
Vars.read_ok [in POCS.Lab1.VariablesImpl]
Vars.recover [in POCS.Lab1.VariablesImpl]
Vars.recover_noop [in POCS.Lab1.VariablesImpl]
Vars.write [in POCS.Lab1.VariablesImpl]
Vars.write_ok [in POCS.Lab1.VariablesImpl]

W

world [in POCS.Spec.Proc]
world_crash [in POCS.Spec.Proc]

Inductive Index

E

EqualDec [in POCS.Helpers.Helpers]
ErrorCode [in POCS.Common.NbdAPI]
exec [in POCS.Spec.Proc]
exec_recover [in POCS.Spec.Proc]

I

InitResult [in POCS.Spec.Abstraction]

P

proc [in POCS.Spec.Proc]

R

RemappedDisk.remapped_abstraction [in POCS.Lab2.RemappedDiskImpl]
Request [in POCS.Common.NbdAPI]
Result [in POCS.Spec.Proc]
rexec [in POCS.Spec.Proc]
RResult [in POCS.Spec.Proc]

V

var [in POCS.Lab1.VariablesAPI]

Projection Index

A

abstraction [in POCS.Spec.Abstraction]

D

data [in POCS.Common.NbdAPI]
data_len [in POCS.Common.NbdAPI]

E

equal_dec [in POCS.Helpers.Helpers]
error [in POCS.Common.NbdAPI]

P

post [in POCS.Spec.Abstraction]
pre [in POCS.Spec.Abstraction]

R

recovered [in POCS.Spec.Abstraction]
rhandle [in POCS.Common.NbdAPI]

S

stateBadBlock [in POCS.Lab2.BadBlockAPI]
StateCount [in POCS.Lab1.VariablesAPI]
stateDisk [in POCS.Lab2.BadBlockAPI]
StateDisk [in POCS.Common.NbdAPI]
StateReq [in POCS.Common.NbdAPI]
StateSum [in POCS.Lab1.VariablesAPI]

Instance Index

B

bool_equal_dec [in POCS.Helpers.Helpers]

E

exec_equiv_equiv [in POCS.Spec.ProcTheorems]

N

nat_equal_dec [in POCS.Helpers.Helpers]

Definition Index

A

Abstraction [in POCS.Spec.Abstraction]
abstraction_compose [in POCS.Spec.Abstraction]
addr [in POCS.Helpers.Disk]
add_spec [in POCS.Lab1.StatDbAPI]

B

block [in POCS.Helpers.Disk]
blockbytes [in POCS.Helpers.Disk]
block0 [in POCS.Helpers.Disk]
block1 [in POCS.Helpers.Disk]
bnull [in POCS.Helpers.Disk]
bsplit_list [in POCS.Helpers.Disk]

C

cli [in POCS.Lab1.StatDbCli]

D

disk [in POCS.Helpers.Disk]
diskGet [in POCS.Helpers.Disk]
diskShrink [in POCS.Helpers.Disk]
diskSize [in POCS.Helpers.Disk]
diskUpd [in POCS.Helpers.Disk]

E

empty_disk [in POCS.Helpers.Disk]
exec_equiv [in POCS.Spec.ProcTheorems]

G

getBadBlock_spec [in POCS.Lab2.BadBlockAPI]
getRequest_spec [in POCS.Common.NbdAPI]

I

IdAbstraction [in POCS.Spec.Abstraction]
idempotent [in POCS.Spec.Recovery]
init [in POCS.Lab2.RemappedServer]
inited [in POCS.Lab1.StatDbAPI]
inited [in POCS.Common.NbdAPI]
inited_any [in POCS.Spec.Abstraction]
init_abstraction [in POCS.Spec.Abstraction]

L

loop [in POCS.Lab1.StatDbCli]

M

maybe_holds [in POCS.Helpers.Helpers]
mean_spec [in POCS.Lab1.StatDbAPI]
missing [in POCS.Helpers.Helpers]

N

NBDServer.handle [in POCS.Common.NbdServer]
NBDServer.init [in POCS.Common.NbdServer]
NBDServer.read [in POCS.Common.NbdServer]
NBDServer.serverLoop [in POCS.Common.NbdServer]
NBDServer.size [in POCS.Common.NbdServer]
NBDServer.write [in POCS.Common.NbdServer]
no_crash [in POCS.Spec.Recovery]
no_wipe [in POCS.Spec.Recovery]

O

op_spec [in POCS.Spec.Recovery]

P

post_step [in POCS.Spec.Recovery]
pre_step [in POCS.Spec.Recovery]
proc_loopspec [in POCS.Spec.Recovery]
proc_spec [in POCS.Spec.Abstraction]

R

read_spec [in POCS.Lab2.BadBlockAPI]
read_spec [in POCS.Common.OneDiskAPI]
read_match' [in POCS.Common.NbdAPI]
read_match [in POCS.Common.NbdAPI]
read_spec [in POCS.Lab1.VariablesAPI]
rec_noop [in POCS.Spec.Abstraction]
RemappedDisk.abstr [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_5_nok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_4_nok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_3_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_2_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.abst_1_ok [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.init' [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.read [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.recover [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.size [in POCS.Lab2.RemappedDiskImpl]
RemappedDisk.write [in POCS.Lab2.RemappedDiskImpl]

S

Semantics [in POCS.Spec.Recovery]
sendResponse_spec [in POCS.Common.NbdAPI]
serverLoop [in POCS.Lab2.RemappedServer]
size [in POCS.Lab2.RemappedServer]
size_spec [in POCS.Lab2.BadBlockAPI]
size_spec [in POCS.Common.OneDiskAPI]
Specification [in POCS.Spec.Abstraction]
spec_impl [in POCS.Spec.Abstraction]
StatDB.abstr [in POCS.Lab1.StatDbImpl]
StatDB.abstr_3_ok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_2_nok [in POCS.Lab1.StatDbImpl]
StatDB.abstr_1_ok [in POCS.Lab1.StatDbImpl]
StatDB.add [in POCS.Lab1.StatDbImpl]
StatDB.init [in POCS.Lab1.StatDbImpl]
StatDB.init' [in POCS.Lab1.StatDbImpl]
StatDB.mean [in POCS.Lab1.StatDbImpl]
StatDB.recover [in POCS.Lab1.StatDbImpl]
StatDB.statdb_abstraction [in POCS.Lab1.StatDbImpl]
State [in POCS.Lab1.StatDbAPI]
State [in POCS.Common.OneDiskAPI]

T

then_init [in POCS.Spec.Abstraction]

W

wipe_req [in POCS.Common.NbdAPI]
write_spec [in POCS.Lab2.BadBlockAPI]
write_spec [in POCS.Common.OneDiskAPI]
write_upd [in POCS.Common.NbdAPI]
write_spec [in POCS.Lab1.VariablesAPI]

Record Index

E

EqualDec [in POCS.Helpers.Helpers]

L

LayerAbstraction [in POCS.Spec.Abstraction]

R

Response [in POCS.Common.NbdAPI]

S

SpecProps [in POCS.Spec.Abstraction]
State [in POCS.Lab2.BadBlockAPI]
State [in POCS.Common.NbdAPI]
State [in POCS.Lab1.VariablesAPI]

Global Index

J

K

Q

Y

Z

_

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

_

(3 entries)

Module Index

A

C

E

F

G

H

I

J

K

L

M

P

Q

T

U

W

Y

Z

_

other

(20 entries)

Library Index

C

E

F

G

I

J

K

L

M

Q

T

U

W

X

Y

Z

_

other

(20 entries)

Lemma Index

A

F

G

J

K

L

O

Q

U

V

W

X

Y

Z

_

other

(64 entries)

Constructor Index

A

G

H

J

K

L

N

O

P

Q

T

X

Y

Z

_

other

(35 entries)

Axiom Index

A

C

D

E

F

I

J

K

L

M

P

Q

T

U

X

Y

Z

_

other

(97 entries)

Inductive Index

A

B

C

D

F

G

H

J

K

L

M

N

O

Q

S

T

U

W

X

Y

Z

_

other

(12 entries)

Projection Index

B

C

F

G

H

I

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(15 entries)

Instance Index

A

C

D

F

G

H

I

J

K

L

M

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Definition Index

F

H

J

K

Q

U

V

X

Y

Z

_

other

(88 entries)

Record Index

A

B

C

D

F

G

H

I

J

K

M

N

O

P

Q

T

U

V

W

X

Y

Z

_

other

(7 entries)

This page has been generated by coqdoc