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

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

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

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

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

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

(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

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

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

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

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

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

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

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

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

(12 entries)

V

val [definition, in Top.test_extraction_malfunction]
val [definition, in Top.test_primarray_ffi]
Valid [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
value [inductive, in Malfunction.SemanticsSpec]
value_sind [definition, in Malfunction.SemanticsSpec]
value_rec [definition, in Malfunction.SemanticsSpec]
value_ind [definition, in Malfunction.SemanticsSpec]
value_rect [definition, in Malfunction.SemanticsSpec]
value_Int [constructor, in Malfunction.SemanticsSpec]
var [definition, in Malfunction.Malfunction]
Var [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
var [definition, in VerifiedExtraction.Benchmarks.lib.vs]
var_cspec [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
var0 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
var1 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
var2 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
vBlock [constructor, in Malfunction.Interpreter]
Vec [constructor, in Malfunction.SemanticsSpec]
vector_type_sind [definition, in Malfunction.Malfunction]
vector_type_rec [definition, in Malfunction.Malfunction]
vector_type_ind [definition, in Malfunction.Malfunction]
vector_type_rect [definition, in Malfunction.Malfunction]
vector_type [inductive, in Malfunction.Malfunction]
vector_type_to_string [definition, in Malfunction.Serialize]
vector_type_eqb [definition, in Malfunction.SemanticsSpec]
verified_named_erasure_pipeline_irrel [lemma, in Malfunction.Firstorder]
verified_malfunction_pipeline [definition, in Malfunction.Pipeline]
verified_named_erasure_pipeline [definition, in Malfunction.Pipeline]
verified_named_erasure_pipeline_inductive_irrel [lemma, in Malfunction.PipelineCorrect]
verified_malfunction_pipeline_wellformed [lemma, in Malfunction.PipelineCorrect]
verified_named_erasure_pipeline_eta_app [lemma, in Malfunction.PipelineCorrect]
verified_malfunction_pipeline_theorem [lemma, in Malfunction.PipelineCorrect]
verified_named_erasure_pipeline_lookup_env_in' [lemma, in Malfunction.PipelineCorrect]
verified_named_erasure_pipeline_fo [lemma, in Malfunction.PipelineCorrect]
verified_malfunction_pipeline_theorem_gen [lemma, in Malfunction.PipelineCorrect]
verified_malfunction_pipeline_compat [lemma, in Malfunction.PipelineCorrect]
verified_malfunction_pipeline_lookup [lemma, in Malfunction.PipelineCorrect]
verified_named_erasure_pipeline_lookup_env_in [lemma, in Malfunction.PipelineCorrect]
VeriStar [module, in VerifiedExtraction.Benchmarks.lib.vs]
VERISTAR [module, in VerifiedExtraction.Benchmarks.lib.vs]
veristar_result_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
veristar_result_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
veristar_result_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
veristar_result_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
veristar_result [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.Aborted [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.check_entailment [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VERISTAR.check_entailment [axiom, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.C_example [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.impl_pure_clause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.incorp [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.is_empty_clause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.naive_sublist [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.Ppred_decrease [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.pureb [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.pures [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.pure_clauses [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.RedundancyElim [section, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.RedundancyElim.A [variable, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.RedundancyElim.cmp [variable, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.relim1 [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.sublist [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.sublistg [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.Valid [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.veristar_result_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.veristar_result_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.veristar_result_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.veristar_result_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
VeriStar.veristar_result [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
vFail [constructor, in Malfunction.Interpreter]
vFloat [constructor, in Malfunction.Interpreter]
vFunc [constructor, in Malfunction.Interpreter]
vInt [constructor, in Malfunction.Interpreter]
vLazy [constructor, in Malfunction.Interpreter]
vNot_evaluated [constructor, in Malfunction.Interpreter]
vplus [definition, in Top.test_extract]
vplus [definition, in Top.Tests]
vplus0123 [definition, in Top.test_extract]
vplus0123 [definition, in Top.Tests]
vRClos [constructor, in Malfunction.Interpreter]
vrel [inductive, in Malfunction.Interpreter]
vrel_locals_add_self [lemma, in Malfunction.Interpreter]
vrel_add [lemma, in Malfunction.Interpreter]
vrel_locals [definition, in Malfunction.Interpreter]
vrel_sym [lemma, in Malfunction.Interpreter]
vrel_ind [lemma, in Malfunction.Interpreter]
vs [library]
vThunk [constructor, in Malfunction.Interpreter]
vVec [constructor, in Malfunction.Interpreter]
v01 [definition, in Top.test_extract]
v01 [definition, in Top.Tests]
v23 [definition, in Top.test_extract]
v23 [definition, in Top.Tests]

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

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

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

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

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

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

(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

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

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

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

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

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

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

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

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

(12 entries)