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

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

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

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

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

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

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

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

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

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

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

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

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

(143 entries)

---

Global Index

A

AbsTy [definition, in Top.Semantics]
AbsTyTrans [definition, in Top.Semantics]
admit [definition, in Top.Utils]
AppTy [definition, in Top.Semantics]
AppTyFVal [lemma, in Top.Semantics]
AppTyValVal [lemma, in Top.Semantics]
AppTy_Prop [lemma, in Top.Semantics]
AppTy_ρ [definition, in Top.Semantics]

B

Biorthogonality [module, in Top.Biorthogonality]
Biorthogonality [library]
Biorthogonality.CO [module, in Top.Biorthogonality]
Biorthogonality.GC [module, in Top.Biorthogonality]
BOp [inductive, in Top.BOp]
BOp [library]
BOpTyValVal [lemma, in Top.Semantics]
BOpTyValVal' [lemma, in Top.Semantics]

C

CCURRY [definition, in Top.DomainStuff]
ClosureOperator [module, in Top.Biorthogonality]
ClosureOperator.extensive [axiom, in Top.Biorthogonality]
ClosureOperator.h [axiom, in Top.Biorthogonality]
ClosureOperator.idemp [axiom, in Top.Biorthogonality]
ClosureOperator.monotone [axiom, in Top.Biorthogonality]
ClosureOperator.P [module, in Top.Biorthogonality]
_ == _ [notation, in Top.Biorthogonality]
_ ≦ _ [notation, in Top.Biorthogonality]
Code [inductive, in Top.Machine]
compile [definition, in Top.Compiler]
Compiler [library]
comp_simpl [lemma, in Top.DomainStuff]
cprod_fun [definition, in Top.Semantics]
CProd_fun [definition, in Top.Semantics]
ctx [definition, in Top.Syntax]
ctx_denot [definition, in Top.Semantics]
Curry1_cont [lemma, in Top.DomainStuff]
CURRY1_mon [definition, in Top.DomainStuff]
Curry1_mon [lemma, in Top.DomainStuff]

D

