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)

---

E

E [module, in VerifiedExtraction.Benchmarks.lib.Color]
e [definition, in VerifiedExtraction.Benchmarks.lib.vs]
elemb [definition, in VerifiedExtraction.Benchmarks.lib.vs]
embed_binary_comparison [constructor, in Malfunction.Malfunction]
embed_binary_bitwise_op [constructor, in Malfunction.Malfunction]
embed_binary_arith_op [constructor, in Malfunction.Malfunction]
embed_inttype [constructor, in Malfunction.Malfunction]
empty [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
empty_heap [definition, in Malfunction.RealizabilitySemantics]
empty_set_elems' [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
empty_clause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
empty_locals [definition, in Malfunction.SemanticsSpec]
encode_name [definition, in Malfunction.Serialize]
end_to_end [library]
enforce_extraction_conditions [definition, in Malfunction.Pipeline]
Entailment [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
entailment [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
entailment_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
entailment_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
entailment_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
entailment_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
Eq [constructor, in Malfunction.Malfunction]
Equ [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
Eqv [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
eqv_eq_key_elt [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
eq_lt_trans [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
eq_var [definition, in VerifiedExtraction.Benchmarks.lib.vs]
eq_space_atomlist [definition, in VerifiedExtraction.Benchmarks.lib.vs]
eq_space_atom [definition, in VerifiedExtraction.Benchmarks.lib.vs]
eq_comp [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
Erased [constructor, in Malfunction.Malfunction]
erasure_config [projection, in Malfunction.Pipeline]
eval [inductive, in Malfunction.SemanticsSpec]
eval [section, in Malfunction.SemanticsSpec]
evalnamed [module, in Malfunction.PipelineCorrect]
evalnamed.eval_det [lemma, in Malfunction.PipelineCorrect]
eval_case_int [lemma, in Malfunction.Mcase]
eval_case_block [lemma, in Malfunction.Mcase]
eval_apply_lambda [lemma, in Malfunction.Mcase]
eval_app_ [lemma, in Malfunction.Mcase]
eval_app_nested_inv [lemma, in Malfunction.Mcase]
eval_app_nested_ [lemma, in Malfunction.Mcase]
eval_sim [lemma, in Malfunction.RealizabilitySemantics]
eval_det [lemma, in Malfunction.RealizabilitySemantics]
eval_num [lemma, in Malfunction.CompileCorrect]
eval_Mvar [lemma, in Malfunction.CompileCorrect]
eval_app_nested_inv [lemma, in Malfunction.CompileCorrect]
eval_app_nested_ [lemma, in Malfunction.CompileCorrect]
eval_malfunction_sexp [definition, in Top.Tests]
eval_malfunction [definition, in Top.Tests]
eval_correct [lemma, in Malfunction.Interpreter]
eval_fo [definition, in Malfunction.PipelineCorrect]
eval_ind [lemma, in Malfunction.SemanticsSpec]
eval_veclen [constructor, in Malfunction.SemanticsSpec]
eval_vecset [constructor, in Malfunction.SemanticsSpec]
eval_vecget [constructor, in Malfunction.SemanticsSpec]
eval_vecnew_bytevec [constructor, in Malfunction.SemanticsSpec]
eval_vecnew_array [constructor, in Malfunction.SemanticsSpec]
eval_convert_float_float [constructor, in Malfunction.SemanticsSpec]
eval_convert_float [constructor, in Malfunction.SemanticsSpec]
eval_convert_int [constructor, in Malfunction.SemanticsSpec]
eval_numop2_embed_float [constructor, in Malfunction.SemanticsSpec]
eval_numop2_float [constructor, in Malfunction.SemanticsSpec]
eval_numop2_float_fail [constructor, in Malfunction.SemanticsSpec]
eval_numop1_float_fail [constructor, in Malfunction.SemanticsSpec]
eval_numop1_neg [constructor, in Malfunction.SemanticsSpec]
eval_numop2 [constructor, in Malfunction.SemanticsSpec]
eval_numop1 [constructor, in Malfunction.SemanticsSpec]
eval_string [constructor, in Malfunction.SemanticsSpec]
eval_num_float [constructor, in Malfunction.SemanticsSpec]
eval_num_bigint [constructor, in Malfunction.SemanticsSpec]
eval_num_int [constructor, in Malfunction.SemanticsSpec]
eval_global [constructor, in Malfunction.SemanticsSpec]
eval_force_fail [constructor, in Malfunction.SemanticsSpec]
eval_force [constructor, in Malfunction.SemanticsSpec]
eval_force_done [constructor, in Malfunction.SemanticsSpec]
eval_thunk [constructor, in Malfunction.SemanticsSpec]
eval_field_fail [constructor, in Malfunction.SemanticsSpec]
eval_field [constructor, in Malfunction.SemanticsSpec]
eval_block [constructor, in Malfunction.SemanticsSpec]
eval_switch [constructor, in Malfunction.SemanticsSpec]
eval_let_rec [constructor, in Malfunction.SemanticsSpec]
eval_let_named [constructor, in Malfunction.SemanticsSpec]
eval_let_unnamed [constructor, in Malfunction.SemanticsSpec]
eval_let_body [constructor, in Malfunction.SemanticsSpec]
eval_var [constructor, in Malfunction.SemanticsSpec]
eval_app [constructor, in Malfunction.SemanticsSpec]
eval_app_fail [constructor, in Malfunction.SemanticsSpec]
eval_app_sing_rec [constructor, in Malfunction.SemanticsSpec]
eval_app_sing [constructor, in Malfunction.SemanticsSpec]
eval_lambda [constructor, in Malfunction.SemanticsSpec]
eval_lambda_sing [constructor, in Malfunction.SemanticsSpec]
eval.globals [variable, in Malfunction.SemanticsSpec]
eval._Heap [variable, in Malfunction.SemanticsSpec]
eval._Pointer [variable, in Malfunction.SemanticsSpec]
example_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
example_ent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
example1_myfail [definition, in VerifiedExtraction.Benchmarks.lib.vs]
example1_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
example2_myfail [definition, in VerifiedExtraction.Benchmarks.lib.vs]
example2_myent [definition, in VerifiedExtraction.Benchmarks.lib.vs]
existsb_ext [lemma, in Malfunction.Interpreter]
Existsi [inductive, in Malfunction.RealizabilitySemantics]
Existsi_spec [lemma, in Malfunction.RealizabilitySemantics]
Existsi_sind [definition, in Malfunction.RealizabilitySemantics]
Existsi_ind [definition, in Malfunction.RealizabilitySemantics]
Existsi_cons_tl [constructor, in Malfunction.RealizabilitySemantics]
Existsi_cons_hd [constructor, in Malfunction.RealizabilitySemantics]
exports [definition, in Malfunction.Serialize]
expr [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
expr_rewriteC [abbreviation, in VerifiedExtraction.Benchmarks.lib.vs]
expr_merge [abbreviation, in VerifiedExtraction.Benchmarks.lib.vs]
expr_get [abbreviation, in VerifiedExtraction.Benchmarks.lib.vs]
expr_geq [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_eq [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_lt [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_order [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_cmp_rfl [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
expr_cmp [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_rec [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
expr_rect [definition, in VerifiedExtraction.Benchmarks.lib.vs]
extensionality [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
extract [definition, in Top.Tests]
Extraction [library]
Extraction [library]
extraction_env_flags_mlf [definition, in Malfunction.Pipeline]
extraction_term_flags_mlf [definition, in Malfunction.Pipeline]
extraction_env_flags_mlf [definition, in Malfunction.CompileCorrect]
extract_names [definition, in Malfunction.Pipeline]
extract_names [definition, in Malfunction.PrintMli]
extract_def [definition, in Top.Tests]
extract_extraction [library]
ex_2 [definition, in VerifiedExtraction.Benchmarks.lib.Color]
ex_1 [definition, in VerifiedExtraction.Benchmarks.lib.Color]

---

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)

Generated by coqdoc and improved with CoqdocJS