Global Index

B

F

H

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(69 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)

Variable Index

A

B

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Library Index

B

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(20 entries)

Constructor Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Section Index

A

B

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Instance Index

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)

Definition Index

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(28 entries)

Global Index

A

abort_ast_decidable [instance, in AnalysersSign]
abort_ares_decidable [instance, in AnalysersSign]
AbstractSign [library]
Analysers [library]
AnalysersSign [library]
analyser_match [definition, in AnalysersSign]

C

ConcreteWhile [library]

D

DomainsSign [library]

E

eq_aValVar [definition, in AnalysersSign]

G

General [section, in AnalysersSign]
General.analyser_correct [variable, in AnalysersSign]
General.analyser_result [variable, in AnalysersSign]
General.correct_analyser_result [variable, in AnalysersSign]
General.Typed [section, in AnalysersSign]

I

is_looping_branch_Decidable [instance, in AnalysersSign]
is_looping_branch_call [constructor, in AnalysersSign]
is_looping_branch_while [constructor, in AnalysersSign]
is_looping_branch [inductive, in AnalysersSign]

P

PrettyBigStep [library]

S

sign_analyse_oracle_back_and_forth_deep_loop_correct [lemma, in AnalysersSign]
sign_analyse_oracle_back_and_forth_deep_loop [definition, in AnalysersSign]
sign_analyse_oracle_back_and_forth_deep_correct [lemma, in AnalysersSign]
sign_analyse_oracle_back_and_forth_deep [definition, in AnalysersSign]
sign_analyse_oracle_back_and_forth_loop_correct [lemma, in AnalysersSign]
sign_analyse_oracle_back_and_forth_loop [definition, in AnalysersSign]
sign_analyse_oracle_back_and_forth_correct [lemma, in AnalysersSign]
sign_analyse_oracle_back_and_forth [definition, in AnalysersSign]
sign_analyse_deep_fuel_type_correct [lemma, in AnalysersSign]
sign_analyse_deep_fuel_type [definition, in AnalysersSign]
sign_analyse_deep_fuel_fail_correct [lemma, in AnalysersSign]
sign_analyse_deep_fuel_fail [definition, in AnalysersSign]
sign_analyse_fuel_type_correct [lemma, in AnalysersSign]
sign_analyse_fuel_type [definition, in AnalysersSign]
sign_analyse_fuel_fail_correct [lemma, in AnalysersSign]
sign_analyse_fuel_fail [definition, in AnalysersSign]
sign_type_analyse_correct [lemma, in AnalysersSign]
sign_type_analyse [definition, in AnalysersSign]
sign_oracle_loop_unfold [definition, in AnalysersSign]
sign_oracle_unfold [definition, in AnalysersSign]
sign_analyser_back_and_forth_correct [lemma, in AnalysersSign]
sign_analyser_back_and_forth [definition, in AnalysersSign]
sign_deep_analyser_oracle_fuel_correct [lemma, in AnalysersSign]
sign_analyser_oracle_deep_fuel [definition, in AnalysersSign]
sign_analyser_oracle_fuel_correct [lemma, in AnalysersSign]
sign_analyser_oracle_fuel [definition, in AnalysersSign]
sign_guess_fuel [definition, in AnalysersSign]
sign_deep_guess_step [definition, in AnalysersSign]
sign_guess_step [definition, in AnalysersSign]
sign_analyse_deep_fuel_correct [lemma, in AnalysersSign]
sign_analyse_deep_fuel [definition, in AnalysersSign]
sign_analyse_step_prev_term_loops_correct [lemma, in AnalysersSign]
sign_analyse_step_prev_term_loops [definition, in AnalysersSign]
sign_prev_term_not_looping_wf [lemma, in AnalysersSign]
sign_prev_term_not_looping [definition, in AnalysersSign]
sign_analyse_fuel_correct [lemma, in AnalysersSign]
sign_analyse_fuel [definition, in AnalysersSign]
sign_analyse_step_correct [lemma, in AnalysersSign]
sign_analyse_step [definition, in AnalysersSign]
sign_trivial_analyser_correct [lemma, in AnalysersSign]
sign_trivial_analyser [definition, in AnalysersSign]
sign_failing_analyser_correct [lemma, in AnalysersSign]
sign_failing_analyser [definition, in AnalysersSign]
sign_applicable_names_correct [lemma, in AnalysersSign]
sign_applicable_names [definition, in AnalysersSign]
sign_acond_Decidable [instance, in AnalysersSign]
sign_analyser_found [definition, in AnalysersSign]

other

[ _ ; .. ; _ ] (list_scope) [notation, in AnalysersSign]
[ _ ] (list_scope) [notation, in AnalysersSign]
[ ] (list_scope) [notation, in AnalysersSign]

