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)

---

M

M [module, in VerifiedExtraction.Benchmarks.lib.Color]
M [module, in VerifiedExtraction.Benchmarks.lib.vs]
main [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
main [definition, in VerifiedExtraction.Benchmarks.lib.Color]
main [definition, in VerifiedExtraction.Benchmarks.lib.vs]
main_easy [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
main_h [definition, in VerifiedExtraction.Benchmarks.lib.vs]
make_list [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
make_palette [definition, in VerifiedExtraction.Benchmarks.lib.Color]
Malfunction [library]
Malfunction_ind_env_empty [lemma, in Malfunction.Firstorder]
malfunction_pipeline [definition, in Malfunction.Pipeline]
malfunction_pipeline_config [record, in Malfunction.Pipeline]
malfunction_env_prop [definition, in Malfunction.CompileCorrect]
malfunction_pipeline_wellformed.Σ_t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.typing [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.expt [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.A [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.Normalisation [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.expΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.HΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.no_axioms [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.Σ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.HH [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed.HP [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_wellformed [section, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Haxiom_free [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Henvflags [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.compile_value_mf [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Σ_t' [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Σ_v [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.v_irred [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.v_red [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Σ_t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Normalisation [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.noParam [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.fo [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.typing [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.args [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.u [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.i [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.v [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.expt [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.expΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.HΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.no_axioms [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.Σ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.HH [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red.HP [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem_red [section, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.compile_value_mf [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Haxiom_free [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Henvflags [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Σ_t' [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Σ_v [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Heval [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Σ_t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.typing [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Normalisation [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.noParam [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.fo [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.args [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.u [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.i [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.v [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.expt [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.t [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.expΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.HΣ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.no_axioms [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.Σ [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.HH [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem.HP [variable, in Malfunction.PipelineCorrect]
malfunction_pipeline_theorem [section, in Malfunction.PipelineCorrect]
many_list_functions [definition, in Top.test_extract]
MapiInP [section, in Malfunction.Compile]
MapiInP.A [variable, in Malfunction.Compile]
MapiInP.B [variable, in Malfunction.Compile]
mapi_InP_spec [lemma, in Malfunction.Compile]
mapi_InP_spec' [lemma, in Malfunction.Compile]
mapi_InP [definition, in Malfunction.Compile]
Mapply [constructor, in Malfunction.Malfunction]
Mapply_u_eval [lemma, in Malfunction.CompileCorrect]
Mapply_eval_last [lemma, in Malfunction.CompileCorrect]
Mapply_eval_fail [lemma, in Malfunction.CompileCorrect]
Mapply_spec [lemma, in Malfunction.CompileCorrect]
Mapply_u_spec [lemma, in Malfunction.CompileCorrect]
Mapply_eval_rec [lemma, in Malfunction.CompileCorrect]
Mapply_eval [lemma, in Malfunction.CompileCorrect]
Mapply_u [definition, in Malfunction.Compile]
Mapply_ [definition, in Malfunction.Compile]
map_forall [definition, in Malfunction.Firstorder]
map_acc [definition, in Malfunction.utils_array]
max [definition, in VerifiedExtraction.Benchmarks.lib.vs]
maxs [definition, in VerifiedExtraction.Benchmarks.lib.vs]
max_to_Z [definition, in Top.test_extraction_malfunction]
max_expr_sind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
max_expr_ind [definition, in VerifiedExtraction.Benchmarks.lib.vs]
max_expr [inductive, in VerifiedExtraction.Benchmarks.lib.vs]
Mblock [constructor, in Malfunction.Malfunction]
Mcardinal_spec' [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
Mcase [definition, in Malfunction.Compile]
Mcase [library]
Mconvert [constructor, in Malfunction.Malfunction]
Mdomain [definition, in VerifiedExtraction.Benchmarks.lib.Color]
Melements_spec1 [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
mem_spec' [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
merge [definition, in VerifiedExtraction.Benchmarks.lib.Binom]
merge [definition, in append]
merge [definition, in VerifiedExtraction.Benchmarks.lib.vs]
mergeC [definition, in VerifiedExtraction.Benchmarks.lib.vs]
merge_sort_rec [definition, in append]
merge_sort_push [definition, in append]
merge_sort_pop [definition, in append]
mexpr_right [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
mexpr_left [constructor, in VerifiedExtraction.Benchmarks.lib.vs]
Mfield [constructor, in Malfunction.Malfunction]
Mforce [constructor, in Malfunction.Malfunction]
Mglobal [constructor, in Malfunction.Malfunction]
Mif [definition, in Malfunction.Deserialize]
minid [definition, in VerifiedExtraction.Benchmarks.lib.vs]
minid_eq [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
mkApps_irred [lemma, in Malfunction.Firstorder]
Mklambda [definition, in Malfunction.SemanticsSpec]
mkPureClause [definition, in VerifiedExtraction.Benchmarks.lib.vs]
mk_eta_exp [definition, in Malfunction.Serialize]
mk_graph [definition, in VerifiedExtraction.Benchmarks.lib.Color]
mk_pureR [definition, in VerifiedExtraction.Benchmarks.lib.vs]
mk_pureL [definition, in VerifiedExtraction.Benchmarks.lib.vs]
Mlambda [constructor, in Malfunction.Malfunction]
Mlambda_ [definition, in Malfunction.Compile]
Mlazy [constructor, in Malfunction.Malfunction]
Mlet [constructor, in Malfunction.Malfunction]
Mlet_ [definition, in Top.Tests]
Mnapply [definition, in Malfunction.Mcase]
Mnapply [definition, in Malfunction.CompileCorrect]
Mnapply_app [lemma, in Malfunction.Mcase]
Mnapply_app [lemma, in Malfunction.CompileCorrect]
Mnum [constructor, in Malfunction.Malfunction]
Mnumop1 [constructor, in Malfunction.Malfunction]
Mnumop2 [constructor, in Malfunction.Malfunction]
Mod [constructor, in Malfunction.Malfunction]
module [definition, in Malfunction.Malfunction]
Mremove_cardinal_less [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
Mremove_elements [lemma, in VerifiedExtraction.Benchmarks.lib.Color]
msg_true [definition, in Top.tutorial]
Mstring [constructor, in Malfunction.Malfunction]
Mswitch [constructor, in Malfunction.Malfunction]
Mul [constructor, in Malfunction.Malfunction]
multiple [library]
Mut [constructor, in Malfunction.Malfunction]
mutability [inductive, in Malfunction.Malfunction]
mutability_sind [definition, in Malfunction.Malfunction]
mutability_rec [definition, in Malfunction.Malfunction]
mutability_ind [definition, in Malfunction.Malfunction]
mutability_rect [definition, in Malfunction.Malfunction]
Mvar [constructor, in Malfunction.Malfunction]
Mvecget [constructor, in Malfunction.Malfunction]
Mveclen [constructor, in Malfunction.Malfunction]
Mvecnew [constructor, in Malfunction.Malfunction]
Mvecset [constructor, in Malfunction.Malfunction]
mygraph [definition, in VerifiedExtraction.Benchmarks.lib.Color]
myMain [definition, in VerifiedExtraction.Benchmarks.lib.vs]
myprod [record, in Top.test_extract]
M1 [module, in VerifiedExtraction.Benchmarks.lib.vs]
M1.mem_add_spec [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
M1.mem_add [definition, in VerifiedExtraction.Benchmarks.lib.vs]
M1.remove_min_spec2 [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
M1.remove_min_spec2x [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
M1.remove_min_spec1 [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
M1.remove_min_spec1x [lemma, in VerifiedExtraction.Benchmarks.lib.vs]
M1.remove_min [definition, in VerifiedExtraction.Benchmarks.lib.vs]

---

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