DenoApprox [module, in Top.DenoApprox]
DenoApprox [library]
DenoApprox.approx_rec_n [lemma, in Top.DenoApprox]
DenoApprox.bot_approx [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_snd [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_fst [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_pair [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_cprod_fun_pair [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_ifz [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_bop [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_let [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_app [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_swap_app [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_abs [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_var [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_int [lemma, in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_unit [lemma, in Top.DenoApprox]
DenoApprox.clos_approx_rec [lemma, in Top.DenoApprox]
DenoApprox.clos_approx_rec_n [lemma, in Top.DenoApprox]
DenoApprox.clos_realizers_Equal [lemma, in Top.DenoApprox]
DenoApprox.clos_Realizers [definition, in Top.DenoApprox]
DenoApprox.compiler_correctness_abs [lemma, in Top.DenoApprox]
DenoApprox.compiler_correctness_var [lemma, in Top.DenoApprox]
DenoApprox.compiler_correctness_int [lemma, in Top.DenoApprox]
DenoApprox.compiler_correctness_unit [lemma, in Top.DenoApprox]
DenoApprox.EnvRealizers [definition, in Top.DenoApprox]
DenoApprox.env_realizer_lookup [lemma, in Top.DenoApprox]
DenoApprox.env_realizer_realizer_cons [lemma, in Top.DenoApprox]
DenoApprox.env_realizer_extend_heap [lemma, in Top.DenoApprox]
DenoApprox.env_realizer_def [lemma, in Top.DenoApprox]
DenoApprox.env_realizer_nil [lemma, in Top.DenoApprox]
DenoApprox.env_realizer_ptr [lemma, in Top.DenoApprox]
DenoApprox.env_realizers_Equal [lemma, in Top.DenoApprox]
DenoApprox.EType [definition, in Top.DenoApprox]
DenoApprox.exists_fresh_pointer [definition, in Top.DenoApprox]
DenoApprox.flipIn [abbreviation, in Top.DenoApprox]
DenoApprox.fold_Realizer [lemma, in Top.DenoApprox]
DenoApprox.GRealizers [definition, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_snd [lemma, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_fst [lemma, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_pair [lemma, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_ifz [lemma, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_bop [lemma, in Top.DenoApprox]
DenoApprox.g_compiler_correctness_app [lemma, in Top.DenoApprox]
DenoApprox.g_bot_approx [lemma, in Top.DenoApprox]
DenoApprox.ideal_compiler_correctness [lemma, in Top.DenoApprox]
DenoApprox.ifz_conf_prop [lemma, in Top.DenoApprox]
DenoApprox.OO [module, in Top.DenoApprox]
DenoApprox.Primitives [definition, in Top.DenoApprox]
DenoApprox.primitives_Equal [lemma, in Top.DenoApprox]
DenoApprox.primitive_realizer [lemma, in Top.DenoApprox]
DenoApprox.primitive_Equal [lemma, in Top.DenoApprox]
DenoApprox.Realizers [definition, in Top.DenoApprox]
DenoApprox.realizers_Equal [lemma, in Top.DenoApprox]
DenoApprox.realizers_Equal' [lemma, in Top.DenoApprox]
DenoApprox.realizer_ifz [lemma, in Top.DenoApprox]
DenoApprox.realizer_push [lemma, in Top.DenoApprox]
DenoApprox.realizer_access [lemma, in Top.DenoApprox]
DenoApprox.realizer_extend_heap [lemma, in Top.DenoApprox]
DenoApprox.realizer_in_Ω [lemma, in Top.DenoApprox]
DenoApprox.RType [definition, in Top.DenoApprox]
DenoApprox.r_wf_joinable [lemma, in Top.DenoApprox]
DenoApprox.r_wf_heap' [lemma, in Top.DenoApprox]
DenoApprox.r_wf_heap [lemma, in Top.DenoApprox]
DenoApprox.r_wf_find [lemma, in Top.DenoApprox]
DenoApprox.r_wf [definition, in Top.DenoApprox]
DenoApprox.satif [definition, in Top.DenoApprox]
DenoApprox.TestRealizer [module, in Top.DenoApprox]
DenoApprox.TestRealizer.Elt [definition, in Top.DenoApprox]
DenoApprox.TestRealizer.satif [definition, in Top.DenoApprox]
DenoApprox.TestRealizer.Tst [definition, in Top.DenoApprox]
DenoApprox.Tests [definition, in Top.DenoApprox]
DenoApprox.tests_ifz_NZ [lemma, in Top.DenoApprox]
DenoApprox.tests_ifz_Z [lemma, in Top.DenoApprox]
DenoApprox.tests_ifz [lemma, in Top.DenoApprox]
DenoApprox.tests_bop_3 [lemma, in Top.DenoApprox]
DenoApprox.tests_bop_2 [lemma, in Top.DenoApprox]
DenoApprox.tests_bop_1 [lemma, in Top.DenoApprox]
DenoApprox.tests_pairs_2 [lemma, in Top.DenoApprox]
DenoApprox.tests_pairs_1 [lemma, in Top.DenoApprox]
DenoApprox.tests_functional [lemma, in Top.DenoApprox]
DenoApprox.Tests_Equal [lemma, in Top.DenoApprox]
DenoApprox.Tests_Equal' [lemma, in Top.DenoApprox]
DenoApprox.tests_realizers [lemma, in Top.DenoApprox]
DenoApprox.TType [definition, in Top.DenoApprox]
DenoApprox.t_wf_heap [lemma, in Top.DenoApprox]
DenoApprox.t_wf [definition, in Top.DenoApprox]
DenoApprox.var_to_nat_lookup [lemma, in Top.DenoApprox]
_ ◈ _ [notation, in Top.DenoApprox]
_ ▶ _ [notation, in Top.DenoApprox]
_ ⊆ _ [notation, in Top.DenoApprox]
_ ∈ _ [notation, in Top.DenoApprox]
Rp( _ , _ ) [notation, in Top.DenoApprox]
R( _ , _ ) [notation, in Top.DenoApprox]
t_Rp( _ , _ ) [notation, in Top.DenoApprox]
DLleEpsTrans [lemma, in Top.DomainStuff]
DLleEq [lemma, in Top.DomainStuff]
DLleEqR [lemma, in Top.DomainStuff]
DomainStuff [library]

E

EnsembleGC [module, in Top.Biorthogonality]
EnsembleGC.antitone [lemma, in Top.Biorthogonality]
EnsembleGC.f [definition, in Top.Biorthogonality]
EnsembleGC.g [definition, in Top.Biorthogonality]
EnsembleGC.OO [module, in Top.Biorthogonality]
EnsembleGC.P [module, in Top.Biorthogonality]
EnsembleGC.PTyp [module, in Top.Biorthogonality]
EnsembleGC.PTyp.t [definition, in Top.Biorthogonality]
EnsembleGC.Q [module, in Top.Biorthogonality]
EnsembleGC.QTyp [module, in Top.Biorthogonality]
EnsembleGC.QTyp.t [definition, in Top.Biorthogonality]
EpsStable [lemma, in Top.DomainStuff]
EqCompat [module, in Top.Map]
EqCompat.eq [definition, in Top.Map]
EqCompat.eq_trans [lemma, in Top.Map]
EqCompat.eq_sym [lemma, in Top.Map]
EqCompat.eq_refl [lemma, in Top.Map]
EqCompat.t [definition, in Top.Map]

F

FC [definition, in Top.DomainStuff]
FChain [definition, in Top.DomainStuff]
FChainCore [definition, in Top.DomainStuff]
FChainCore_mon [lemma, in Top.DomainStuff]
FChainCore_S [lemma, in Top.DomainStuff]
FChainCore_S_unfold [lemma, in Top.DomainStuff]
FChainCore_unfold [lemma, in Top.DomainStuff]
FChain_mon [lemma, in Top.DomainStuff]
FChain_S [lemma, in Top.DomainStuff]
FC_Prop [lemma, in Top.DomainStuff]
FC_lub [lemma, in Top.DomainStuff]
FC_unfold [lemma, in Top.DomainStuff]
FC_zero [lemma, in Top.DomainStuff]
FC_simpl [lemma, in Top.DomainStuff]
FixF [definition, in Top.DomainStuff]
FstTyValVal [lemma, in Top.Semantics]

G

GCClosure [module, in Top.Biorthogonality]
GCClosure.extensive [lemma, in Top.Biorthogonality]
GCClosure.GD [module, in Top.Biorthogonality]
GCClosure.GDF [module, in Top.Biorthogonality]
GCClosure.GF [module, in Top.Biorthogonality]
GCClosure.h [definition, in Top.Biorthogonality]
GCClosure.idemp [lemma, in Top.Biorthogonality]
GCClosure.monotone [lemma, in Top.Biorthogonality]
GCClosure.P [module, in Top.Biorthogonality]
GCDual [module, in Top.Biorthogonality]
GCDual.antitone [lemma, in Top.Biorthogonality]
GCDual.f [definition, in Top.Biorthogonality]
GCDual.g [definition, in Top.Biorthogonality]
GCDual.P [module, in Top.Biorthogonality]
GCDual.Q [module, in Top.Biorthogonality]
GCFacts [module, in Top.Biorthogonality]
GCFacts.comp_equality [lemma, in Top.Biorthogonality]
GCFacts.comp_extensivity [lemma, in Top.Biorthogonality]
GCFacts.function_resp [lemma, in Top.Biorthogonality]
GCFacts.function_antitone [lemma, in Top.Biorthogonality]
GCType [module, in Top.Biorthogonality]
GCType.antitone [axiom, in Top.Biorthogonality]
GCType.f [axiom, in Top.Biorthogonality]
GCType.g [axiom, in Top.Biorthogonality]
GCType.P [module, in Top.Biorthogonality]
GCType.Q [module, in Top.Biorthogonality]
_ == _ (P_scope) [notation, in Top.Biorthogonality]
_ ≦ _ (P_scope) [notation, in Top.Biorthogonality]
_ == _ (Q_scope) [notation, in Top.Biorthogonality]
_ ≦ _ (Q_scope) [notation, in Top.Biorthogonality]

H

Heap [module, in Top.Map]
Heap.elt [definition, in Top.Map]
Heap.EltPairEq [module, in Top.Map]
Heap.elt_pair [definition, in Top.Map]
Heap.Heap [definition, in Top.Map]
Heap.Map [module, in Top.Map]
Heap.Pointer [definition, in Top.Map]
Heap.PointerListEq [module, in Top.Map]
Heap.PointerTypeU [module, in Top.Map]

I

iaccess [constructor, in Top.Machine]
ibop [constructor, in Top.Machine]
ifst [constructor, in Top.Machine]
IfZInt [definition, in Top.DomainStuff]
IfZIntCoreM [definition, in Top.DomainStuff]
IfZIntCoreM2 [definition, in Top.DomainStuff]
IfZIntCore_cont2 [lemma, in Top.DomainStuff]
IfZIntCore_mon2 [lemma, in Top.DomainStuff]
IfZIntCore_mon [lemma, in Top.DomainStuff]
IfZIntTy [definition, in Top.Semantics]
IfZNat [definition, in Top.DomainStuff]
IfZNatCoreM [definition, in Top.DomainStuff]
IfZNatCoreM2 [definition, in Top.DomainStuff]
IfZNatCore_cont2 [lemma, in Top.DomainStuff]
IfZNatCore_mon2 [lemma, in Top.DomainStuff]
IfZNatCore_mon [lemma, in Top.DomainStuff]
IfZSemInt [definition, in Top.DomainStuff]
IfZSemInt_cont [lemma, in Top.Semantics]
IfZSemNat [definition, in Top.DomainStuff]
IfZSem_prop [lemma, in Top.Semantics]
IfZTyValVal [lemma, in Top.Semantics]
IfZTyValVal' [lemma, in Top.Semantics]
igrab [constructor, in Top.Machine]
iifz [constructor, in Top.Machine]
iint [constructor, in Top.Machine]
ilet [constructor, in Top.Machine]
Included_Singleton [lemma, in Top.Sets]
Included_Union_2 [lemma, in Top.Sets]
Included_Union_1 [lemma, in Top.Sets]
Included_trans [lemma, in Top.Sets]
Included_refl [lemma, in Top.Sets]
InclusionOrdered [module, in Top.Biorthogonality]
InclusionOrdered.E [module, in Top.Biorthogonality]
InclusionOrdered.eq [definition, in Top.Biorthogonality]
InclusionOrdered.E.eq [definition, in Top.Biorthogonality]
InclusionOrdered.E.eq_equiv [lemma, in Top.Biorthogonality]
InclusionOrdered.E.t [definition, in Top.Biorthogonality]
InclusionOrdered.le [definition, in Top.Biorthogonality]
InclusionOrdered.le_antisym [lemma, in Top.Biorthogonality]
InclusionOrdered.le_trans [lemma, in Top.Biorthogonality]
InclusionOrdered.le_refl [lemma, in Top.Biorthogonality]
InclusionOrdered.le_compat [lemma, in Top.Biorthogonality]
InclusionOrdered.PosetType_Compat [instance, in Top.Biorthogonality]
InclusionOrdered.PosetType_Antisymmetric [instance, in Top.Biorthogonality]
InclusionOrdered.PosetType_Transitive [instance, in Top.Biorthogonality]
InclusionOrdered.PosetType_Reflexive [instance, in Top.Biorthogonality]
InclusionOrdered.t [definition, in Top.Biorthogonality]
IntOpTy [definition, in Top.Semantics]
ipair [constructor, in Top.Machine]
ipush [constructor, in Top.Machine]
irec [constructor, in Top.Machine]
isnd [constructor, in Top.Machine]
iunit [constructor, in Top.Machine]
ival [constructor, in Top.Machine]

K

KLEISLIL_Eps [lemma, in Top.DomainStuff]
KLEISLIL_PBot [lemma, in Top.DomainStuff]
KLEISLIL_unit2 [lemma, in Top.DomainStuff]
KLEISLIR_Eps [lemma, in Top.DomainStuff]
KLEISLIR_KR_eq2 [lemma, in Top.DomainStuff]
KLEISLIR_KR_eq [lemma, in Top.DomainStuff]
KLEISLIR_PBot [lemma, in Top.DomainStuff]
KLEISLIR_unit2 [lemma, in Top.DomainStuff]
KLEISLI_RL_Val [lemma, in Top.DomainStuff]
KLEISLI_LR_Val [lemma, in Top.DomainStuff]
KLESILIL_lub_comp_eq [lemma, in Top.DomainStuff]
KLESILIR_lub_comp_eq [lemma, in Top.DomainStuff]
KR [definition, in Top.DomainStuff]
KRKUR_id2 [lemma, in Top.DomainStuff]
KRKUR_id [lemma, in Top.DomainStuff]
KUR [definition, in Top.DomainStuff]
KURKR_id2 [lemma, in Top.DomainStuff]
KURKR_id [lemma, in Top.DomainStuff]

L

LetTy [definition, in Top.Semantics]
Letty_unfold [lemma, in Top.Semantics]
ListEq [module, in Top.Map]
ListEq.eq [definition, in Top.Map]
ListEq.eq_equiv [lemma, in Top.Map]
ListEq.t [definition, in Top.Map]
lookup [definition, in Top.Semantics]
lookup_nat [definition, in Top.Semantics]
lub_discrete_chain [lemma, in Top.DomainStuff]

M

Machine [module, in Top.Machine]
Machine [library]
Machine.bopapply [constructor, in Top.Machine]
Machine.C [constructor, in Top.Machine]
Machine.CodeTyp [module, in Top.Machine]
Machine.CodeTyp.t [definition, in Top.Machine]
Machine.conf [definition, in Top.Machine]
Machine.conf_eq [definition, in Top.Machine]
Machine.conf_wf [definition, in Top.Machine]
Machine.Cont [inductive, in Top.Machine]
Machine.env_ptr_cons_included [lemma, in Top.Machine]
Machine.env_ptr [definition, in Top.Machine]
Machine.find_heap_range [lemma, in Top.Machine]
Machine.fresh_for_heap_join_1 [lemma, in Top.Machine]
Machine.fresh_for_heap_join [lemma, in Top.Machine]
Machine.fresh_for [definition, in Top.Machine]
Machine.fresh_for_stack [definition, in Top.Machine]
Machine.fresh_for_env [definition, in Top.Machine]
Machine.fresh_for_heap [definition, in Top.Machine]
Machine.HClos [definition, in Top.Machine]
Machine.HClos_prop' [lemma, in Top.Machine]
Machine.HClos_prop [lemma, in Top.Machine]
Machine.HClos_to_MClos [definition, in Top.Machine]
Machine.HeapElem [inductive, in Top.Machine]
Machine.HeapM [module, in Top.Machine]
Machine.heaps_prop_ifz [lemma, in Top.Machine]
Machine.heap_add_prop'' [lemma, in Top.Machine]
Machine.heap_add_join_prop [lemma, in Top.Machine]
Machine.heap_add_prop_idemp''' [lemma, in Top.Machine]
Machine.heap_add_prop_idemp'' [lemma, in Top.Machine]
Machine.heap_add_prop' [lemma, in Top.Machine]
Machine.heap_ptr_Same [lemma, in Top.Machine]
Machine.heap_ptr_Included [lemma, in Top.Machine]
Machine.heap_range_Same [lemma, in Top.Machine]
Machine.heap_range_Included [lemma, in Top.Machine]
Machine.heap_range_singleton [lemma, in Top.Machine]
Machine.heap_wf [definition, in Top.Machine]
Machine.heap_ptr [definition, in Top.Machine]
Machine.heap_range_ptr [definition, in Top.Machine]
Machine.IfZ [constructor, in Top.Machine]
Machine.ifzapply [constructor, in Top.Machine]
Machine.ival_update_2 [constructor, in Top.Machine]
Machine.ival_update_1 [constructor, in Top.Machine]
Machine.ival_update [constructor, in Top.Machine]
Machine.Joinable_fresh [lemma, in Top.Machine]
Machine.Join_fresh_add_prop [lemma, in Top.Machine]
Machine.Join_add_prop' [lemma, in Top.Machine]
Machine.Join_heap_ptr [lemma, in Top.Machine]
Machine.Join_range_ptr [lemma, in Top.Machine]
Machine.K [constructor, in Top.Machine]
Machine.key_set_singleton [lemma, in Top.Machine]
Machine.mapply [constructor, in Top.Machine]
Machine.mapplypi1 [constructor, in Top.Machine]
Machine.mapplypi2 [constructor, in Top.Machine]
Machine.Marker [inductive, in Top.Machine]
Machine.MClos [definition, in Top.Machine]
Machine.MClos_to_HClos [definition, in Top.Machine]
Machine.MEnv [definition, in Top.Machine]
Machine.mupdate [constructor, in Top.Machine]
Machine.mupdatepi1 [constructor, in Top.Machine]
Machine.mupdatepi2 [constructor, in Top.Machine]
Machine.Pointer [definition, in Top.Machine]
Machine.rec_eval [constructor, in Top.Machine]
Machine.stack [definition, in Top.Machine]
Machine.stack_ptr_eq_2 [lemma, in Top.Machine]
Machine.stack_ptr_eq_1 [lemma, in Top.Machine]
Machine.stack_ptr_cons_included_if [lemma, in Top.Machine]
Machine.stack_ptr_cons_included_bop [lemma, in Top.Machine]
Machine.stack_ptr_cons_included2 [lemma, in Top.Machine]
Machine.stack_ptr_cons_included [lemma, in Top.Machine]
Machine.stack_ptr [definition, in Top.Machine]
Machine.taccess [constructor, in Top.Machine]
Machine.tbop_apply_3 [constructor, in Top.Machine]
Machine.tbop_apply_2 [constructor, in Top.Machine]
Machine.tbop_apply_1 [constructor, in Top.Machine]
Machine.tfst [constructor, in Top.Machine]
Machine.tgrab_apply [constructor, in Top.Machine]
Machine.tifz [constructor, in Top.Machine]
Machine.tifz_n0 [constructor, in Top.Machine]
Machine.tifz_0 [constructor, in Top.Machine]
Machine.tlet [constructor, in Top.Machine]
Machine.tpair_apply_pi2 [constructor, in Top.Machine]
Machine.tpair_apply_pi1 [constructor, in Top.Machine]
Machine.tpush [constructor, in Top.Machine]
Machine.trans [inductive, in Top.Machine]
Machine.tsnd [constructor, in Top.Machine]
Machine.wf_add [lemma, in Top.Machine]
Machine.wf_union [lemma, in Top.Machine]
Machine.ZBOpL [constructor, in Top.Machine]
Machine.ZBOpR [constructor, in Top.Machine]
_ [==] _ [notation, in Top.Machine]
_ ↦ _ [notation, in Top.Machine]
# _ [notation, in Top.Machine]
#1 _ [notation, in Top.Machine]
#2 _ [notation, in Top.Machine]
? _ [notation, in Top.Machine]
⌑ _ [notation, in Top.Machine]
⦿ _ _ [notation, in Top.Machine]
MakeMap [module, in Top.Map]
MakeMap.elt [definition, in Top.Map]
MakeMap.heap_eq [definition, in Top.Map]
MakeMap.join [definition, in Top.Map]
MakeMap.Joinable [definition, in Top.Map]
MakeMap.JoinableDef [section, in Top.Map]
MakeMap.JoinableDef.m1 [variable, in Top.Map]
MakeMap.JoinableDef.m2 [variable, in Top.Map]
MakeMap.Joinable_join_assoc_1 [lemma, in Top.Map]
MakeMap.Joinable_join_elim_2 [lemma, in Top.Map]
MakeMap.Joinable_join_elim_1 [lemma, in Top.Map]
MakeMap.Joinable_submap_2 [lemma, in Top.Map]
MakeMap.Joinable_submap [lemma, in Top.Map]
MakeMap.Joinable_join_intro_l [lemma, in Top.Map]
MakeMap.Joinable_join_intro_r [lemma, in Top.Map]
MakeMap.Joinable_join_comm [lemma, in Top.Map]
MakeMap.Joinable_refl [lemma, in Top.Map]
MakeMap.joinable_join2 [lemma, in Top.Map]
MakeMap.joinable_join1 [lemma, in Top.Map]
MakeMap.joinable_comm [lemma, in Top.Map]
MakeMap.JoinDef [section, in Top.Map]
MakeMap.JoinSpec [section, in Top.Map]
MakeMap.JoinSpec.m1 [variable, in Top.Map]
MakeMap.JoinSpec.m2 [variable, in Top.Map]
MakeMap.join_sub2 [lemma, in Top.Map]
MakeMap.join_sub1 [lemma, in Top.Map]
MakeMap.join_in2 [lemma, in Top.Map]
MakeMap.join_in1 [lemma, in Top.Map]
MakeMap.join_in [lemma, in Top.Map]
MakeMap.join_MapsTo [lemma, in Top.Map]
MakeMap.KeySet [definition, in Top.Map]
MakeMap.key_set_find_in [lemma, in Top.Map]
MakeMap.key_set [definition, in Top.Map]
MakeMap.key_eq [abbreviation, in Top.Map]
MakeMap.Map [module, in Top.Map]
MakeMap.MapFacts [module, in Top.Map]
MakeMap.MapRaw [module, in Top.Map]
MakeMap.SetIn [definition, in Top.Map]
MakeMap.singleton [definition, in Top.Map]
MakeMap.Submap [definition, in Top.Map]
MakeMap.SubmapDef [section, in Top.Map]
MakeMap.SubmapDef.m1 [variable, in Top.Map]
MakeMap.SubmapDef.m2 [variable, in Top.Map]
MakeMap.Submap_MapsTo [lemma, in Top.Map]
_ ⋈ _ [notation, in Top.Map]
_ ∪ _ [notation, in Top.Map]
⎨ _ ⤇ _ ⎬ [notation, in Top.Map]
Map [library]
MapRaw [module, in Top.Map]
MapRaw.InA_remove [lemma, in Top.Map]
MapRaw.InA_join_1 [lemma, in Top.Map]
MapRaw.In_nil [lemma, in Top.Map]
MapRaw.join [definition, in Top.Map]
MapRaw.join_in2 [lemma, in Top.Map]
MapRaw.join_in1 [lemma, in Top.Map]
MapRaw.join_NoDup [lemma, in Top.Map]
MapRaw.join_MapsTo [lemma, in Top.Map]
MapRaw.MapsTo_join_2_aux1 [lemma, in Top.Map]
MapRaw.MapsTo_InA [lemma, in Top.Map]
MapRaw.MapsTo_join_1 [lemma, in Top.Map]
MinusBOp [constructor, in Top.BOp]

N

none_is_not_some [lemma, in Top.Semantics]
nth_var_to_nat [lemma, in Top.Compiler]
nth_error_nil [lemma, in Top.Semantics]

O

Obs [library]
Observations [module, in Top.Obs]
ObservationsSI [module, in Top.ObsSI]
ObservationsSI.add_marker_pi2 [axiom, in Top.ObsSI]
ObservationsSI.add_marker_pi1 [axiom, in Top.ObsSI]
ObservationsSI.add_marker [axiom, in Top.ObsSI]
ObservationsSI.antiex [axiom, in Top.ObsSI]
ObservationsSI.ConfSet [definition, in Top.ObsSI]
ObservationsSI.eq_closed [axiom, in Top.ObsSI]
ObservationsSI.extend_heap [axiom, in Top.ObsSI]
ObservationsSI.M [module, in Top.ObsSI]
ObservationsSI.SetIn [definition, in Top.ObsSI]
ObservationsSI.stepI [axiom, in Top.ObsSI]
ObservationsSI.Ω [axiom, in Top.ObsSI]
Observations.add_marker_pi2 [axiom, in Top.Obs]
Observations.add_marker_pi1 [axiom, in Top.Obs]
Observations.add_marker [axiom, in Top.Obs]
Observations.antiex [axiom, in Top.Obs]
Observations.ConfSet [definition, in Top.Obs]
Observations.eq_closed [axiom, in Top.Obs]
Observations.extend_heap [axiom, in Top.Obs]
Observations.M [module, in Top.Obs]
Observations.SetIn [definition, in Top.Obs]
Observations.Ω [axiom, in Top.Obs]
ObsSI [library]
OperApprox [module, in Top.OperApprox]
OperApprox [library]
OperApprox.bbot_down_closed [lemma, in Top.OperApprox]
OperApprox.ble [lemma, in Top.OperApprox]
OperApprox.compiler_correctness [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_snd [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_fst [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_pair [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_ifz [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_bop [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_app [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_let [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_abs [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_var [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_int [lemma, in Top.OperApprox]
OperApprox.compiler_correctness_unit [lemma, in Top.OperApprox]
OperApprox.EnvRealizers [definition, in Top.OperApprox]
OperApprox.env_realizer_ptr [lemma, in Top.OperApprox]
OperApprox.env_realizer_realizer_cons [lemma, in Top.OperApprox]
OperApprox.env_realizer_extend_heap [lemma, in Top.OperApprox]
OperApprox.env_realizer_gen_StepI [lemma, in Top.OperApprox]
OperApprox.env_realizer_StepI [lemma, in Top.OperApprox]
OperApprox.env_realizer_def [lemma, in Top.OperApprox]
OperApprox.env_realizer_nil [lemma, in Top.OperApprox]
OperApprox.env_realizers_Equal [lemma, in Top.OperApprox]
OperApprox.env_realizer_lookup [lemma, in Top.OperApprox]
OperApprox.EType [definition, in Top.OperApprox]
OperApprox.exists_fresh_pointer [definition, in Top.OperApprox]
OperApprox.flipIn [abbreviation, in Top.OperApprox]
OperApprox.GRealizers [definition, in Top.OperApprox]
OperApprox.ifz_conf_prop [lemma, in Top.OperApprox]
OperApprox.iRType [definition, in Top.OperApprox]
OperApprox.isatif [definition, in Top.OperApprox]
OperApprox.isatif_eq_Fullset [lemma, in Top.OperApprox]
OperApprox.isatif_down_closed [lemma, in Top.OperApprox]
OperApprox.iTType [definition, in Top.OperApprox]
OperApprox.LiftRel [definition, in Top.OperApprox]
OperApprox.OO [module, in Top.OperApprox]
OperApprox.Primitives [definition, in Top.OperApprox]
OperApprox.primitive_gen_StepI [lemma, in Top.OperApprox]
OperApprox.primitive_StepI [lemma, in Top.OperApprox]
OperApprox.primitive_realizer [lemma, in Top.OperApprox]
OperApprox.primitive_Equal [lemma, in Top.OperApprox]
OperApprox.Realizers [definition, in Top.OperApprox]
OperApprox.realizers_Equal' [lemma, in Top.OperApprox]
OperApprox.realizers_Equal [lemma, in Top.OperApprox]
OperApprox.realizer_push [lemma, in Top.OperApprox]
OperApprox.realizer_rec [lemma, in Top.OperApprox]
OperApprox.realizer_access [lemma, in Top.OperApprox]
OperApprox.realizer_extend_heap [lemma, in Top.OperApprox]
OperApprox.realizer_gen_StepI [lemma, in Top.OperApprox]
OperApprox.realizer_StepI [lemma, in Top.OperApprox]
OperApprox.realizer_in_Ω [lemma, in Top.OperApprox]
OperApprox.RType [definition, in Top.OperApprox]
OperApprox.r_wf_joinable [lemma, in Top.OperApprox]
OperApprox.r_wf_heap' [lemma, in Top.OperApprox]
OperApprox.r_wf_heap [lemma, in Top.OperApprox]
OperApprox.r_wf_find [lemma, in Top.OperApprox]
OperApprox.r_wf [definition, in Top.OperApprox]
OperApprox.satif [definition, in Top.OperApprox]
OperApprox.satif_Equal1 [lemma, in Top.OperApprox]
OperApprox.TestRealizer [module, in Top.OperApprox]
OperApprox.TestRealizer.Elt [definition, in Top.OperApprox]
OperApprox.TestRealizer.satif [definition, in Top.OperApprox]
OperApprox.TestRealizer.Tst [definition, in Top.OperApprox]
OperApprox.Tests [definition, in Top.OperApprox]
OperApprox.tests_pairs_2 [lemma, in Top.OperApprox]
OperApprox.tests_pairs_1 [lemma, in Top.OperApprox]
OperApprox.tests_ifz [lemma, in Top.OperApprox]
OperApprox.tests_bop_2 [lemma, in Top.OperApprox]
OperApprox.tests_bop_1 [lemma, in Top.OperApprox]
OperApprox.tests_functional [lemma, in Top.OperApprox]
OperApprox.tests_bot [lemma, in Top.OperApprox]
OperApprox.Tests_Equal [lemma, in Top.OperApprox]
OperApprox.Tests_Equal' [lemma, in Top.OperApprox]
OperApprox.tests_realizers [lemma, in Top.OperApprox]
OperApprox.test_gen_StepI [lemma, in Top.OperApprox]
OperApprox.test_StepI [lemma, in Top.OperApprox]
OperApprox.TType [definition, in Top.OperApprox]
OperApprox.t_wf_heap [lemma, in Top.OperApprox]
OperApprox.t_wf [definition, in Top.OperApprox]
OperApprox.var_to_nat_lookup [lemma, in Top.OperApprox]
_ ⊢ _ ◀| _ [notation, in Top.OperApprox]
_ ⊴ _ | _ [notation, in Top.OperApprox]
_ ⊆ _ [notation, in Top.OperApprox]
_ ∈ _ [notation, in Top.OperApprox]
Rp( _ , _ , _ ) [notation, in Top.OperApprox]
R( _ , _ , _ ) [notation, in Top.OperApprox]
Operator2_reverse [definition, in Top.DomainStuff]
Operator2_strictR [lemma, in Top.DomainStuff]
Operator2_strictL [lemma, in Top.DomainStuff]
OpPlus [definition, in Top.DomainStuff]
OrthogonalOperators [module, in Top.Biorthogonality]
OrthogonalOperators.bbot [definition, in Top.Biorthogonality]
OrthogonalOperators.btop [definition, in Top.Biorthogonality]
_ ⌶ [notation, in Top.Biorthogonality]
_ ⊥ [notation, in Top.Biorthogonality]
_ ⊤ [notation, in Top.Biorthogonality]
_ ⊧ _ [notation, in Top.Biorthogonality]

P

PairEq [module, in Top.Map]
PairEq.eq [definition, in Top.Map]
PairEq.eq_equiv [lemma, in Top.Map]
PairEq.t [definition, in Top.Map]
PlusBOp [constructor, in Top.BOp]
PosetType [module, in Top.Biorthogonality]
PosetType.E [module, in Top.Biorthogonality]
PosetType.eq [definition, in Top.Biorthogonality]
PosetType.le [axiom, in Top.Biorthogonality]
PosetType.le_compat [axiom, in Top.Biorthogonality]
PosetType.le_antisym [axiom, in Top.Biorthogonality]
PosetType.le_trans [axiom, in Top.Biorthogonality]
PosetType.le_refl [axiom, in Top.Biorthogonality]
PosetType.PosetType_Compat [instance, in Top.Biorthogonality]
PosetType.PosetType_Antisymmetric [instance, in Top.Biorthogonality]
PosetType.PosetType_Transitive [instance, in Top.Biorthogonality]
PosetType.PosetType_Reflexive [instance, in Top.Biorthogonality]
PosetType.t [definition, in Top.Biorthogonality]
prod_fun_prop [lemma, in Top.Semantics]
prod_simpl [lemma, in Top.DomainStuff]

R

RUid [lemma, in Top.DomainStuff]

S

Same_set_in_iff [lemma, in Top.Sets]
Same_set_trans [lemma, in Top.Sets]
Same_set_sym [lemma, in Top.Sets]
Same_set_refl [lemma, in Top.Sets]
Semantics [library]
semZBOp [definition, in Top.BOp]
sem_term_app_Eq [lemma, in Top.Semantics]
sem_term_app_Eq' [lemma, in Top.Semantics]
Sets [library]
SimpleBOp [definition, in Top.DomainStuff]
SimpleBOpm [definition, in Top.DomainStuff]
SimpleB_cont [lemma, in Top.DomainStuff]
SimpleB_mon [lemma, in Top.DomainStuff]
SimpleU_mon [lemma, in Top.DomainStuff]
Smashs_eq [lemma, in Top.DomainStuff]
SmashValVal [lemma, in Top.Semantics]
Smash_ValVal [lemma, in Top.DomainStuff]
Smash_Val [lemma, in Top.DomainStuff]
Smash_Eps_r [lemma, in Top.DomainStuff]
Smash_reverse [definition, in Top.DomainStuff]
Smash_Eps_l [lemma, in Top.DomainStuff]
SndTyValVal [lemma, in Top.Semantics]
svar [constructor, in Top.Syntax]
SwapAppTy [definition, in Top.Semantics]
SwapArgs [definition, in Top.DomainStuff]
Syntax [library]

T

tarrow [constructor, in Top.Syntax]
term [inductive, in Top.Syntax]
term_snd [constructor, in Top.Syntax]
term_fst [constructor, in Top.Syntax]
term_pair [constructor, in Top.Syntax]
term_ifz [constructor, in Top.Syntax]
term_bop [constructor, in Top.Syntax]
term_let [constructor, in Top.Syntax]
term_app [constructor, in Top.Syntax]
term_abs [constructor, in Top.Syntax]
term_var [constructor, in Top.Syntax]
term_int [constructor, in Top.Syntax]
term_unit [constructor, in Top.Syntax]
term_denot [definition, in Top.Semantics]
tint [constructor, in Top.Syntax]
tpair [constructor, in Top.Syntax]
TstElt [module, in Top.Biorthogonality]
TstElt.Elt [axiom, in Top.Biorthogonality]
TstElt.satif [axiom, in Top.Biorthogonality]
TstElt.Tst [axiom, in Top.Biorthogonality]
tunit [constructor, in Top.Syntax]
type [inductive, in Top.Syntax]
ty_denot [definition, in Top.Semantics]
t_ty_denot [definition, in Top.Semantics]

U

UNCURRY [definition, in Top.DomainStuff]
UnCurry_cont [lemma, in Top.DomainStuff]
UNCURRY_mon [definition, in Top.DomainStuff]
UnCurry_mon [lemma, in Top.DomainStuff]
Union_subset [lemma, in Top.Sets]
Union_idem [lemma, in Top.Sets]
Union_assoc [lemma, in Top.Sets]
Union_comm [lemma, in Top.Sets]
union_included [lemma, in Top.Sets]
Union_in_iff [lemma, in Top.Sets]
URid [lemma, in Top.DomainStuff]
UsualHeap [module, in Top.Map]
UsualHeap.comp_join_elim_r [lemma, in Top.Map]
UsualHeap.comp_join_elim_l [lemma, in Top.Map]
UsualHeap.Eq [module, in Top.Map]
UsualHeap.eqlistA_leibniz [lemma, in Top.Map]
UsualHeap.Equal_join_mor [lemma, in Top.Map]
UsualHeap.Equal_key_set [lemma, in Top.Map]
UsualHeap.Eq.eq [definition, in Top.Map]
UsualHeap.Eq.eq_equiv [lemma, in Top.Map]
UsualHeap.Eq.t [definition, in Top.Map]
UsualHeap.find_singleton_Join [lemma, in Top.Map]
UsualHeap.find_singleton_Joinable [lemma, in Top.Map]
UsualHeap.find_Joinable_singleton_1 [lemma, in Top.Map]
UsualHeap.find_submap_singleton [lemma, in Top.Map]
UsualHeap.find_Equal [lemma, in Top.Map]
UsualHeap.find_submap [lemma, in Top.Map]
UsualHeap.Heap [module, in Top.Map]
UsualHeap.heap_find_join_prop' [lemma, in Top.Map]
UsualHeap.heap_find_join_prop [lemma, in Top.Map]
UsualHeap.heap_add_join_prop' [lemma, in Top.Map]
UsualHeap.heap_add_prop_idemp' [lemma, in Top.Map]
UsualHeap.heap_add_prop_idemp [lemma, in Top.Map]
UsualHeap.heap_add_prop [lemma, in Top.Map]
UsualHeap.heap_add_update_prop [lemma, in Top.Map]
UsualHeap.heap_Equal [lemma, in Top.Map]
UsualHeap.heap_Equiv [lemma, in Top.Map]
UsualHeap.heap_Equiv_eq [lemma, in Top.Map]
UsualHeap.heap_eq_Equiv [lemma, in Top.Map]
UsualHeap.Joinable_not_in [lemma, in Top.Map]
UsualHeap.Joinable_Equal_1 [lemma, in Top.Map]
UsualHeap.Join_add_prop''' [lemma, in Top.Map]
UsualHeap.Join_add_prop'' [lemma, in Top.Map]
UsualHeap.Join_add_prop [lemma, in Top.Map]
UsualHeap.Join_key_set [lemma, in Top.Map]
UsualHeap.Join_add [lemma, in Top.Map]
UsualHeap.Join_idem [lemma, in Top.Map]
UsualHeap.Join_assoc_1 [lemma, in Top.Map]
UsualHeap.Join_comm_1 [lemma, in Top.Map]
UsualHeap.MapsTo_singleton [lemma, in Top.Map]
UsualHeap.pair_eq_leibniz [lemma, in Top.Map]
UsualHeap.PointerTypeB [module, in Top.Map]
UsualHeap.Submap_MapsTo_leibniz [lemma, in Top.Map]
_ ≃ _ [notation, in Top.Map]
Utils [library]

V

Val [inductive, in Top.Machine]
var [inductive, in Top.Syntax]
var_to_nat [definition, in Top.Compiler]

W

WSfunExtended [module, in Top.Map]
WSfunExtended.elt [definition, in Top.Map]
WSfunExtended.join [axiom, in Top.Map]
WSfunExtended.Joinable [axiom, in Top.Map]
WSfunExtended.JoinSpec [section, in Top.Map]
WSfunExtended.JoinSpec.m1 [variable, in Top.Map]
WSfunExtended.JoinSpec.m2 [variable, in Top.Map]
WSfunExtended.join_MapsTo [axiom, in Top.Map]
WSfunExtended.join_sub2 [axiom, in Top.Map]
WSfunExtended.join_sub1 [axiom, in Top.Map]
WSfunExtended.Submap [axiom, in Top.Map]

Z

zvar [constructor, in Top.Syntax]

other

_ ⨱ _ [notation, in Top.Syntax]
_ ⇾ _ [notation, in Top.Syntax]
? [notation, in Top.Utils]
⟦ _ ⟧ [notation, in Top.Semantics]
⦇ _ ⦈ [notation, in Top.Compiler]

---

Notation Index

C

_ == _ [in Top.Biorthogonality]
_ ≦ _ [in Top.Biorthogonality]

D

_ ◈ _ [in Top.DenoApprox]
_ ▶ _ [in Top.DenoApprox]
_ ⊆ _ [in Top.DenoApprox]
_ ∈ _ [in Top.DenoApprox]
Rp( _ , _ ) [in Top.DenoApprox]
R( _ , _ ) [in Top.DenoApprox]
t_Rp( _ , _ ) [in Top.DenoApprox]

G

_ == _ (P_scope) [in Top.Biorthogonality]
_ ≦ _ (P_scope) [in Top.Biorthogonality]
_ == _ (Q_scope) [in Top.Biorthogonality]
_ ≦ _ (Q_scope) [in Top.Biorthogonality]

M

_ [==] _ [in Top.Machine]
_ ↦ _ [in Top.Machine]
# _ [in Top.Machine]
#1 _ [in Top.Machine]
#2 _ [in Top.Machine]
? _ [in Top.Machine]
⌑ _ [in Top.Machine]
⦿ _ _ [in Top.Machine]
_ ⋈ _ [in Top.Map]
_ ∪ _ [in Top.Map]
⎨ _ ⤇ _ ⎬ [in Top.Map]

O

_ ⊢ _ ◀| _ [in Top.OperApprox]
_ ⊴ _ | _ [in Top.OperApprox]
_ ⊆ _ [in Top.OperApprox]
_ ∈ _ [in Top.OperApprox]
Rp( _ , _ , _ ) [in Top.OperApprox]
R( _ , _ , _ ) [in Top.OperApprox]
_ ⌶ [in Top.Biorthogonality]
_ ⊥ [in Top.Biorthogonality]
_ ⊤ [in Top.Biorthogonality]
_ ⊧ _ [in Top.Biorthogonality]

U

_ ≃ _ [in Top.Map]

other

_ ⨱ _ [in Top.Syntax]
_ ⇾ _ [in Top.Syntax]
? [in Top.Utils]
⟦ _ ⟧ [in Top.Semantics]
⦇ _ ⦈ [in Top.Compiler]

---

Module Index

B

Biorthogonality [in Top.Biorthogonality]
Biorthogonality.CO [in Top.Biorthogonality]
Biorthogonality.GC [in Top.Biorthogonality]

C

ClosureOperator [in Top.Biorthogonality]
ClosureOperator.P [in Top.Biorthogonality]

D

DenoApprox [in Top.DenoApprox]
DenoApprox.OO [in Top.DenoApprox]
DenoApprox.TestRealizer [in Top.DenoApprox]

E

EnsembleGC [in Top.Biorthogonality]
EnsembleGC.OO [in Top.Biorthogonality]
EnsembleGC.P [in Top.Biorthogonality]
EnsembleGC.PTyp [in Top.Biorthogonality]
EnsembleGC.Q [in Top.Biorthogonality]
EnsembleGC.QTyp [in Top.Biorthogonality]
EqCompat [in Top.Map]

G

GCClosure [in Top.Biorthogonality]
GCClosure.GD [in Top.Biorthogonality]
GCClosure.GDF [in Top.Biorthogonality]
GCClosure.GF [in Top.Biorthogonality]
GCClosure.P [in Top.Biorthogonality]
GCDual [in Top.Biorthogonality]
GCDual.P [in Top.Biorthogonality]
GCDual.Q [in Top.Biorthogonality]
GCFacts [in Top.Biorthogonality]
GCType [in Top.Biorthogonality]
GCType.P [in Top.Biorthogonality]
GCType.Q [in Top.Biorthogonality]

H

Heap [in Top.Map]
Heap.EltPairEq [in Top.Map]
Heap.Map [in Top.Map]
Heap.PointerListEq [in Top.Map]
Heap.PointerTypeU [in Top.Map]

I

InclusionOrdered [in Top.Biorthogonality]
InclusionOrdered.E [in Top.Biorthogonality]

L

ListEq [in Top.Map]

M

Machine [in Top.Machine]
Machine.CodeTyp [in Top.Machine]
Machine.HeapM [in Top.Machine]
MakeMap [in Top.Map]
MakeMap.Map [in Top.Map]
MakeMap.MapFacts [in Top.Map]
MakeMap.MapRaw [in Top.Map]
MapRaw [in Top.Map]

O

Observations [in Top.Obs]
ObservationsSI [in Top.ObsSI]
ObservationsSI.M [in Top.ObsSI]
Observations.M [in Top.Obs]
OperApprox [in Top.OperApprox]
OperApprox.OO [in Top.OperApprox]
OperApprox.TestRealizer [in Top.OperApprox]
OrthogonalOperators [in Top.Biorthogonality]

P

PairEq [in Top.Map]
PosetType [in Top.Biorthogonality]
PosetType.E [in Top.Biorthogonality]

T

TstElt [in Top.Biorthogonality]

U

UsualHeap [in Top.Map]
UsualHeap.Eq [in Top.Map]
UsualHeap.Heap [in Top.Map]
UsualHeap.PointerTypeB [in Top.Map]

W

WSfunExtended [in Top.Map]

---

Variable Index

M

MakeMap.JoinableDef.m1 [in Top.Map]
MakeMap.JoinableDef.m2 [in Top.Map]
MakeMap.JoinSpec.m1 [in Top.Map]
MakeMap.JoinSpec.m2 [in Top.Map]
MakeMap.SubmapDef.m1 [in Top.Map]
MakeMap.SubmapDef.m2 [in Top.Map]

W

WSfunExtended.JoinSpec.m1 [in Top.Map]
WSfunExtended.JoinSpec.m2 [in Top.Map]

---

Library Index

B

Biorthogonality
BOp

C

Compiler

D

DenoApprox
DomainStuff

M

Machine
Map

O

Obs
ObsSI
OperApprox

S

Semantics
Sets
Syntax

U

Utils

---

Lemma Index

A

AppTyFVal [in Top.Semantics]
AppTyValVal [in Top.Semantics]
AppTy_Prop [in Top.Semantics]

B

BOpTyValVal [in Top.Semantics]
BOpTyValVal' [in Top.Semantics]

C

comp_simpl [in Top.DomainStuff]
Curry1_cont [in Top.DomainStuff]
Curry1_mon [in Top.DomainStuff]

D

DenoApprox.approx_rec_n [in Top.DenoApprox]
DenoApprox.bot_approx [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_snd [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_fst [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_pair [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_cprod_fun_pair [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_ifz [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_bop [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_let [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_app [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_swap_app [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_abs [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_var [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_int [in Top.DenoApprox]
DenoApprox.clos_compiler_correctness_unit [in Top.DenoApprox]
DenoApprox.clos_approx_rec [in Top.DenoApprox]
DenoApprox.clos_approx_rec_n [in Top.DenoApprox]
DenoApprox.clos_realizers_Equal [in Top.DenoApprox]
DenoApprox.compiler_correctness_abs [in Top.DenoApprox]
DenoApprox.compiler_correctness_var [in Top.DenoApprox]
DenoApprox.compiler_correctness_int [in Top.DenoApprox]
DenoApprox.compiler_correctness_unit [in Top.DenoApprox]
DenoApprox.env_realizer_lookup [in Top.DenoApprox]
DenoApprox.env_realizer_realizer_cons [in Top.DenoApprox]
DenoApprox.env_realizer_extend_heap [in Top.DenoApprox]
DenoApprox.env_realizer_def [in Top.DenoApprox]
DenoApprox.env_realizer_nil [in Top.DenoApprox]
DenoApprox.env_realizer_ptr [in Top.DenoApprox]
DenoApprox.env_realizers_Equal [in Top.DenoApprox]
DenoApprox.fold_Realizer [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_snd [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_fst [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_pair [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_ifz [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_bop [in Top.DenoApprox]
DenoApprox.g_compiler_correctness_app [in Top.DenoApprox]
DenoApprox.g_bot_approx [in Top.DenoApprox]
DenoApprox.ideal_compiler_correctness [in Top.DenoApprox]
DenoApprox.ifz_conf_prop [in Top.DenoApprox]
DenoApprox.primitives_Equal [in Top.DenoApprox]
DenoApprox.primitive_realizer [in Top.DenoApprox]
DenoApprox.primitive_Equal [in Top.DenoApprox]
DenoApprox.realizers_Equal [in Top.DenoApprox]
DenoApprox.realizers_Equal' [in Top.DenoApprox]
DenoApprox.realizer_ifz [in Top.DenoApprox]
DenoApprox.realizer_push [in Top.DenoApprox]
DenoApprox.realizer_access [in Top.DenoApprox]
DenoApprox.realizer_extend_heap [in Top.DenoApprox]
DenoApprox.realizer_in_Ω [in Top.DenoApprox]
DenoApprox.r_wf_joinable [in Top.DenoApprox]
DenoApprox.r_wf_heap' [in Top.DenoApprox]
DenoApprox.r_wf_heap [in Top.DenoApprox]
DenoApprox.r_wf_find [in Top.DenoApprox]
DenoApprox.tests_ifz_NZ [in Top.DenoApprox]
DenoApprox.tests_ifz_Z [in Top.DenoApprox]
DenoApprox.tests_ifz [in Top.DenoApprox]
DenoApprox.tests_bop_3 [in Top.DenoApprox]
DenoApprox.tests_bop_2 [in Top.DenoApprox]
DenoApprox.tests_bop_1 [in Top.DenoApprox]
DenoApprox.tests_pairs_2 [in Top.DenoApprox]
DenoApprox.tests_pairs_1 [in Top.DenoApprox]
DenoApprox.tests_functional [in Top.DenoApprox]
DenoApprox.Tests_Equal [in Top.DenoApprox]
DenoApprox.Tests_Equal' [in Top.DenoApprox]
DenoApprox.tests_realizers [in Top.DenoApprox]
DenoApprox.t_wf_heap [in Top.DenoApprox]
DenoApprox.var_to_nat_lookup [in Top.DenoApprox]
DLleEpsTrans [in Top.DomainStuff]
DLleEq [in Top.DomainStuff]
DLleEqR [in Top.DomainStuff]

E

EnsembleGC.antitone [in Top.Biorthogonality]
EpsStable [in Top.DomainStuff]
EqCompat.eq_trans [in Top.Map]
EqCompat.eq_sym [in Top.Map]
EqCompat.eq_refl [in Top.Map]

F

FChainCore_mon [in Top.DomainStuff]
FChainCore_S [in Top.DomainStuff]
FChainCore_S_unfold [in Top.DomainStuff]
FChainCore_unfold [in Top.DomainStuff]
FChain_mon [in Top.DomainStuff]
FChain_S [in Top.DomainStuff]
FC_Prop [in Top.DomainStuff]
FC_lub [in Top.DomainStuff]
FC_unfold [in Top.DomainStuff]
FC_zero [in Top.DomainStuff]
FC_simpl [in Top.DomainStuff]
FstTyValVal [in Top.Semantics]

G

GCClosure.extensive [in Top.Biorthogonality]
GCClosure.idemp [in Top.Biorthogonality]
GCClosure.monotone [in Top.Biorthogonality]
GCDual.antitone [in Top.Biorthogonality]
GCFacts.comp_equality [in Top.Biorthogonality]
GCFacts.comp_extensivity [in Top.Biorthogonality]
GCFacts.function_resp [in Top.Biorthogonality]
GCFacts.function_antitone [in Top.Biorthogonality]

I

IfZIntCore_cont2 [in Top.DomainStuff]
IfZIntCore_mon2 [in Top.DomainStuff]
IfZIntCore_mon [in Top.DomainStuff]
IfZNatCore_cont2 [in Top.DomainStuff]
IfZNatCore_mon2 [in Top.DomainStuff]
IfZNatCore_mon [in Top.DomainStuff]
IfZSemInt_cont [in Top.Semantics]
IfZSem_prop [in Top.Semantics]
IfZTyValVal [in Top.Semantics]
IfZTyValVal' [in Top.Semantics]
Included_Singleton [in Top.Sets]
Included_Union_2 [in Top.Sets]
Included_Union_1 [in Top.Sets]
Included_trans [in Top.Sets]
Included_refl [in Top.Sets]
InclusionOrdered.E.eq_equiv [in Top.Biorthogonality]
InclusionOrdered.le_antisym [in Top.Biorthogonality]
InclusionOrdered.le_trans [in Top.Biorthogonality]
InclusionOrdered.le_refl [in Top.Biorthogonality]
InclusionOrdered.le_compat [in Top.Biorthogonality]

K

KLEISLIL_Eps [in Top.DomainStuff]
KLEISLIL_PBot [in Top.DomainStuff]
KLEISLIL_unit2 [in Top.DomainStuff]
KLEISLIR_Eps [in Top.DomainStuff]
KLEISLIR_KR_eq2 [in Top.DomainStuff]
KLEISLIR_KR_eq [in Top.DomainStuff]
KLEISLIR_PBot [in Top.DomainStuff]
KLEISLIR_unit2 [in Top.DomainStuff]
KLEISLI_RL_Val [in Top.DomainStuff]
KLEISLI_LR_Val [in Top.DomainStuff]
KLESILIL_lub_comp_eq [in Top.DomainStuff]
KLESILIR_lub_comp_eq [in Top.DomainStuff]
KRKUR_id2 [in Top.DomainStuff]
KRKUR_id [in Top.DomainStuff]
KURKR_id2 [in Top.DomainStuff]
KURKR_id [in Top.DomainStuff]

L

Letty_unfold [in Top.Semantics]
ListEq.eq_equiv [in Top.Map]
lub_discrete_chain [in Top.DomainStuff]

M

Machine.env_ptr_cons_included [in Top.Machine]
Machine.find_heap_range [in Top.Machine]
Machine.fresh_for_heap_join_1 [in Top.Machine]
Machine.fresh_for_heap_join [in Top.Machine]
Machine.HClos_prop' [in Top.Machine]
Machine.HClos_prop [in Top.Machine]
Machine.heaps_prop_ifz [in Top.Machine]
Machine.heap_add_prop'' [in Top.Machine]
Machine.heap_add_join_prop [in Top.Machine]
Machine.heap_add_prop_idemp''' [in Top.Machine]
Machine.heap_add_prop_idemp'' [in Top.Machine]
Machine.heap_add_prop' [in Top.Machine]
Machine.heap_ptr_Same [in Top.Machine]
Machine.heap_ptr_Included [in Top.Machine]
Machine.heap_range_Same [in Top.Machine]
Machine.heap_range_Included [in Top.Machine]
Machine.heap_range_singleton [in Top.Machine]
Machine.Joinable_fresh [in Top.Machine]
Machine.Join_fresh_add_prop [in Top.Machine]
Machine.Join_add_prop' [in Top.Machine]
Machine.Join_heap_ptr [in Top.Machine]
Machine.Join_range_ptr [in Top.Machine]
Machine.key_set_singleton [in Top.Machine]
Machine.stack_ptr_eq_2 [in Top.Machine]
Machine.stack_ptr_eq_1 [in Top.Machine]
Machine.stack_ptr_cons_included_if [in Top.Machine]
Machine.stack_ptr_cons_included_bop [in Top.Machine]
Machine.stack_ptr_cons_included2 [in Top.Machine]
Machine.stack_ptr_cons_included [in Top.Machine]
Machine.wf_add [in Top.Machine]
Machine.wf_union [in Top.Machine]
MakeMap.Joinable_join_assoc_1 [in Top.Map]
MakeMap.Joinable_join_elim_2 [in Top.Map]
MakeMap.Joinable_join_elim_1 [in Top.Map]
MakeMap.Joinable_submap_2 [in Top.Map]
MakeMap.Joinable_submap [in Top.Map]
MakeMap.Joinable_join_intro_l [in Top.Map]
MakeMap.Joinable_join_intro_r [in Top.Map]
MakeMap.Joinable_join_comm [in Top.Map]
MakeMap.Joinable_refl [in Top.Map]
MakeMap.joinable_join2 [in Top.Map]
MakeMap.joinable_join1 [in Top.Map]
MakeMap.joinable_comm [in Top.Map]
MakeMap.join_sub2 [in Top.Map]
MakeMap.join_sub1 [in Top.Map]
MakeMap.join_in2 [in Top.Map]
MakeMap.join_in1 [in Top.Map]
MakeMap.join_in [in Top.Map]
MakeMap.join_MapsTo [in Top.Map]
MakeMap.key_set_find_in [in Top.Map]
MakeMap.Submap_MapsTo [in Top.Map]
MapRaw.InA_remove [in Top.Map]
MapRaw.InA_join_1 [in Top.Map]
MapRaw.In_nil [in Top.Map]
MapRaw.join_in2 [in Top.Map]
MapRaw.join_in1 [in Top.Map]
MapRaw.join_NoDup [in Top.Map]
MapRaw.join_MapsTo [in Top.Map]
MapRaw.MapsTo_join_2_aux1 [in Top.Map]
MapRaw.MapsTo_InA [in Top.Map]
MapRaw.MapsTo_join_1 [in Top.Map]

N

none_is_not_some [in Top.Semantics]
nth_var_to_nat [in Top.Compiler]
nth_error_nil [in Top.Semantics]

O

OperApprox.bbot_down_closed [in Top.OperApprox]
OperApprox.ble [in Top.OperApprox]
OperApprox.compiler_correctness [in Top.OperApprox]
OperApprox.compiler_correctness_snd [in Top.OperApprox]
OperApprox.compiler_correctness_fst [in Top.OperApprox]
OperApprox.compiler_correctness_pair [in Top.OperApprox]
OperApprox.compiler_correctness_ifz [in Top.OperApprox]
OperApprox.compiler_correctness_bop [in Top.OperApprox]
OperApprox.compiler_correctness_app [in Top.OperApprox]
OperApprox.compiler_correctness_let [in Top.OperApprox]
OperApprox.compiler_correctness_abs [in Top.OperApprox]
OperApprox.compiler_correctness_var [in Top.OperApprox]
OperApprox.compiler_correctness_int [in Top.OperApprox]
OperApprox.compiler_correctness_unit [in Top.OperApprox]
OperApprox.env_realizer_ptr [in Top.OperApprox]
OperApprox.env_realizer_realizer_cons [in Top.OperApprox]
OperApprox.env_realizer_extend_heap [in Top.OperApprox]
OperApprox.env_realizer_gen_StepI [in Top.OperApprox]
OperApprox.env_realizer_StepI [in Top.OperApprox]
OperApprox.env_realizer_def [in Top.OperApprox]
OperApprox.env_realizer_nil [in Top.OperApprox]
OperApprox.env_realizers_Equal [in Top.OperApprox]
OperApprox.env_realizer_lookup [in Top.OperApprox]
OperApprox.ifz_conf_prop [in Top.OperApprox]
OperApprox.isatif_eq_Fullset [in Top.OperApprox]
OperApprox.isatif_down_closed [in Top.OperApprox]
OperApprox.primitive_gen_StepI [in Top.OperApprox]
OperApprox.primitive_StepI [in Top.OperApprox]
OperApprox.primitive_realizer [in Top.OperApprox]
OperApprox.primitive_Equal [in Top.OperApprox]
OperApprox.realizers_Equal' [in Top.OperApprox]
OperApprox.realizers_Equal [in Top.OperApprox]
OperApprox.realizer_push [in Top.OperApprox]
OperApprox.realizer_rec [in Top.OperApprox]
OperApprox.realizer_access [in Top.OperApprox]
OperApprox.realizer_extend_heap [in Top.OperApprox]
OperApprox.realizer_gen_StepI [in Top.OperApprox]
OperApprox.realizer_StepI [in Top.OperApprox]
OperApprox.realizer_in_Ω [in Top.OperApprox]
OperApprox.r_wf_joinable [in Top.OperApprox]
OperApprox.r_wf_heap' [in Top.OperApprox]
OperApprox.r_wf_heap [in Top.OperApprox]
OperApprox.r_wf_find [in Top.OperApprox]
OperApprox.satif_Equal1 [in Top.OperApprox]
OperApprox.tests_pairs_2 [in Top.OperApprox]
OperApprox.tests_pairs_1 [in Top.OperApprox]
OperApprox.tests_ifz [in Top.OperApprox]
OperApprox.tests_bop_2 [in Top.OperApprox]
OperApprox.tests_bop_1 [in Top.OperApprox]
OperApprox.tests_functional [in Top.OperApprox]
OperApprox.tests_bot [in Top.OperApprox]
OperApprox.Tests_Equal [in Top.OperApprox]
OperApprox.Tests_Equal' [in Top.OperApprox]
OperApprox.tests_realizers [in Top.OperApprox]
OperApprox.test_gen_StepI [in Top.OperApprox]
OperApprox.test_StepI [in Top.OperApprox]
OperApprox.t_wf_heap [in Top.OperApprox]
OperApprox.var_to_nat_lookup [in Top.OperApprox]
Operator2_strictR [in Top.DomainStuff]
Operator2_strictL [in Top.DomainStuff]

P

PairEq.eq_equiv [in Top.Map]
prod_fun_prop [in Top.Semantics]
prod_simpl [in Top.DomainStuff]

R

RUid [in Top.DomainStuff]

S

Same_set_in_iff [in Top.Sets]
Same_set_trans [in Top.Sets]
Same_set_sym [in Top.Sets]
Same_set_refl [in Top.Sets]
sem_term_app_Eq [in Top.Semantics]
sem_term_app_Eq' [in Top.Semantics]
SimpleB_cont [in Top.DomainStuff]
SimpleB_mon [in Top.DomainStuff]
SimpleU_mon [in Top.DomainStuff]
Smashs_eq [in Top.DomainStuff]
SmashValVal [in Top.Semantics]
Smash_ValVal [in Top.DomainStuff]
Smash_Val [in Top.DomainStuff]
Smash_Eps_r [in Top.DomainStuff]
Smash_Eps_l [in Top.DomainStuff]
SndTyValVal [in Top.Semantics]

U

UnCurry_cont [in Top.DomainStuff]
UnCurry_mon [in Top.DomainStuff]
Union_subset [in Top.Sets]
Union_idem [in Top.Sets]
Union_assoc [in Top.Sets]
Union_comm [in Top.Sets]
union_included [in Top.Sets]
Union_in_iff [in Top.Sets]
URid [in Top.DomainStuff]
UsualHeap.comp_join_elim_r [in Top.Map]
UsualHeap.comp_join_elim_l [in Top.Map]
UsualHeap.eqlistA_leibniz [in Top.Map]
UsualHeap.Equal_join_mor [in Top.Map]
UsualHeap.Equal_key_set [in Top.Map]
UsualHeap.Eq.eq_equiv [in Top.Map]
UsualHeap.find_singleton_Join [in Top.Map]
UsualHeap.find_singleton_Joinable [in Top.Map]
UsualHeap.find_Joinable_singleton_1 [in Top.Map]
UsualHeap.find_submap_singleton [in Top.Map]
UsualHeap.find_Equal [in Top.Map]
UsualHeap.find_submap [in Top.Map]
UsualHeap.heap_find_join_prop' [in Top.Map]
UsualHeap.heap_find_join_prop [in Top.Map]
UsualHeap.heap_add_join_prop' [in Top.Map]
UsualHeap.heap_add_prop_idemp' [in Top.Map]
UsualHeap.heap_add_prop_idemp [in Top.Map]
UsualHeap.heap_add_prop [in Top.Map]
UsualHeap.heap_add_update_prop [in Top.Map]
UsualHeap.heap_Equal [in Top.Map]
UsualHeap.heap_Equiv [in Top.Map]
UsualHeap.heap_Equiv_eq [in Top.Map]
UsualHeap.heap_eq_Equiv [in Top.Map]
UsualHeap.Joinable_not_in [in Top.Map]
UsualHeap.Joinable_Equal_1 [in Top.Map]
UsualHeap.Join_add_prop''' [in Top.Map]
UsualHeap.Join_add_prop'' [in Top.Map]
UsualHeap.Join_add_prop [in Top.Map]
UsualHeap.Join_key_set [in Top.Map]
UsualHeap.Join_add [in Top.Map]
UsualHeap.Join_idem [in Top.Map]
UsualHeap.Join_assoc_1 [in Top.Map]
UsualHeap.Join_comm_1 [in Top.Map]
UsualHeap.MapsTo_singleton [in Top.Map]
UsualHeap.pair_eq_leibniz [in Top.Map]
UsualHeap.Submap_MapsTo_leibniz [in Top.Map]

---

Axiom Index

C

ClosureOperator.extensive [in Top.Biorthogonality]
ClosureOperator.h [in Top.Biorthogonality]
ClosureOperator.idemp [in Top.Biorthogonality]
ClosureOperator.monotone [in Top.Biorthogonality]

G

GCType.antitone [in Top.Biorthogonality]
GCType.f [in Top.Biorthogonality]
GCType.g [in Top.Biorthogonality]

O

ObservationsSI.add_marker_pi2 [in Top.ObsSI]
ObservationsSI.add_marker_pi1 [in Top.ObsSI]
ObservationsSI.add_marker [in Top.ObsSI]
ObservationsSI.antiex [in Top.ObsSI]
ObservationsSI.eq_closed [in Top.ObsSI]
ObservationsSI.extend_heap [in Top.ObsSI]
ObservationsSI.stepI [in Top.ObsSI]
ObservationsSI.Ω [in Top.ObsSI]
Observations.add_marker_pi2 [in Top.Obs]
Observations.add_marker_pi1 [in Top.Obs]
Observations.add_marker [in Top.Obs]
Observations.antiex [in Top.Obs]
Observations.eq_closed [in Top.Obs]
Observations.extend_heap [in Top.Obs]
Observations.Ω [in Top.Obs]

P

PosetType.le [in Top.Biorthogonality]
PosetType.le_compat [in Top.Biorthogonality]
PosetType.le_antisym [in Top.Biorthogonality]
PosetType.le_trans [in Top.Biorthogonality]
PosetType.le_refl [in Top.Biorthogonality]

T

TstElt.Elt [in Top.Biorthogonality]
TstElt.satif [in Top.Biorthogonality]
TstElt.Tst [in Top.Biorthogonality]

W

WSfunExtended.join [in Top.Map]
WSfunExtended.Joinable [in Top.Map]
WSfunExtended.join_MapsTo [in Top.Map]
WSfunExtended.join_sub2 [in Top.Map]
WSfunExtended.join_sub1 [in Top.Map]
WSfunExtended.Submap [in Top.Map]

---

Constructor Index

I

iaccess [in Top.Machine]
ibop [in Top.Machine]
ifst [in Top.Machine]
igrab [in Top.Machine]
iifz [in Top.Machine]
iint [in Top.Machine]
ilet [in Top.Machine]
ipair [in Top.Machine]
ipush [in Top.Machine]
irec [in Top.Machine]
isnd [in Top.Machine]
iunit [in Top.Machine]
ival [in Top.Machine]

M

Machine.bopapply [in Top.Machine]
Machine.C [in Top.Machine]
Machine.IfZ [in Top.Machine]
Machine.ifzapply [in Top.Machine]
Machine.ival_update_2 [in Top.Machine]
Machine.ival_update_1 [in Top.Machine]
Machine.ival_update [in Top.Machine]
Machine.K [in Top.Machine]
Machine.mapply [in Top.Machine]
Machine.mapplypi1 [in Top.Machine]
Machine.mapplypi2 [in Top.Machine]
Machine.mupdate [in Top.Machine]
Machine.mupdatepi1 [in Top.Machine]
Machine.mupdatepi2 [in Top.Machine]
Machine.rec_eval [in Top.Machine]
Machine.taccess [in Top.Machine]
Machine.tbop_apply_3 [in Top.Machine]
Machine.tbop_apply_2 [in Top.Machine]
Machine.tbop_apply_1 [in Top.Machine]
Machine.tfst [in Top.Machine]
Machine.tgrab_apply [in Top.Machine]
Machine.tifz [in Top.Machine]
Machine.tifz_n0 [in Top.Machine]
Machine.tifz_0 [in Top.Machine]
Machine.tlet [in Top.Machine]
Machine.tpair_apply_pi2 [in Top.Machine]
Machine.tpair_apply_pi1 [in Top.Machine]
Machine.tpush [in Top.Machine]
Machine.tsnd [in Top.Machine]
Machine.ZBOpL [in Top.Machine]
Machine.ZBOpR [in Top.Machine]
MinusBOp [in Top.BOp]

P

PlusBOp [in Top.BOp]

S

svar [in Top.Syntax]

T

tarrow [in Top.Syntax]
term_snd [in Top.Syntax]
term_fst [in Top.Syntax]
term_pair [in Top.Syntax]
term_ifz [in Top.Syntax]
term_bop [in Top.Syntax]
term_let [in Top.Syntax]
term_app [in Top.Syntax]
term_abs [in Top.Syntax]
term_var [in Top.Syntax]
term_int [in Top.Syntax]
term_unit [in Top.Syntax]
tint [in Top.Syntax]
tpair [in Top.Syntax]
tunit [in Top.Syntax]

Z

zvar [in Top.Syntax]

---

Inductive Index

B

BOp [in Top.BOp]

C

Code [in Top.Machine]

M

Machine.Cont [in Top.Machine]
Machine.HeapElem [in Top.Machine]
Machine.Marker [in Top.Machine]
Machine.trans [in Top.Machine]

T

term [in Top.Syntax]
type [in Top.Syntax]

V

Val [in Top.Machine]
var [in Top.Syntax]

---

Instance Index

I

InclusionOrdered.PosetType_Compat [in Top.Biorthogonality]
InclusionOrdered.PosetType_Antisymmetric [in Top.Biorthogonality]
InclusionOrdered.PosetType_Transitive [in Top.Biorthogonality]
InclusionOrdered.PosetType_Reflexive [in Top.Biorthogonality]

P

PosetType.PosetType_Compat [in Top.Biorthogonality]
PosetType.PosetType_Antisymmetric [in Top.Biorthogonality]
PosetType.PosetType_Transitive [in Top.Biorthogonality]
PosetType.PosetType_Reflexive [in Top.Biorthogonality]

---

Section Index

M

MakeMap.JoinableDef [in Top.Map]
MakeMap.JoinDef [in Top.Map]
MakeMap.JoinSpec [in Top.Map]
MakeMap.SubmapDef [in Top.Map]

W

WSfunExtended.JoinSpec [in Top.Map]

---

Abbreviation Index

D

DenoApprox.flipIn [in Top.DenoApprox]

M

MakeMap.key_eq [in Top.Map]

O

OperApprox.flipIn [in Top.OperApprox]

---

Definition Index

A

AbsTy [in Top.Semantics]
AbsTyTrans [in Top.Semantics]
admit [in Top.Utils]
AppTy [in Top.Semantics]
AppTy_ρ [in Top.Semantics]

C

CCURRY [in Top.DomainStuff]
compile [in Top.Compiler]
cprod_fun [in Top.Semantics]
CProd_fun [in Top.Semantics]
ctx [in Top.Syntax]
ctx_denot [in Top.Semantics]
CURRY1_mon [in Top.DomainStuff]

D

DenoApprox.clos_Realizers [in Top.DenoApprox]
DenoApprox.EnvRealizers [in Top.DenoApprox]
DenoApprox.EType [in Top.DenoApprox]
DenoApprox.exists_fresh_pointer [in Top.DenoApprox]
DenoApprox.GRealizers [in Top.DenoApprox]
DenoApprox.Primitives [in Top.DenoApprox]
DenoApprox.Realizers [in Top.DenoApprox]
DenoApprox.RType [in Top.DenoApprox]
DenoApprox.r_wf [in Top.DenoApprox]
DenoApprox.satif [in Top.DenoApprox]
DenoApprox.TestRealizer.Elt [in Top.DenoApprox]
DenoApprox.TestRealizer.satif [in Top.DenoApprox]
DenoApprox.TestRealizer.Tst [in Top.DenoApprox]
DenoApprox.Tests [in Top.DenoApprox]
DenoApprox.TType [in Top.DenoApprox]
DenoApprox.t_wf [in Top.DenoApprox]

E

EnsembleGC.f [in Top.Biorthogonality]
EnsembleGC.g [in Top.Biorthogonality]
EnsembleGC.PTyp.t [in Top.Biorthogonality]
EnsembleGC.QTyp.t [in Top.Biorthogonality]
EqCompat.eq [in Top.Map]
EqCompat.t [in Top.Map]

F

FC [in Top.DomainStuff]
FChain [in Top.DomainStuff]
FChainCore [in Top.DomainStuff]
FixF [in Top.DomainStuff]

G

GCClosure.h [in Top.Biorthogonality]
GCDual.f [in Top.Biorthogonality]
GCDual.g [in Top.Biorthogonality]

H

Heap.elt [in Top.Map]
Heap.elt_pair [in Top.Map]
Heap.Heap [in Top.Map]
Heap.Pointer [in Top.Map]

I

IfZInt [in Top.DomainStuff]
IfZIntCoreM [in Top.DomainStuff]
IfZIntCoreM2 [in Top.DomainStuff]
IfZIntTy [in Top.Semantics]
IfZNat [in Top.DomainStuff]
IfZNatCoreM [in Top.DomainStuff]
IfZNatCoreM2 [in Top.DomainStuff]
IfZSemInt [in Top.DomainStuff]
IfZSemNat [in Top.DomainStuff]
InclusionOrdered.eq [in Top.Biorthogonality]
InclusionOrdered.E.eq [in Top.Biorthogonality]
InclusionOrdered.E.t [in Top.Biorthogonality]
InclusionOrdered.le [in Top.Biorthogonality]
InclusionOrdered.t [in Top.Biorthogonality]
IntOpTy [in Top.Semantics]

K

KR [in Top.DomainStuff]
KUR [in Top.DomainStuff]

L

LetTy [in Top.Semantics]
ListEq.eq [in Top.Map]
ListEq.t [in Top.Map]
lookup [in Top.Semantics]
lookup_nat [in Top.Semantics]

M

Machine.CodeTyp.t [in Top.Machine]
Machine.conf [in Top.Machine]
Machine.conf_eq [in Top.Machine]
Machine.conf_wf [in Top.Machine]
Machine.env_ptr [in Top.Machine]
Machine.fresh_for [in Top.Machine]
Machine.fresh_for_stack [in Top.Machine]
Machine.fresh_for_env [in Top.Machine]
Machine.fresh_for_heap [in Top.Machine]
Machine.HClos [in Top.Machine]
Machine.HClos_to_MClos [in Top.Machine]
Machine.heap_wf [in Top.Machine]
Machine.heap_ptr [in Top.Machine]
Machine.heap_range_ptr [in Top.Machine]
Machine.MClos [in Top.Machine]
Machine.MClos_to_HClos [in Top.Machine]
Machine.MEnv [in Top.Machine]
Machine.Pointer [in Top.Machine]
Machine.stack [in Top.Machine]
Machine.stack_ptr [in Top.Machine]
MakeMap.elt [in Top.Map]
MakeMap.heap_eq [in Top.Map]
MakeMap.join [in Top.Map]
MakeMap.Joinable [in Top.Map]
MakeMap.KeySet [in Top.Map]
MakeMap.key_set [in Top.Map]
MakeMap.SetIn [in Top.Map]
MakeMap.singleton [in Top.Map]
MakeMap.Submap [in Top.Map]
MapRaw.join [in Top.Map]

O

ObservationsSI.ConfSet [in Top.ObsSI]
ObservationsSI.SetIn [in Top.ObsSI]
Observations.ConfSet [in Top.Obs]
Observations.SetIn [in Top.Obs]
OperApprox.EnvRealizers [in Top.OperApprox]
OperApprox.EType [in Top.OperApprox]
OperApprox.exists_fresh_pointer [in Top.OperApprox]
OperApprox.GRealizers [in Top.OperApprox]
OperApprox.iRType [in Top.OperApprox]
OperApprox.isatif [in Top.OperApprox]
OperApprox.iTType [in Top.OperApprox]
OperApprox.LiftRel [in Top.OperApprox]
OperApprox.Primitives [in Top.OperApprox]
OperApprox.Realizers [in Top.OperApprox]
OperApprox.RType [in Top.OperApprox]
OperApprox.r_wf [in Top.OperApprox]
OperApprox.satif [in Top.OperApprox]
OperApprox.TestRealizer.Elt [in Top.OperApprox]
OperApprox.TestRealizer.satif [in Top.OperApprox]
OperApprox.TestRealizer.Tst [in Top.OperApprox]
OperApprox.Tests [in Top.OperApprox]
OperApprox.TType [in Top.OperApprox]
OperApprox.t_wf [in Top.OperApprox]
Operator2_reverse [in Top.DomainStuff]
OpPlus [in Top.DomainStuff]
OrthogonalOperators.bbot [in Top.Biorthogonality]
OrthogonalOperators.btop [in Top.Biorthogonality]

P

PairEq.eq [in Top.Map]
PairEq.t [in Top.Map]
PosetType.eq [in Top.Biorthogonality]
PosetType.t [in Top.Biorthogonality]

S

semZBOp [in Top.BOp]
SimpleBOp [in Top.DomainStuff]
SimpleBOpm [in Top.DomainStuff]
Smash_reverse [in Top.DomainStuff]
SwapAppTy [in Top.Semantics]
SwapArgs [in Top.DomainStuff]

T

term_denot [in Top.Semantics]
ty_denot [in Top.Semantics]
t_ty_denot [in Top.Semantics]

U

UNCURRY [in Top.DomainStuff]
UNCURRY_mon [in Top.DomainStuff]
UsualHeap.Eq.eq [in Top.Map]
UsualHeap.Eq.t [in Top.Map]

V

var_to_nat [in Top.Compiler]

W

WSfunExtended.elt [in Top.Map]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

(143 entries)

---

This page has been generated by coqdoc