Notation Index

other

[ _ ; .. ; _ ] (list_scope) [in AnalysersSign]
[ _ ] (list_scope) [in AnalysersSign]
[ ] (list_scope) [in AnalysersSign]

Variable Index

G

General.analyser_correct [in AnalysersSign]
General.analyser_result [in AnalysersSign]
General.correct_analyser_result [in AnalysersSign]

Library Index

A

AbstractSign
Analysers
AnalysersSign

C

D

P

Lemma Index

S

sign_analyse_oracle_back_and_forth_deep_loop_correct [in AnalysersSign]
sign_analyse_oracle_back_and_forth_deep_correct [in AnalysersSign]
sign_analyse_oracle_back_and_forth_loop_correct [in AnalysersSign]
sign_analyse_oracle_back_and_forth_correct [in AnalysersSign]
sign_analyse_deep_fuel_type_correct [in AnalysersSign]
sign_analyse_deep_fuel_fail_correct [in AnalysersSign]
sign_analyse_fuel_type_correct [in AnalysersSign]
sign_analyse_fuel_fail_correct [in AnalysersSign]
sign_type_analyse_correct [in AnalysersSign]
sign_analyser_back_and_forth_correct [in AnalysersSign]
sign_deep_analyser_oracle_fuel_correct [in AnalysersSign]
sign_analyser_oracle_fuel_correct [in AnalysersSign]
sign_analyse_deep_fuel_correct [in AnalysersSign]
sign_analyse_step_prev_term_loops_correct [in AnalysersSign]
sign_prev_term_not_looping_wf [in AnalysersSign]
sign_analyse_fuel_correct [in AnalysersSign]
sign_analyse_step_correct [in AnalysersSign]
sign_trivial_analyser_correct [in AnalysersSign]
sign_failing_analyser_correct [in AnalysersSign]
sign_applicable_names_correct [in AnalysersSign]

Constructor Index

I

is_looping_branch_call [in AnalysersSign]
is_looping_branch_while [in AnalysersSign]

Inductive Index

I

is_looping_branch [in AnalysersSign]

Section Index

G

General [in AnalysersSign]
General.Typed [in AnalysersSign]

Instance Index

A

abort_ast_decidable [in AnalysersSign]
abort_ares_decidable [in AnalysersSign]

I

is_looping_branch_Decidable [in AnalysersSign]

S

sign_acond_Decidable [in AnalysersSign]

Definition Index

A

analyser_match [in AnalysersSign]

E

eq_aValVar [in AnalysersSign]

S

sign_analyse_oracle_back_and_forth_deep_loop [in AnalysersSign]
sign_analyse_oracle_back_and_forth_deep [in AnalysersSign]
sign_analyse_oracle_back_and_forth_loop [in AnalysersSign]
sign_analyse_oracle_back_and_forth [in AnalysersSign]
sign_analyse_deep_fuel_type [in AnalysersSign]
sign_analyse_deep_fuel_fail [in AnalysersSign]
sign_analyse_fuel_type [in AnalysersSign]
sign_analyse_fuel_fail [in AnalysersSign]
sign_type_analyse [in AnalysersSign]
sign_oracle_loop_unfold [in AnalysersSign]
sign_oracle_unfold [in AnalysersSign]
sign_analyser_back_and_forth [in AnalysersSign]
sign_analyser_oracle_deep_fuel [in AnalysersSign]
sign_analyser_oracle_fuel [in AnalysersSign]
sign_guess_fuel [in AnalysersSign]
sign_deep_guess_step [in AnalysersSign]
sign_guess_step [in AnalysersSign]
sign_analyse_deep_fuel [in AnalysersSign]
sign_analyse_step_prev_term_loops [in AnalysersSign]
sign_prev_term_not_looping [in AnalysersSign]
sign_analyse_fuel [in AnalysersSign]
sign_analyse_step [in AnalysersSign]
sign_trivial_analyser [in AnalysersSign]
sign_failing_analyser [in AnalysersSign]
sign_applicable_names [in AnalysersSign]
sign_analyser_found [in AnalysersSign]

Global Index

B

F

H

J

K

L

M

N

O

Q

R

T

U

V

W

X

Y

Z

_

(69 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)

Variable Index

A

B

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Library Index

B

E

F

G

H

I

J

K

L

M

N

O

Q

R

S

T

U

V

W

X

Y

Z

_

other

(6 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(20 entries)

Constructor Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Inductive Index

A

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Section Index

A

B

C

D

E

F

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(2 entries)

Instance Index

B

C

D

E

F

G

H

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(4 entries)

Definition Index

B

C

D

F

G

H

I

J

K

L

M

N

O

P

Q

R

T

U

V

W

X

Y

Z

_

other

(28 entries)

This page has been generated by coqdoc