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

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

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

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

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

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

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

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

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

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

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

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

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

(4 entries)

Global Index

A

aamap [definition, in oadt.lang_oadt.base]
aamap_is_finmap [instance, in oadt.lang_oadt.base]
admissible [section, in oadt.lang_oadt.admissible]
admissible [library]
any_kind_otval [lemma, in oadt.lang_oadt.values]
aset_stale [instance, in oadt.lang_oadt.infrastructure]
Atom [record, in oadt.ln]
atom_stale [instance, in oadt.lang_oadt.infrastructure]
atom_instance.is_atom [instance, in oadt.ln]
atom_instance.aset [definition, in oadt.ln]
atom_instance.amap [definition, in oadt.ln]
atom_instance.atom [definition, in oadt.ln]
atom_instance [module, in oadt.ln]
atom_dom_spec [instance, in oadt.ln]
atom_is_fresh [projection, in oadt.ln]
atom_fresh [projection, in oadt.ln]
atom_finmap_elem_of_dec [projection, in oadt.ln]
atom_elem_of_dom [projection, in oadt.ln]
atom_finmap [projection, in oadt.ln]
atom_finset [projection, in oadt.ln]
atom_infinite [projection, in oadt.ln]
atom_eq_decision [projection, in oadt.ln]
atom_finset_elements [projection, in oadt.ln]
atom_finset_difference [projection, in oadt.ln]
atom_finset_intersection [projection, in oadt.ln]
atom_finset_union [projection, in oadt.ln]
atom_finset_singleton [projection, in oadt.ln]
atom_finset_empty [projection, in oadt.ln]
atom_finset_elem_of [projection, in oadt.ln]
atom_finmap_map_fold [projection, in oadt.ln]
atom_finmap_merge [projection, in oadt.ln]
atom_finmap_omap [projection, in oadt.ln]
atom_finmap_partial_alter [projection, in oadt.ln]
atom_finmap_empty [projection, in oadt.ln]
atom_finmap_lookup [projection, in oadt.ln]
atom_finmap_fmap [projection, in oadt.ln]
atom_finmap_dom [projection, in oadt.ln]

B

base [library]
base [library]
body [definition, in oadt.lang_oadt.infrastructure]
body_bvar [lemma, in oadt.lang_oadt.infrastructure]
body_open_lc [lemma, in oadt.lang_oadt.infrastructure]
body_intro [lemma, in oadt.lang_oadt.infrastructure]
bool_semilattice [instance, in oadt.semilattice]
bool_le [instance, in oadt.semilattice]
bool_bot [instance, in oadt.semilattice]
bool_top [instance, in oadt.semilattice]
bool_join [instance, in oadt.semilattice]
bot_inv [lemma, in oadt.semilattice]
bot_lb [lemma, in oadt.semilattice]

C

canonical_form_fold [lemma, in oadt.lang_oadt.progress]
canonical_form_osum [lemma, in oadt.lang_oadt.progress]
canonical_form_sum [lemma, in oadt.lang_oadt.progress]
canonical_form_psi [lemma, in oadt.lang_oadt.progress]
canonical_form_oprod [lemma, in oadt.lang_oadt.progress]
canonical_form_prod [lemma, in oadt.lang_oadt.progress]
canonical_form_obool [lemma, in oadt.lang_oadt.progress]
canonical_form_bool [lemma, in oadt.lang_oadt.progress]
canonical_form_abs [lemma, in oadt.lang_oadt.progress]
canonical_form_unit [lemma, in oadt.lang_oadt.progress]
close [definition, in oadt.lang_oadt.infrastructure]
close [section, in oadt.lang_oadt.infrastructure]
closed [definition, in oadt.lang_oadt.infrastructure]
close_open [lemma, in oadt.lang_oadt.infrastructure]
close_fv [lemma, in oadt.lang_oadt.infrastructure]
close_fv_subseteq2 [lemma, in oadt.lang_oadt.infrastructure]
close_fv_subseteq1 [lemma, in oadt.lang_oadt.infrastructure]
close_fresh [lemma, in oadt.lang_oadt.infrastructure]
close_open_fresh_ [lemma, in oadt.lang_oadt.infrastructure]
close_ [definition, in oadt.lang_oadt.infrastructure]
oadt:{ _ <~ _ } _ [notation, in oadt.lang_oadt.infrastructure]
CtxApp1 [constructor, in oadt.lang_oadt.semantics]
CtxApp2 [constructor, in oadt.lang_oadt.semantics]
CtxCase [constructor, in oadt.lang_oadt.semantics]
CtxFold [constructor, in oadt.lang_oadt.semantics]
CtxInj [constructor, in oadt.lang_oadt.semantics]
CtxIte [constructor, in oadt.lang_oadt.semantics]
CtxLet [constructor, in oadt.lang_oadt.semantics]
CtxMux1 [constructor, in oadt.lang_oadt.semantics]
CtxMux2 [constructor, in oadt.lang_oadt.semantics]
CtxMux3 [constructor, in oadt.lang_oadt.semantics]
CtxOCase [constructor, in oadt.lang_oadt.semantics]
CtxOInj1 [constructor, in oadt.lang_oadt.semantics]
CtxOInj2 [constructor, in oadt.lang_oadt.semantics]
CtxOSum1 [constructor, in oadt.lang_oadt.semantics]
CtxOSum2 [constructor, in oadt.lang_oadt.semantics]
CtxPair1 [constructor, in oadt.lang_oadt.semantics]
CtxPair2 [constructor, in oadt.lang_oadt.semantics]
CtxProd1 [constructor, in oadt.lang_oadt.semantics]
CtxProd2 [constructor, in oadt.lang_oadt.semantics]
CtxProj [constructor, in oadt.lang_oadt.semantics]
CtxPsiPair1 [constructor, in oadt.lang_oadt.semantics]
CtxPsiPair2 [constructor, in oadt.lang_oadt.semantics]
CtxPsiProj [constructor, in oadt.lang_oadt.semantics]
CtxSec [constructor, in oadt.lang_oadt.semantics]
CtxTApp [constructor, in oadt.lang_oadt.semantics]
CtxUnfold [constructor, in oadt.lang_oadt.semantics]

D

DADT [constructor, in oadt.lang_oadt.syntax]
definitions [section, in oadt.lang_oadt.syntax]
oadt:_ ^ _ [notation, in oadt.lang_oadt.syntax]
oadt:{ _ ↦ _ } _ [notation, in oadt.lang_oadt.syntax]
oadt:{ _ ~> _ } _ [notation, in oadt.lang_oadt.syntax]
DFun [constructor, in oadt.lang_oadt.syntax]
DOADT [constructor, in oadt.lang_oadt.syntax]
DTADT [constructor, in oadt.lang_oadt.typing]
DTFun [constructor, in oadt.lang_oadt.typing]
DTOADT [constructor, in oadt.lang_oadt.typing]

E

EAbs [constructor, in oadt.lang_oadt.syntax]
EApp [constructor, in oadt.lang_oadt.syntax]
EBool [constructor, in oadt.lang_oadt.syntax]
EBoxedInj [constructor, in oadt.lang_oadt.syntax]
EBoxedLit [constructor, in oadt.lang_oadt.syntax]
EBVar [constructor, in oadt.lang_oadt.syntax]
ECase [constructor, in oadt.lang_oadt.syntax]
ectx [inductive, in oadt.lang_oadt.semantics]
EFold [constructor, in oadt.lang_oadt.syntax]
EFVar [constructor, in oadt.lang_oadt.syntax]
EGVar [constructor, in oadt.lang_oadt.syntax]
EInj [constructor, in oadt.lang_oadt.syntax]
EIte [constructor, in oadt.lang_oadt.syntax]
elem_of_subseteq_flip_proper [instance, in oadt.base]
elem_of_subseteq_proper [instance, in oadt.base]
ELet [constructor, in oadt.lang_oadt.syntax]
ELit [constructor, in oadt.lang_oadt.syntax]
EMux [constructor, in oadt.lang_oadt.syntax]
EPair [constructor, in oadt.lang_oadt.syntax]
EPi [constructor, in oadt.lang_oadt.syntax]
EProd [constructor, in oadt.lang_oadt.syntax]
EProj [constructor, in oadt.lang_oadt.syntax]
EPsi [constructor, in oadt.lang_oadt.syntax]
EPsiPair [constructor, in oadt.lang_oadt.syntax]
EPsiProj [constructor, in oadt.lang_oadt.syntax]
equivalence [section, in oadt.lang_oadt.equivalence]
equivalence [section, in oadt.lang_oadt.equivalence]
equivalence [library]
ESec [constructor, in oadt.lang_oadt.syntax]
ESum [constructor, in oadt.lang_oadt.syntax]
ETApp [constructor, in oadt.lang_oadt.syntax]
EUnfold [constructor, in oadt.lang_oadt.syntax]
EUnitT [constructor, in oadt.lang_oadt.syntax]
EUnitV [constructor, in oadt.lang_oadt.syntax]
expr [inductive, in oadt.lang_oadt.syntax]
expr_stale [instance, in oadt.lang_oadt.infrastructure]
oadt:ite _ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:[ inr < _ > _ ] [notation, in oadt.lang_oadt.syntax]
oadt:[ inl < _ > _ ] [notation, in oadt.lang_oadt.syntax]
oadt:[ inj@ _ < _ > _ ] [notation, in oadt.lang_oadt.syntax]
oadt:[ _ ] [notation, in oadt.lang_oadt.syntax]
oadt:mux _ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:unfold < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:fold < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:~case _ of _ | _ [notation, in oadt.lang_oadt.syntax]
oadt:case _ of _ | _ [notation, in oadt.lang_oadt.syntax]
oadt:case{ _ } _ of _ | _ [notation, in oadt.lang_oadt.syntax]
oadt:~inr < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:~inl < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:~inj@ _ < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inr < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inl < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inj@ _ < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inr{ _ } < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inl{ _ } < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:inj{ _ }@ _ < _ > _ [notation, in oadt.lang_oadt.syntax]
oadt:let _ in _ [notation, in oadt.lang_oadt.syntax]
oadt:if _ then _ else _ [notation, in oadt.lang_oadt.syntax]
oadt:s𝔹 _ [notation, in oadt.lang_oadt.syntax]
oadt:#π2 _ [notation, in oadt.lang_oadt.syntax]
oadt:#π1 _ [notation, in oadt.lang_oadt.syntax]
oadt:#π@ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:#( _ , _ ) [notation, in oadt.lang_oadt.syntax]
oadt:Ψ _ [notation, in oadt.lang_oadt.syntax]
oadt:~π2 _ [notation, in oadt.lang_oadt.syntax]
oadt:~π1 _ [notation, in oadt.lang_oadt.syntax]
oadt:π2 _ [notation, in oadt.lang_oadt.syntax]
oadt:π1 _ [notation, in oadt.lang_oadt.syntax]
oadt:~π@ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:π@ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:π{ _ }@ _ _ [notation, in oadt.lang_oadt.syntax]
oadt:~( _ , _ , .. , _ ) [notation, in oadt.lang_oadt.syntax]
oadt:( _ , _ , .. , _ ) [notation, in oadt.lang_oadt.syntax]
oadt:( _ , _ , .. , _ ){ _ } [notation, in oadt.lang_oadt.syntax]
oadt:() [notation, in oadt.lang_oadt.syntax]
oadt:_ @ _ [notation, in oadt.lang_oadt.syntax]
oadt:_ _ [notation, in oadt.lang_oadt.syntax]
oadt:\ : _ => _ [notation, in oadt.lang_oadt.syntax]
oadt:Π : _ , _ [notation, in oadt.lang_oadt.syntax]
oadt:_ ~+ _ [notation, in oadt.lang_oadt.syntax]
oadt:_ + _ [notation, in oadt.lang_oadt.syntax]
oadt:_ +{ _ } _ [notation, in oadt.lang_oadt.syntax]
oadt:_ ~* _ [notation, in oadt.lang_oadt.syntax]
oadt:_ * _ [notation, in oadt.lang_oadt.syntax]
oadt:_ *{ _ } _ [notation, in oadt.lang_oadt.syntax]
oadt:~Bool [notation, in oadt.lang_oadt.syntax]
oadt:~𝔹 [notation, in oadt.lang_oadt.syntax]
oadt:Bool [notation, in oadt.lang_oadt.syntax]
oadt:𝔹 [notation, in oadt.lang_oadt.syntax]
oadt:𝔹{ _ } [notation, in oadt.lang_oadt.syntax]
oadt:Unit [notation, in oadt.lang_oadt.syntax]
oadt:𝟙 [notation, in oadt.lang_oadt.syntax]
oadt:lit _ [notation, in oadt.lang_oadt.syntax]
oadt:gvar _ [notation, in oadt.lang_oadt.syntax]
oadt:fvar _ [notation, in oadt.lang_oadt.syntax]
oadt:bvar _ [notation, in oadt.lang_oadt.syntax]
oadt:_ [notation, in oadt.lang_oadt.syntax]
oadt:( _ ) [notation, in oadt.lang_oadt.syntax]
oadt:,( _ ) [notation, in oadt.lang_oadt.syntax]
<{ _ }> [notation, in oadt.lang_oadt.syntax]
expr_notations [module, in oadt.lang_oadt.syntax]
expr_eq [instance, in oadt.lang_oadt.syntax]
expr_sind [definition, in oadt.lang_oadt.syntax]
expr_rec [definition, in oadt.lang_oadt.syntax]
expr_ind [definition, in oadt.lang_oadt.syntax]
expr_rect [definition, in oadt.lang_oadt.syntax]

F

FinMapPack [record, in oadt.base]
fix_gctx [section, in oadt.lang_oadt.progress]
fix_gctx [section, in oadt.lang_oadt.progress]
fix_gctx [section, in oadt.lang_oadt.values]
fix_gctx [section, in oadt.lang_oadt.preservation]
fix_gctx [section, in oadt.lang_oadt.obliviousness]
fv [definition, in oadt.lang_oadt.infrastructure]

G

gctx [definition, in oadt.lang_oadt.syntax]
gctx_wf_closed [lemma, in oadt.lang_oadt.infrastructure]
gctx_wf [definition, in oadt.lang_oadt.typing]
gctx_typing [definition, in oadt.lang_oadt.typing]
gdef [inductive, in oadt.lang_oadt.syntax]
gdefs_typing_wf [lemma, in oadt.lang_oadt.metatheories]
gdef_typing_sind [definition, in oadt.lang_oadt.typing]
gdef_typing_ind [definition, in oadt.lang_oadt.typing]
gdef_typing [inductive, in oadt.lang_oadt.typing]

I

indistinguishable [library]
indistinguishable_deterministic [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_step [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_val_type [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_val_obliv_type_equiv [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_obliv_val [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_val [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_val_ [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_oval [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_otval_inv [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_otval [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_ovalty_inv [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_ovalty [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_open [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_subst [lemma, in oadt.lang_oadt.obliviousness]
indistinguishable_is_equiv [instance, in oadt.lang_oadt.obliviousness]
infrastructure [library]
insert_fresh_subseteq [lemma, in oadt.base]
inversion [library]

J

join_bot_iff [lemma, in oadt.semilattice]
join_lub [lemma, in oadt.semilattice]
join_prime [lemma, in oadt.semilattice]
join_ub_r [lemma, in oadt.semilattice]
join_ub_l [lemma, in oadt.semilattice]
join_right_absorb [instance, in oadt.semilattice]
join_right_id [instance, in oadt.semilattice]
join_consistent [projection, in oadt.semilattice]
join_left_absorb [projection, in oadt.semilattice]
join_left_id [projection, in oadt.semilattice]
join_idemp [projection, in oadt.semilattice]
join_assoc [projection, in oadt.semilattice]
join_comm [projection, in oadt.semilattice]

K

KAny [constructor, in oadt.lang_oadt.kind]
KApp [constructor, in oadt.lang_oadt.typing]
KBool [constructor, in oadt.lang_oadt.typing]
KCase [constructor, in oadt.lang_oadt.typing]
KCase_intro [lemma, in oadt.lang_oadt.admissible]
kernel [module, in oadt.lang_oadt.indistinguishable]
kernel.IBoxedInj [constructor, in oadt.lang_oadt.indistinguishable]
kernel.IBoxedLit [constructor, in oadt.lang_oadt.indistinguishable]
kernel.indistinguishable [inductive, in oadt.lang_oadt.indistinguishable]
kernel.indistinguishable_sind [definition, in oadt.lang_oadt.indistinguishable]
kernel.indistinguishable_ind [definition, in oadt.lang_oadt.indistinguishable]
_ ≈ _ [notation, in oadt.lang_oadt.indistinguishable]
KGVar [constructor, in oadt.lang_oadt.typing]
kind [inductive, in oadt.lang_oadt.kind]
kind [library]
kinding [inductive, in oadt.lang_oadt.typing]
kinding_progress [lemma, in oadt.lang_oadt.progress]
kinding_fv [lemma, in oadt.lang_oadt.infrastructure]
kinding_body [lemma, in oadt.lang_oadt.infrastructure]
kinding_lc [lemma, in oadt.lang_oadt.infrastructure]
kinding_preservation [lemma, in oadt.lang_oadt.preservation]
kinding_subst_conv [lemma, in oadt.lang_oadt.preservation]
kinding_open_preservation [lemma, in oadt.lang_oadt.preservation]
kinding_subst_preservation [lemma, in oadt.lang_oadt.preservation]
kinding_inv_complete [lemma, in oadt.lang_oadt.inversion]
kinding_rename [lemma, in oadt.lang_oadt.admissible]
kinding_rename_ [lemma, in oadt.lang_oadt.admissible]
kinding_weakening_insert [lemma, in oadt.lang_oadt.weakening]
kinding_weakening_empty [lemma, in oadt.lang_oadt.weakening]
kinding_weakening [lemma, in oadt.lang_oadt.weakening]
kinding_typing_ind [definition, in oadt.lang_oadt.typing]
kinding_sind [definition, in oadt.lang_oadt.typing]
kinding_ind [definition, in oadt.lang_oadt.typing]
kind_semilattice [instance, in oadt.lang_oadt.kind]
kind_bot [instance, in oadt.lang_oadt.kind]
kind_top [instance, in oadt.lang_oadt.kind]
kind_le [instance, in oadt.lang_oadt.kind]
kind_join [instance, in oadt.lang_oadt.kind]
kind_eq [instance, in oadt.lang_oadt.kind]
KIte [constructor, in oadt.lang_oadt.typing]
KLet [constructor, in oadt.lang_oadt.typing]
KLet_intro [lemma, in oadt.lang_oadt.admissible]
KMixed [constructor, in oadt.lang_oadt.kind]
KObliv [constructor, in oadt.lang_oadt.kind]
KOBool [constructor, in oadt.lang_oadt.typing]
KOProd [constructor, in oadt.lang_oadt.typing]
KOSum [constructor, in oadt.lang_oadt.typing]
KPi [constructor, in oadt.lang_oadt.typing]
KPi_intro [lemma, in oadt.lang_oadt.admissible]
KProd [constructor, in oadt.lang_oadt.typing]
KProd_intro [lemma, in oadt.lang_oadt.admissible]
KPsi [constructor, in oadt.lang_oadt.typing]
KPublic [constructor, in oadt.lang_oadt.kind]
KSub [constructor, in oadt.lang_oadt.typing]
KSum [constructor, in oadt.lang_oadt.typing]
KUnit [constructor, in oadt.lang_oadt.typing]

L

lc [inductive, in oadt.lang_oadt.syntax]
LCAbs [constructor, in oadt.lang_oadt.syntax]
LCApp [constructor, in oadt.lang_oadt.syntax]
LCBool [constructor, in oadt.lang_oadt.syntax]
LCBoxedInj [constructor, in oadt.lang_oadt.syntax]
LCBoxedLit [constructor, in oadt.lang_oadt.syntax]
LCCase [constructor, in oadt.lang_oadt.syntax]
LCFold [constructor, in oadt.lang_oadt.syntax]
LCFVar [constructor, in oadt.lang_oadt.syntax]
LCGVar [constructor, in oadt.lang_oadt.syntax]
LCInj [constructor, in oadt.lang_oadt.syntax]
LCIte [constructor, in oadt.lang_oadt.syntax]
LCLet [constructor, in oadt.lang_oadt.syntax]
LCLit [constructor, in oadt.lang_oadt.syntax]
LCMux [constructor, in oadt.lang_oadt.syntax]
LCPair [constructor, in oadt.lang_oadt.syntax]
LCPi [constructor, in oadt.lang_oadt.syntax]
LCProd [constructor, in oadt.lang_oadt.syntax]
LCProj [constructor, in oadt.lang_oadt.syntax]
LCPsi [constructor, in oadt.lang_oadt.syntax]
LCPsiPair [constructor, in oadt.lang_oadt.syntax]
LCPsiProj [constructor, in oadt.lang_oadt.syntax]
LCSec [constructor, in oadt.lang_oadt.syntax]
LCSum [constructor, in oadt.lang_oadt.syntax]
LCTApp [constructor, in oadt.lang_oadt.syntax]
LCUnfold [constructor, in oadt.lang_oadt.syntax]
LCUnitT [constructor, in oadt.lang_oadt.syntax]
LCUnitV [constructor, in oadt.lang_oadt.syntax]
lc_body [lemma, in oadt.lang_oadt.infrastructure]
lc_rename [lemma, in oadt.lang_oadt.infrastructure]
lc_sind [definition, in oadt.lang_oadt.syntax]
lc_ind [definition, in oadt.lang_oadt.syntax]
ln [library]
LObliv [abbreviation, in oadt.lang_oadt.syntax]
LPub [abbreviation, in oadt.lang_oadt.syntax]

M

metatheories [library]

N

notations [module, in oadt.lang_oadt.syntax]
notations [module, in oadt.lang_oadt.kind]
notations [module, in oadt.lang_oadt.semantics]
notations [module, in oadt.lang_oadt.indistinguishable]
notations [module, in oadt.lang_oadt.equivalence]
notations [module, in oadt.lang_oadt.typing]
oadt:_ ^ _ [notation, in oadt.lang_oadt.syntax]
oadt:_ ⊔ _ [notation, in oadt.lang_oadt.kind]
oadt:*@A [notation, in oadt.lang_oadt.kind]
oadt:*@M [notation, in oadt.lang_oadt.kind]
oadt:*@O [notation, in oadt.lang_oadt.kind]
oadt:*@P [notation, in oadt.lang_oadt.kind]
oadt:{ _ ↦ _ } _ [notation, in oadt.lang_oadt.syntax]
oadt:{ _ ~> _ } _ [notation, in oadt.lang_oadt.syntax]
_ # _ [notation, in oadt.lang_oadt.syntax]
_ -->{ _ } _ [notation, in oadt.lang_oadt.semantics]
_ -->* _ [notation, in oadt.lang_oadt.semantics]
_ -->! _ [notation, in oadt.lang_oadt.semantics]
_ ⊨ _ -->{ _ } _ [notation, in oadt.lang_oadt.semantics]
_ ⊨ _ -->* _ [notation, in oadt.lang_oadt.semantics]
_ ⊨ _ -->! _ [notation, in oadt.lang_oadt.semantics]
_ ≈ _ [notation, in oadt.lang_oadt.indistinguishable]
_ ≡ _ [notation, in oadt.lang_oadt.equivalence]
_ ⊢ _ :: _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ : _ [notation, in oadt.lang_oadt.typing]
_ ⇛* _ [notation, in oadt.lang_oadt.typing]
_ ⇛ _ [notation, in oadt.lang_oadt.typing]
_ ; _ ▷ _ [notation, in oadt.lang_oadt.typing]
_ ⊢₁ _ [notation, in oadt.lang_oadt.typing]
_ ; _ ⊢ _ :: _ [notation, in oadt.lang_oadt.typing]
_ ; _ ⊢ _ : _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ ≡ _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ ⇛* _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ ⇛ _ [notation, in oadt.lang_oadt.typing]
{ _ ↦ _ } [notation, in oadt.lang_oadt.syntax]

O

obliviousness [lemma, in oadt.lang_oadt.metatheories]
obliviousness [library]
obliviousness_step [lemma, in oadt.lang_oadt.obliviousness]
obliviousness_open_obliv_val [lemma, in oadt.lang_oadt.metatheories]
obliviousness_open [lemma, in oadt.lang_oadt.metatheories]
olabel [abbreviation, in oadt.lang_oadt.syntax]
open [definition, in oadt.lang_oadt.syntax]
open_close [lemma, in oadt.lang_oadt.infrastructure]
open_close_subst [lemma, in oadt.lang_oadt.infrastructure]
open_close_ [lemma, in oadt.lang_oadt.infrastructure]
open_fresh_atom [lemma, in oadt.lang_oadt.infrastructure]
open_fresh [lemma, in oadt.lang_oadt.infrastructure]
open_fv_r [lemma, in oadt.lang_oadt.infrastructure]
open_fv_l [lemma, in oadt.lang_oadt.infrastructure]
open_body [lemma, in oadt.lang_oadt.infrastructure]
open_respect_lc [lemma, in oadt.lang_oadt.infrastructure]
open_inj [lemma, in oadt.lang_oadt.infrastructure]
open_comm [lemma, in oadt.lang_oadt.infrastructure]
open_lc_intro [lemma, in oadt.lang_oadt.infrastructure]
open_lc [lemma, in oadt.lang_oadt.infrastructure]
open_lc_ [lemma, in oadt.lang_oadt.infrastructure]
open_preservation_lc [lemma, in oadt.lang_oadt.preservation]
open_preservation [lemma, in oadt.lang_oadt.preservation]
open_preservation_alt [lemma, in oadt.lang_oadt.preservation]
open_ [definition, in oadt.lang_oadt.syntax]
OTOBool [constructor, in oadt.lang_oadt.semantics]
OTOSum [constructor, in oadt.lang_oadt.semantics]
OTProd [constructor, in oadt.lang_oadt.semantics]
OTUnit [constructor, in oadt.lang_oadt.semantics]
otval [inductive, in oadt.lang_oadt.syntax]
otval_is_nf [lemma, in oadt.lang_oadt.values]
otval_step [lemma, in oadt.lang_oadt.values]
otval_uniq [lemma, in oadt.lang_oadt.values]
otval_closed [lemma, in oadt.lang_oadt.infrastructure]
otval_lc [lemma, in oadt.lang_oadt.infrastructure]
otval_well_kinded [lemma, in oadt.lang_oadt.infrastructure]
otval_sind [definition, in oadt.lang_oadt.syntax]
otval_ind [definition, in oadt.lang_oadt.syntax]
otval_whnf [lemma, in oadt.lang_oadt.equivalence]
oval [inductive, in oadt.lang_oadt.syntax]
ovalty [inductive, in oadt.lang_oadt.semantics]
ovalty_inhabited [lemma, in oadt.lang_oadt.values]
ovalty_intro_alt [lemma, in oadt.lang_oadt.values]
ovalty_intro [lemma, in oadt.lang_oadt.values]
ovalty_elim_alt [lemma, in oadt.lang_oadt.values]
ovalty_closed [lemma, in oadt.lang_oadt.infrastructure]
ovalty_lc2 [lemma, in oadt.lang_oadt.infrastructure]
ovalty_lc1 [lemma, in oadt.lang_oadt.infrastructure]
ovalty_lc [lemma, in oadt.lang_oadt.infrastructure]
ovalty_elim [lemma, in oadt.lang_oadt.infrastructure]
ovalty_sind [definition, in oadt.lang_oadt.semantics]
ovalty_ind [definition, in oadt.lang_oadt.semantics]
oval_val [lemma, in oadt.lang_oadt.values]
oval_closed [lemma, in oadt.lang_oadt.infrastructure]
oval_lc [lemma, in oadt.lang_oadt.infrastructure]
oval_sind [definition, in oadt.lang_oadt.syntax]
oval_ind [definition, in oadt.lang_oadt.syntax]
OVBoxedInj [constructor, in oadt.lang_oadt.syntax]
OVBoxedLit [constructor, in oadt.lang_oadt.syntax]
OVOBool [constructor, in oadt.lang_oadt.syntax]
OVOSum [constructor, in oadt.lang_oadt.syntax]
OVPair [constructor, in oadt.lang_oadt.syntax]
OVProd [constructor, in oadt.lang_oadt.syntax]
OVUnitT [constructor, in oadt.lang_oadt.syntax]
OVUnitV [constructor, in oadt.lang_oadt.syntax]

P

pack_finmap [projection, in oadt.base]
pack_finmap_map_fold [projection, in oadt.base]
pack_finmap_merge [projection, in oadt.base]
pack_finmap_omap [projection, in oadt.base]
pack_finmap_partial_alter [projection, in oadt.base]
pack_finmap_empty [projection, in oadt.base]
pack_finmap_lookup [projection, in oadt.base]
pack_finmap_fmap [projection, in oadt.base]
pack_finmap_decision [projection, in oadt.base]
pared [inductive, in oadt.lang_oadt.typing]
pared_equiv_obliv_preservation [lemma, in oadt.lang_oadt.progress]
pared_obliv_preservation_inv [lemma, in oadt.lang_oadt.progress]
pared_lc [lemma, in oadt.lang_oadt.infrastructure]
pared_lc2 [lemma, in oadt.lang_oadt.infrastructure]
pared_lc1 [lemma, in oadt.lang_oadt.infrastructure]
pared_kinding_preservation [lemma, in oadt.lang_oadt.preservation]
pared_preservation [lemma, in oadt.lang_oadt.preservation]
pared_preservation_ [lemma, in oadt.lang_oadt.preservation]
pared_equiv_weakening [lemma, in oadt.lang_oadt.weakening]
pared_weakening [lemma, in oadt.lang_oadt.weakening]
pared_equiv_congr_psiproj [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_congr_TApp [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_congr_pi [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_congr_inj [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_congr_sum [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_congr_prod [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_open [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_open2 [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_open1 [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_rename [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_subst [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_subst2 [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_subst1 [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_step [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_pared [lemma, in oadt.lang_oadt.equivalence]
pared_step [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_whnf_equiv [lemma, in oadt.lang_oadt.equivalence]
pared_whnf_equiv [lemma, in oadt.lang_oadt.equivalence]
pared_whnf [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_rtsc [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_is_trans [instance, in oadt.lang_oadt.equivalence]
pared_equiv_iff_join [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_is_symm [instance, in oadt.lang_oadt.equivalence]
pared_equiv_is_refl [instance, in oadt.lang_oadt.equivalence]
pared_confluent [lemma, in oadt.lang_oadt.equivalence]
pared_diamond [lemma, in oadt.lang_oadt.equivalence]
pared_inv_inj [lemma, in oadt.lang_oadt.equivalence]
pared_inv_fold [lemma, in oadt.lang_oadt.equivalence]
pared_inv_psipair [lemma, in oadt.lang_oadt.equivalence]
pared_inv_pair [lemma, in oadt.lang_oadt.equivalence]
pared_inv_abs [lemma, in oadt.lang_oadt.equivalence]
pared_rename [lemma, in oadt.lang_oadt.equivalence]
pared_open1 [lemma, in oadt.lang_oadt.equivalence]
pared_open [lemma, in oadt.lang_oadt.equivalence]
pared_subst [lemma, in oadt.lang_oadt.equivalence]
pared_subst_ [lemma, in oadt.lang_oadt.equivalence]
pared_subst1 [lemma, in oadt.lang_oadt.equivalence]
pared_subst1_ [lemma, in oadt.lang_oadt.equivalence]
pared_otval [lemma, in oadt.lang_oadt.equivalence]
pared_oval [lemma, in oadt.lang_oadt.equivalence]
pared_equiv_join [definition, in oadt.lang_oadt.typing]
pared_equiv_sind [definition, in oadt.lang_oadt.typing]
pared_equiv_ind [definition, in oadt.lang_oadt.typing]
pared_equiv [inductive, in oadt.lang_oadt.typing]
pared_sind [definition, in oadt.lang_oadt.typing]
pared_ind [definition, in oadt.lang_oadt.typing]
prelude [library]
preservation [lemma, in oadt.lang_oadt.preservation]
preservation [library]
program [abbreviation, in oadt.lang_oadt.syntax]
program_typing [definition, in oadt.lang_oadt.typing]
progress [lemma, in oadt.lang_oadt.progress]
progress [library]
progress_ [lemma, in oadt.lang_oadt.progress]

Q

QRRedL [constructor, in oadt.lang_oadt.typing]
QRRedR [constructor, in oadt.lang_oadt.typing]
QRRefl [constructor, in oadt.lang_oadt.typing]

R

RApp [constructor, in oadt.lang_oadt.typing]
RApp_intro [lemma, in oadt.lang_oadt.equivalence]
RCase [constructor, in oadt.lang_oadt.typing]
RCase_intro [lemma, in oadt.lang_oadt.equivalence]
RCgrAbs [constructor, in oadt.lang_oadt.typing]
RCgrAbs_intro [lemma, in oadt.lang_oadt.equivalence]
RCgrApp [constructor, in oadt.lang_oadt.typing]
RCgrCase [constructor, in oadt.lang_oadt.typing]
RCgrCase_intro [lemma, in oadt.lang_oadt.equivalence]
RCgrFold [constructor, in oadt.lang_oadt.typing]
RCgrInj [constructor, in oadt.lang_oadt.typing]
RCgrIte [constructor, in oadt.lang_oadt.typing]
RCgrLet [constructor, in oadt.lang_oadt.typing]
RCgrMux [constructor, in oadt.lang_oadt.typing]
RCgrPair [constructor, in oadt.lang_oadt.typing]
RCgrPi [constructor, in oadt.lang_oadt.typing]
RCgrPi_intro [lemma, in oadt.lang_oadt.equivalence]
RCgrProd [constructor, in oadt.lang_oadt.typing]
RCgrProj [constructor, in oadt.lang_oadt.typing]
RCgrPsiPair [constructor, in oadt.lang_oadt.typing]
RCgrPsiProj [constructor, in oadt.lang_oadt.typing]
RCgrSec [constructor, in oadt.lang_oadt.typing]
RCgrSum [constructor, in oadt.lang_oadt.typing]
RCgrTApp [constructor, in oadt.lang_oadt.typing]
RCgrUnfold [constructor, in oadt.lang_oadt.typing]
regularity [lemma, in oadt.lang_oadt.preservation]
RFun [constructor, in oadt.lang_oadt.typing]
RIte [constructor, in oadt.lang_oadt.typing]
RLet [constructor, in oadt.lang_oadt.typing]
RLet_intro [lemma, in oadt.lang_oadt.equivalence]
RMux [constructor, in oadt.lang_oadt.typing]
ROCase [constructor, in oadt.lang_oadt.typing]
ROCase_intro [lemma, in oadt.lang_oadt.equivalence]
ROInj [constructor, in oadt.lang_oadt.typing]
RProj [constructor, in oadt.lang_oadt.typing]
RPsiProj [constructor, in oadt.lang_oadt.typing]
RRefl [constructor, in oadt.lang_oadt.typing]
RSec [constructor, in oadt.lang_oadt.typing]
RTApp [constructor, in oadt.lang_oadt.typing]
rtc_preserve [lemma, in oadt.base]
RUnfold [constructor, in oadt.lang_oadt.typing]

S

SApp [constructor, in oadt.lang_oadt.semantics]
SCase [constructor, in oadt.lang_oadt.semantics]
SCtx [constructor, in oadt.lang_oadt.semantics]
SCtx_intro [lemma, in oadt.lang_oadt.infrastructure]
semantics [library]
SemiLattice [record, in oadt.semilattice]
semilattice [library]
semilattice_is_po [instance, in oadt.semilattice]
set [section, in oadt.base]
SFun [constructor, in oadt.lang_oadt.semantics]
SIte [constructor, in oadt.lang_oadt.semantics]
SLet [constructor, in oadt.lang_oadt.semantics]
SMux [constructor, in oadt.lang_oadt.semantics]
SOCase [constructor, in oadt.lang_oadt.semantics]
SOInj [constructor, in oadt.lang_oadt.semantics]
soundness [lemma, in oadt.lang_oadt.metatheories]
SProj [constructor, in oadt.lang_oadt.semantics]
SPsiProj [constructor, in oadt.lang_oadt.semantics]
SSec [constructor, in oadt.lang_oadt.semantics]
stale [projection, in oadt.ln]
Stale [record, in oadt.ln]
stale [constructor, in oadt.ln]
Stale [inductive, in oadt.ln]
STApp [constructor, in oadt.lang_oadt.semantics]
step [inductive, in oadt.lang_oadt.semantics]
step [section, in oadt.lang_oadt.semantics]
step_sind [definition, in oadt.lang_oadt.semantics]
step_ind [definition, in oadt.lang_oadt.semantics]
_ -->! _ [notation, in oadt.lang_oadt.semantics]
stuck [definition, in oadt.lang_oadt.metatheories]
subst [definition, in oadt.lang_oadt.syntax]
subst_tctx_fresh [lemma, in oadt.lang_oadt.infrastructure]
subst_fv [lemma, in oadt.lang_oadt.infrastructure]
subst_respect_lc [lemma, in oadt.lang_oadt.infrastructure]
subst_lc [lemma, in oadt.lang_oadt.infrastructure]
subst_intro [lemma, in oadt.lang_oadt.infrastructure]
subst_tctx_id [lemma, in oadt.lang_oadt.infrastructure]
subst_id [lemma, in oadt.lang_oadt.infrastructure]
subst_ite_distr [lemma, in oadt.lang_oadt.infrastructure]
subst_trans [lemma, in oadt.lang_oadt.infrastructure]
subst_open_comm [lemma, in oadt.lang_oadt.infrastructure]
subst_open_distr [lemma, in oadt.lang_oadt.infrastructure]
subst_fresh [lemma, in oadt.lang_oadt.infrastructure]
subst_conv [lemma, in oadt.lang_oadt.preservation]
subst_conv_ [lemma, in oadt.lang_oadt.preservation]
subst_preservation [lemma, in oadt.lang_oadt.preservation]
subst_preservation_ [lemma, in oadt.lang_oadt.preservation]
subst_tctx_typing [lemma, in oadt.lang_oadt.preservation]
subst_tctx_typing_kinding_ [lemma, in oadt.lang_oadt.preservation]
SUnfold [constructor, in oadt.lang_oadt.semantics]
syntax [library]

T

TAbs [constructor, in oadt.lang_oadt.typing]
TAbs_intro [lemma, in oadt.lang_oadt.admissible]
tactics [library]
TApp [constructor, in oadt.lang_oadt.typing]
TBoxedInj [constructor, in oadt.lang_oadt.typing]
TBoxedLit [constructor, in oadt.lang_oadt.typing]
TCase [constructor, in oadt.lang_oadt.typing]
TCase_intro [lemma, in oadt.lang_oadt.admissible]
TConv [constructor, in oadt.lang_oadt.typing]
tctx [abbreviation, in oadt.lang_oadt.typing]
tctx_stale_inv [lemma, in oadt.lang_oadt.infrastructure]
tctx_fv_insert [lemma, in oadt.lang_oadt.infrastructure]
tctx_fv_insert_subseteq [lemma, in oadt.lang_oadt.infrastructure]
tctx_fv_subseteq [lemma, in oadt.lang_oadt.infrastructure]
tctx_fv_consistent [lemma, in oadt.lang_oadt.infrastructure]
tctx_stale [instance, in oadt.lang_oadt.infrastructure]
tctx_fv [definition, in oadt.lang_oadt.infrastructure]
TFold [constructor, in oadt.lang_oadt.typing]
TFVar [constructor, in oadt.lang_oadt.typing]
TGVar [constructor, in oadt.lang_oadt.typing]
theorems [section, in oadt.semilattice]
TInj [constructor, in oadt.lang_oadt.typing]
TIte [constructor, in oadt.lang_oadt.typing]
TLet [constructor, in oadt.lang_oadt.typing]
TLet_intro [lemma, in oadt.lang_oadt.admissible]
TLit [constructor, in oadt.lang_oadt.typing]
TMux [constructor, in oadt.lang_oadt.typing]
TOCase [constructor, in oadt.lang_oadt.typing]
TOCase_intro [lemma, in oadt.lang_oadt.admissible]
TOInj [constructor, in oadt.lang_oadt.typing]
TOPair [constructor, in oadt.lang_oadt.typing]
TOProj [constructor, in oadt.lang_oadt.typing]
top_inv [lemma, in oadt.semilattice]
top_ub [lemma, in oadt.semilattice]
TPair [constructor, in oadt.lang_oadt.typing]
TProj [constructor, in oadt.lang_oadt.typing]
TPsiPair [constructor, in oadt.lang_oadt.typing]
TPsiProj1 [constructor, in oadt.lang_oadt.typing]
TPsiProj2 [constructor, in oadt.lang_oadt.typing]
trace_indistinguishable [definition, in oadt.lang_oadt.metatheories]
TSec [constructor, in oadt.lang_oadt.typing]
TUnfold [constructor, in oadt.lang_oadt.typing]
TUnit [constructor, in oadt.lang_oadt.typing]
typing [inductive, in oadt.lang_oadt.typing]
typing [section, in oadt.lang_oadt.typing]
typing [library]
typing_type_fv [lemma, in oadt.lang_oadt.infrastructure]
typing_fv [lemma, in oadt.lang_oadt.infrastructure]
typing_kinding_fv [lemma, in oadt.lang_oadt.infrastructure]
typing_type_lc [lemma, in oadt.lang_oadt.infrastructure]
typing_body [lemma, in oadt.lang_oadt.infrastructure]
typing_lc [lemma, in oadt.lang_oadt.infrastructure]
typing_inv_complete [lemma, in oadt.lang_oadt.inversion]
typing_rename_lc [lemma, in oadt.lang_oadt.admissible]
typing_rename [lemma, in oadt.lang_oadt.admissible]
typing_rename_alt [lemma, in oadt.lang_oadt.admissible]
typing_rename_ [lemma, in oadt.lang_oadt.admissible]
typing_kinding_rename_ [lemma, in oadt.lang_oadt.admissible]
typing_kinding_ind [definition, in oadt.lang_oadt.typing]
typing_sind [definition, in oadt.lang_oadt.typing]
typing_ind [definition, in oadt.lang_oadt.typing]
_ ⊢ _ :: _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ : _ [notation, in oadt.lang_oadt.typing]
_ ≡ _ [notation, in oadt.lang_oadt.typing]
_ ⇛* _ [notation, in oadt.lang_oadt.typing]
_ ⇛ _ [notation, in oadt.lang_oadt.typing]
typing.fix_gctx [section, in oadt.lang_oadt.typing]
_ ⊢₁ _ [notation, in oadt.lang_oadt.typing]
_ ; _ ⊢ _ :: _ [notation, in oadt.lang_oadt.typing]
_ ; _ ⊢ _ : _ [notation, in oadt.lang_oadt.typing]
_ ⊢ _ ≡ _ [notation, in oadt.lang_oadt.typing]

U

union_subseteq_flip_proper [instance, in oadt.base]
union_subseteq_proper [instance, in oadt.base]

V

VAbs [constructor, in oadt.lang_oadt.syntax]
val [inductive, in oadt.lang_oadt.syntax]
values [library]
val_oval [lemma, in oadt.lang_oadt.progress]
val_is_nf [lemma, in oadt.lang_oadt.values]
val_step [lemma, in oadt.lang_oadt.values]
val_otval [lemma, in oadt.lang_oadt.values]
val_sind [definition, in oadt.lang_oadt.syntax]
val_ind [definition, in oadt.lang_oadt.syntax]
VFold [constructor, in oadt.lang_oadt.syntax]
VInj [constructor, in oadt.lang_oadt.syntax]
VLit [constructor, in oadt.lang_oadt.syntax]
VOVal [constructor, in oadt.lang_oadt.syntax]
VPair [constructor, in oadt.lang_oadt.syntax]
VPsiPair [constructor, in oadt.lang_oadt.syntax]

W

WADT [constructor, in oadt.lang_oadt.equivalence]
WBool [constructor, in oadt.lang_oadt.equivalence]
weakening [lemma, in oadt.lang_oadt.weakening]
weakening [library]
weakening_insert [lemma, in oadt.lang_oadt.weakening]
weakening_empty [lemma, in oadt.lang_oadt.weakening]
weakening_ [lemma, in oadt.lang_oadt.weakening]
whnf [inductive, in oadt.lang_oadt.equivalence]
whnf_equiv_is_symm [instance, in oadt.lang_oadt.equivalence]
whnf_equiv_sind [definition, in oadt.lang_oadt.equivalence]
whnf_equiv_ind [definition, in oadt.lang_oadt.equivalence]
whnf_equiv [inductive, in oadt.lang_oadt.equivalence]
whnf_sind [definition, in oadt.lang_oadt.equivalence]
whnf_ind [definition, in oadt.lang_oadt.equivalence]
WPi [constructor, in oadt.lang_oadt.equivalence]
WProd [constructor, in oadt.lang_oadt.equivalence]
WPsi [constructor, in oadt.lang_oadt.equivalence]
WQADT [constructor, in oadt.lang_oadt.equivalence]
WQBool [constructor, in oadt.lang_oadt.equivalence]
WQPi [constructor, in oadt.lang_oadt.equivalence]
WQProd [constructor, in oadt.lang_oadt.equivalence]
WQPsi [constructor, in oadt.lang_oadt.equivalence]
WQSum [constructor, in oadt.lang_oadt.equivalence]
WQUnitT [constructor, in oadt.lang_oadt.equivalence]
WSum [constructor, in oadt.lang_oadt.equivalence]
WUnitT [constructor, in oadt.lang_oadt.equivalence]

other

' _ <- _ ; _ (stdpp_scope) [notation, in oadt.base]
_ <- _ ; _ (stdpp_scope) [notation, in oadt.base]
_ >>= _ (stdpp_scope) [notation, in oadt.base]

Notation Index

C

oadt:{ _ <~ _ } _ [in oadt.lang_oadt.infrastructure]

D

oadt:_ ^ _ [in oadt.lang_oadt.syntax]
oadt:{ _ ↦ _ } _ [in oadt.lang_oadt.syntax]
oadt:{ _ ~> _ } _ [in oadt.lang_oadt.syntax]

E

oadt:ite _ _ _ [in oadt.lang_oadt.syntax]
oadt:[ inr < _ > _ ] [in oadt.lang_oadt.syntax]
oadt:[ inl < _ > _ ] [in oadt.lang_oadt.syntax]
oadt:[ inj@ _ < _ > _ ] [in oadt.lang_oadt.syntax]
oadt:[ _ ] [in oadt.lang_oadt.syntax]
oadt:mux _ _ _ [in oadt.lang_oadt.syntax]
oadt:unfold < _ > _ [in oadt.lang_oadt.syntax]
oadt:fold < _ > _ [in oadt.lang_oadt.syntax]
oadt:~case _ of _ | _ [in oadt.lang_oadt.syntax]
oadt:case _ of _ | _ [in oadt.lang_oadt.syntax]
oadt:case{ _ } _ of _ | _ [in oadt.lang_oadt.syntax]
oadt:~inr < _ > _ [in oadt.lang_oadt.syntax]
oadt:~inl < _ > _ [in oadt.lang_oadt.syntax]
oadt:~inj@ _ < _ > _ [in oadt.lang_oadt.syntax]
oadt:inr < _ > _ [in oadt.lang_oadt.syntax]
oadt:inl < _ > _ [in oadt.lang_oadt.syntax]
oadt:inj@ _ < _ > _ [in oadt.lang_oadt.syntax]
oadt:inr{ _ } < _ > _ [in oadt.lang_oadt.syntax]
oadt:inl{ _ } < _ > _ [in oadt.lang_oadt.syntax]
oadt:inj{ _ }@ _ < _ > _ [in oadt.lang_oadt.syntax]
oadt:let _ in _ [in oadt.lang_oadt.syntax]
oadt:if _ then _ else _ [in oadt.lang_oadt.syntax]
oadt:s𝔹 _ [in oadt.lang_oadt.syntax]
oadt:#π2 _ [in oadt.lang_oadt.syntax]
oadt:#π1 _ [in oadt.lang_oadt.syntax]
oadt:#π@ _ _ [in oadt.lang_oadt.syntax]
oadt:#( _ , _ ) [in oadt.lang_oadt.syntax]
oadt:Ψ _ [in oadt.lang_oadt.syntax]
oadt:~π2 _ [in oadt.lang_oadt.syntax]
oadt:~π1 _ [in oadt.lang_oadt.syntax]
oadt:π2 _ [in oadt.lang_oadt.syntax]
oadt:π1 _ [in oadt.lang_oadt.syntax]
oadt:~π@ _ _ [in oadt.lang_oadt.syntax]
oadt:π@ _ _ [in oadt.lang_oadt.syntax]
oadt:π{ _ }@ _ _ [in oadt.lang_oadt.syntax]
oadt:~( _ , _ , .. , _ ) [in oadt.lang_oadt.syntax]
oadt:( _ , _ , .. , _ ) [in oadt.lang_oadt.syntax]
oadt:( _ , _ , .. , _ ){ _ } [in oadt.lang_oadt.syntax]
oadt:() [in oadt.lang_oadt.syntax]
oadt:_ @ _ [in oadt.lang_oadt.syntax]
oadt:_ _ [in oadt.lang_oadt.syntax]
oadt:\ : _ => _ [in oadt.lang_oadt.syntax]
oadt:Π : _ , _ [in oadt.lang_oadt.syntax]
oadt:_ ~+ _ [in oadt.lang_oadt.syntax]
oadt:_ + _ [in oadt.lang_oadt.syntax]
oadt:_ +{ _ } _ [in oadt.lang_oadt.syntax]
oadt:_ ~* _ [in oadt.lang_oadt.syntax]
oadt:_ * _ [in oadt.lang_oadt.syntax]
oadt:_ *{ _ } _ [in oadt.lang_oadt.syntax]
oadt:~Bool [in oadt.lang_oadt.syntax]
oadt:~𝔹 [in oadt.lang_oadt.syntax]
oadt:Bool [in oadt.lang_oadt.syntax]
oadt:𝔹 [in oadt.lang_oadt.syntax]
oadt:𝔹{ _ } [in oadt.lang_oadt.syntax]
oadt:Unit [in oadt.lang_oadt.syntax]
oadt:𝟙 [in oadt.lang_oadt.syntax]
oadt:lit _ [in oadt.lang_oadt.syntax]
oadt:gvar _ [in oadt.lang_oadt.syntax]
oadt:fvar _ [in oadt.lang_oadt.syntax]
oadt:bvar _ [in oadt.lang_oadt.syntax]
oadt:_ [in oadt.lang_oadt.syntax]
oadt:( _ ) [in oadt.lang_oadt.syntax]
oadt:,( _ ) [in oadt.lang_oadt.syntax]
<{ _ }> [in oadt.lang_oadt.syntax]

K

_ ≈ _ [in oadt.lang_oadt.indistinguishable]

N

oadt:_ ^ _ [in oadt.lang_oadt.syntax]
oadt:_ ⊔ _ [in oadt.lang_oadt.kind]
oadt:*@A [in oadt.lang_oadt.kind]
oadt:*@M [in oadt.lang_oadt.kind]
oadt:*@O [in oadt.lang_oadt.kind]
oadt:*@P [in oadt.lang_oadt.kind]
oadt:{ _ ↦ _ } _ [in oadt.lang_oadt.syntax]
oadt:{ _ ~> _ } _ [in oadt.lang_oadt.syntax]
_ # _ [in oadt.lang_oadt.syntax]
_ -->{ _ } _ [in oadt.lang_oadt.semantics]
_ -->* _ [in oadt.lang_oadt.semantics]
_ -->! _ [in oadt.lang_oadt.semantics]
_ ⊨ _ -->{ _ } _ [in oadt.lang_oadt.semantics]
_ ⊨ _ -->* _ [in oadt.lang_oadt.semantics]
_ ⊨ _ -->! _ [in oadt.lang_oadt.semantics]
_ ≈ _ [in oadt.lang_oadt.indistinguishable]
_ ≡ _ [in oadt.lang_oadt.equivalence]
_ ⊢ _ :: _ [in oadt.lang_oadt.typing]
_ ⊢ _ : _ [in oadt.lang_oadt.typing]
_ ⇛* _ [in oadt.lang_oadt.typing]
_ ⇛ _ [in oadt.lang_oadt.typing]
_ ; _ ▷ _ [in oadt.lang_oadt.typing]
_ ⊢₁ _ [in oadt.lang_oadt.typing]
_ ; _ ⊢ _ :: _ [in oadt.lang_oadt.typing]
_ ; _ ⊢ _ : _ [in oadt.lang_oadt.typing]
_ ⊢ _ ≡ _ [in oadt.lang_oadt.typing]
_ ⊢ _ ⇛* _ [in oadt.lang_oadt.typing]
_ ⊢ _ ⇛ _ [in oadt.lang_oadt.typing]
{ _ ↦ _ } [in oadt.lang_oadt.syntax]

S

_ -->! _ [in oadt.lang_oadt.semantics]

T

_ ⊢ _ :: _ [in oadt.lang_oadt.typing]
_ ⊢ _ : _ [in oadt.lang_oadt.typing]
_ ≡ _ [in oadt.lang_oadt.typing]
_ ⇛* _ [in oadt.lang_oadt.typing]
_ ⇛ _ [in oadt.lang_oadt.typing]
_ ⊢₁ _ [in oadt.lang_oadt.typing]
_ ; _ ⊢ _ :: _ [in oadt.lang_oadt.typing]
_ ; _ ⊢ _ : _ [in oadt.lang_oadt.typing]
_ ⊢ _ ≡ _ [in oadt.lang_oadt.typing]

other

' _ <- _ ; _ (stdpp_scope) [in oadt.base]
_ <- _ ; _ (stdpp_scope) [in oadt.base]
_ >>= _ (stdpp_scope) [in oadt.base]

Module Index

A

atom_instance [in oadt.ln]

E

expr_notations [in oadt.lang_oadt.syntax]

K

kernel [in oadt.lang_oadt.indistinguishable]

N

notations [in oadt.lang_oadt.syntax]
notations [in oadt.lang_oadt.kind]
notations [in oadt.lang_oadt.semantics]
notations [in oadt.lang_oadt.indistinguishable]
notations [in oadt.lang_oadt.equivalence]
notations [in oadt.lang_oadt.typing]

Library Index

A

admissible

B

base
base

E

equivalence

I

indistinguishable
infrastructure
inversion

K

kind

L

ln

M

metatheories

O

obliviousness

P

prelude
preservation
progress

S

semantics
semilattice
syntax

T

tactics
typing

V

values

W

weakening

Lemma Index

A

any_kind_otval [in oadt.lang_oadt.values]

B

body_bvar [in oadt.lang_oadt.infrastructure]
body_open_lc [in oadt.lang_oadt.infrastructure]
body_intro [in oadt.lang_oadt.infrastructure]
bot_inv [in oadt.semilattice]
bot_lb [in oadt.semilattice]

C

canonical_form_fold [in oadt.lang_oadt.progress]
canonical_form_osum [in oadt.lang_oadt.progress]
canonical_form_sum [in oadt.lang_oadt.progress]
canonical_form_psi [in oadt.lang_oadt.progress]
canonical_form_oprod [in oadt.lang_oadt.progress]
canonical_form_prod [in oadt.lang_oadt.progress]
canonical_form_obool [in oadt.lang_oadt.progress]
canonical_form_bool [in oadt.lang_oadt.progress]
canonical_form_abs [in oadt.lang_oadt.progress]
canonical_form_unit [in oadt.lang_oadt.progress]
close_open [in oadt.lang_oadt.infrastructure]
close_fv [in oadt.lang_oadt.infrastructure]
close_fv_subseteq2 [in oadt.lang_oadt.infrastructure]
close_fv_subseteq1 [in oadt.lang_oadt.infrastructure]
close_fresh [in oadt.lang_oadt.infrastructure]
close_open_fresh_ [in oadt.lang_oadt.infrastructure]

G

gctx_wf_closed [in oadt.lang_oadt.infrastructure]
gdefs_typing_wf [in oadt.lang_oadt.metatheories]

I

indistinguishable_deterministic [in oadt.lang_oadt.obliviousness]
indistinguishable_step [in oadt.lang_oadt.obliviousness]
indistinguishable_val_type [in oadt.lang_oadt.obliviousness]
indistinguishable_val_obliv_type_equiv [in oadt.lang_oadt.obliviousness]
indistinguishable_obliv_val [in oadt.lang_oadt.obliviousness]
indistinguishable_val [in oadt.lang_oadt.obliviousness]
indistinguishable_val_ [in oadt.lang_oadt.obliviousness]
indistinguishable_oval [in oadt.lang_oadt.obliviousness]
indistinguishable_otval_inv [in oadt.lang_oadt.obliviousness]
indistinguishable_otval [in oadt.lang_oadt.obliviousness]
indistinguishable_ovalty_inv [in oadt.lang_oadt.obliviousness]
indistinguishable_ovalty [in oadt.lang_oadt.obliviousness]
indistinguishable_open [in oadt.lang_oadt.obliviousness]
indistinguishable_subst [in oadt.lang_oadt.obliviousness]
insert_fresh_subseteq [in oadt.base]

J

join_bot_iff [in oadt.semilattice]
join_lub [in oadt.semilattice]
join_prime [in oadt.semilattice]
join_ub_r [in oadt.semilattice]
join_ub_l [in oadt.semilattice]

K

KCase_intro [in oadt.lang_oadt.admissible]
kinding_progress [in oadt.lang_oadt.progress]
kinding_fv [in oadt.lang_oadt.infrastructure]
kinding_body [in oadt.lang_oadt.infrastructure]
kinding_lc [in oadt.lang_oadt.infrastructure]
kinding_preservation [in oadt.lang_oadt.preservation]
kinding_subst_conv [in oadt.lang_oadt.preservation]
kinding_open_preservation [in oadt.lang_oadt.preservation]
kinding_subst_preservation [in oadt.lang_oadt.preservation]
kinding_inv_complete [in oadt.lang_oadt.inversion]
kinding_rename [in oadt.lang_oadt.admissible]
kinding_rename_ [in oadt.lang_oadt.admissible]
kinding_weakening_insert [in oadt.lang_oadt.weakening]
kinding_weakening_empty [in oadt.lang_oadt.weakening]
kinding_weakening [in oadt.lang_oadt.weakening]
KLet_intro [in oadt.lang_oadt.admissible]
KPi_intro [in oadt.lang_oadt.admissible]
KProd_intro [in oadt.lang_oadt.admissible]

L

lc_body [in oadt.lang_oadt.infrastructure]
lc_rename [in oadt.lang_oadt.infrastructure]

O

obliviousness [in oadt.lang_oadt.metatheories]
obliviousness_step [in oadt.lang_oadt.obliviousness]
obliviousness_open_obliv_val [in oadt.lang_oadt.metatheories]
obliviousness_open [in oadt.lang_oadt.metatheories]
open_close [in oadt.lang_oadt.infrastructure]
open_close_subst [in oadt.lang_oadt.infrastructure]
open_close_ [in oadt.lang_oadt.infrastructure]
open_fresh_atom [in oadt.lang_oadt.infrastructure]
open_fresh [in oadt.lang_oadt.infrastructure]
open_fv_r [in oadt.lang_oadt.infrastructure]
open_fv_l [in oadt.lang_oadt.infrastructure]
open_body [in oadt.lang_oadt.infrastructure]
open_respect_lc [in oadt.lang_oadt.infrastructure]
open_inj [in oadt.lang_oadt.infrastructure]
open_comm [in oadt.lang_oadt.infrastructure]
open_lc_intro [in oadt.lang_oadt.infrastructure]
open_lc [in oadt.lang_oadt.infrastructure]
open_lc_ [in oadt.lang_oadt.infrastructure]
open_preservation_lc [in oadt.lang_oadt.preservation]
open_preservation [in oadt.lang_oadt.preservation]
open_preservation_alt [in oadt.lang_oadt.preservation]
otval_is_nf [in oadt.lang_oadt.values]
otval_step [in oadt.lang_oadt.values]
otval_uniq [in oadt.lang_oadt.values]
otval_closed [in oadt.lang_oadt.infrastructure]
otval_lc [in oadt.lang_oadt.infrastructure]
otval_well_kinded [in oadt.lang_oadt.infrastructure]
otval_whnf [in oadt.lang_oadt.equivalence]
ovalty_inhabited [in oadt.lang_oadt.values]
ovalty_intro_alt [in oadt.lang_oadt.values]
ovalty_intro [in oadt.lang_oadt.values]
ovalty_elim_alt [in oadt.lang_oadt.values]
ovalty_closed [in oadt.lang_oadt.infrastructure]
ovalty_lc2 [in oadt.lang_oadt.infrastructure]
ovalty_lc1 [in oadt.lang_oadt.infrastructure]
ovalty_lc [in oadt.lang_oadt.infrastructure]
ovalty_elim [in oadt.lang_oadt.infrastructure]
oval_val [in oadt.lang_oadt.values]
oval_closed [in oadt.lang_oadt.infrastructure]
oval_lc [in oadt.lang_oadt.infrastructure]

P

pared_equiv_obliv_preservation [in oadt.lang_oadt.progress]
pared_obliv_preservation_inv [in oadt.lang_oadt.progress]
pared_lc [in oadt.lang_oadt.infrastructure]
pared_lc2 [in oadt.lang_oadt.infrastructure]
pared_lc1 [in oadt.lang_oadt.infrastructure]
pared_kinding_preservation [in oadt.lang_oadt.preservation]
pared_preservation [in oadt.lang_oadt.preservation]
pared_preservation_ [in oadt.lang_oadt.preservation]
pared_equiv_weakening [in oadt.lang_oadt.weakening]
pared_weakening [in oadt.lang_oadt.weakening]
pared_equiv_congr_psiproj [in oadt.lang_oadt.equivalence]
pared_equiv_congr_TApp [in oadt.lang_oadt.equivalence]
pared_equiv_congr_pi [in oadt.lang_oadt.equivalence]
pared_equiv_congr_inj [in oadt.lang_oadt.equivalence]
pared_equiv_congr_sum [in oadt.lang_oadt.equivalence]
pared_equiv_congr_prod [in oadt.lang_oadt.equivalence]
pared_equiv_open [in oadt.lang_oadt.equivalence]
pared_equiv_open2 [in oadt.lang_oadt.equivalence]
pared_equiv_open1 [in oadt.lang_oadt.equivalence]
pared_equiv_rename [in oadt.lang_oadt.equivalence]
pared_equiv_subst [in oadt.lang_oadt.equivalence]
pared_equiv_subst2 [in oadt.lang_oadt.equivalence]
pared_equiv_subst1 [in oadt.lang_oadt.equivalence]
pared_equiv_step [in oadt.lang_oadt.equivalence]
pared_equiv_pared [in oadt.lang_oadt.equivalence]
pared_step [in oadt.lang_oadt.equivalence]
pared_equiv_whnf_equiv [in oadt.lang_oadt.equivalence]
pared_whnf_equiv [in oadt.lang_oadt.equivalence]
pared_whnf [in oadt.lang_oadt.equivalence]
pared_equiv_rtsc [in oadt.lang_oadt.equivalence]
pared_equiv_iff_join [in oadt.lang_oadt.equivalence]
pared_confluent [in oadt.lang_oadt.equivalence]
pared_diamond [in oadt.lang_oadt.equivalence]
pared_inv_inj [in oadt.lang_oadt.equivalence]
pared_inv_fold [in oadt.lang_oadt.equivalence]
pared_inv_psipair [in oadt.lang_oadt.equivalence]
pared_inv_pair [in oadt.lang_oadt.equivalence]
pared_inv_abs [in oadt.lang_oadt.equivalence]
pared_rename [in oadt.lang_oadt.equivalence]
pared_open1 [in oadt.lang_oadt.equivalence]
pared_open [in oadt.lang_oadt.equivalence]
pared_subst [in oadt.lang_oadt.equivalence]
pared_subst_ [in oadt.lang_oadt.equivalence]
pared_subst1 [in oadt.lang_oadt.equivalence]
pared_subst1_ [in oadt.lang_oadt.equivalence]
pared_otval [in oadt.lang_oadt.equivalence]
pared_oval [in oadt.lang_oadt.equivalence]
preservation [in oadt.lang_oadt.preservation]
progress [in oadt.lang_oadt.progress]
progress_ [in oadt.lang_oadt.progress]

R

RApp_intro [in oadt.lang_oadt.equivalence]
RCase_intro [in oadt.lang_oadt.equivalence]
RCgrAbs_intro [in oadt.lang_oadt.equivalence]
RCgrCase_intro [in oadt.lang_oadt.equivalence]
RCgrPi_intro [in oadt.lang_oadt.equivalence]
regularity [in oadt.lang_oadt.preservation]
RLet_intro [in oadt.lang_oadt.equivalence]
ROCase_intro [in oadt.lang_oadt.equivalence]
rtc_preserve [in oadt.base]

S

SCtx_intro [in oadt.lang_oadt.infrastructure]
soundness [in oadt.lang_oadt.metatheories]
subst_tctx_fresh [in oadt.lang_oadt.infrastructure]
subst_fv [in oadt.lang_oadt.infrastructure]
subst_respect_lc [in oadt.lang_oadt.infrastructure]
subst_lc [in oadt.lang_oadt.infrastructure]
subst_intro [in oadt.lang_oadt.infrastructure]
subst_tctx_id [in oadt.lang_oadt.infrastructure]
subst_id [in oadt.lang_oadt.infrastructure]
subst_ite_distr [in oadt.lang_oadt.infrastructure]
subst_trans [in oadt.lang_oadt.infrastructure]
subst_open_comm [in oadt.lang_oadt.infrastructure]
subst_open_distr [in oadt.lang_oadt.infrastructure]
subst_fresh [in oadt.lang_oadt.infrastructure]
subst_conv [in oadt.lang_oadt.preservation]
subst_conv_ [in oadt.lang_oadt.preservation]
subst_preservation [in oadt.lang_oadt.preservation]
subst_preservation_ [in oadt.lang_oadt.preservation]
subst_tctx_typing [in oadt.lang_oadt.preservation]
subst_tctx_typing_kinding_ [in oadt.lang_oadt.preservation]

T

TAbs_intro [in oadt.lang_oadt.admissible]
TCase_intro [in oadt.lang_oadt.admissible]
tctx_stale_inv [in oadt.lang_oadt.infrastructure]
tctx_fv_insert [in oadt.lang_oadt.infrastructure]
tctx_fv_insert_subseteq [in oadt.lang_oadt.infrastructure]
tctx_fv_subseteq [in oadt.lang_oadt.infrastructure]
tctx_fv_consistent [in oadt.lang_oadt.infrastructure]
TLet_intro [in oadt.lang_oadt.admissible]
TOCase_intro [in oadt.lang_oadt.admissible]
top_inv [in oadt.semilattice]
top_ub [in oadt.semilattice]
typing_type_fv [in oadt.lang_oadt.infrastructure]
typing_fv [in oadt.lang_oadt.infrastructure]
typing_kinding_fv [in oadt.lang_oadt.infrastructure]
typing_type_lc [in oadt.lang_oadt.infrastructure]
typing_body [in oadt.lang_oadt.infrastructure]
typing_lc [in oadt.lang_oadt.infrastructure]
typing_inv_complete [in oadt.lang_oadt.inversion]
typing_rename_lc [in oadt.lang_oadt.admissible]
typing_rename [in oadt.lang_oadt.admissible]
typing_rename_alt [in oadt.lang_oadt.admissible]
typing_rename_ [in oadt.lang_oadt.admissible]
typing_kinding_rename_ [in oadt.lang_oadt.admissible]

V

val_oval [in oadt.lang_oadt.progress]
val_is_nf [in oadt.lang_oadt.values]
val_step [in oadt.lang_oadt.values]
val_otval [in oadt.lang_oadt.values]

W

weakening [in oadt.lang_oadt.weakening]
weakening_insert [in oadt.lang_oadt.weakening]
weakening_empty [in oadt.lang_oadt.weakening]
weakening_ [in oadt.lang_oadt.weakening]

Constructor Index

C

CtxApp1 [in oadt.lang_oadt.semantics]
CtxApp2 [in oadt.lang_oadt.semantics]
CtxCase [in oadt.lang_oadt.semantics]
CtxFold [in oadt.lang_oadt.semantics]
CtxInj [in oadt.lang_oadt.semantics]
CtxIte [in oadt.lang_oadt.semantics]
CtxLet [in oadt.lang_oadt.semantics]
CtxMux1 [in oadt.lang_oadt.semantics]
CtxMux2 [in oadt.lang_oadt.semantics]
CtxMux3 [in oadt.lang_oadt.semantics]
CtxOCase [in oadt.lang_oadt.semantics]
CtxOInj1 [in oadt.lang_oadt.semantics]
CtxOInj2 [in oadt.lang_oadt.semantics]
CtxOSum1 [in oadt.lang_oadt.semantics]
CtxOSum2 [in oadt.lang_oadt.semantics]
CtxPair1 [in oadt.lang_oadt.semantics]
CtxPair2 [in oadt.lang_oadt.semantics]
CtxProd1 [in oadt.lang_oadt.semantics]
CtxProd2 [in oadt.lang_oadt.semantics]
CtxProj [in oadt.lang_oadt.semantics]
CtxPsiPair1 [in oadt.lang_oadt.semantics]
CtxPsiPair2 [in oadt.lang_oadt.semantics]
CtxPsiProj [in oadt.lang_oadt.semantics]
CtxSec [in oadt.lang_oadt.semantics]
CtxTApp [in oadt.lang_oadt.semantics]
CtxUnfold [in oadt.lang_oadt.semantics]

D

DADT [in oadt.lang_oadt.syntax]
DFun [in oadt.lang_oadt.syntax]
DOADT [in oadt.lang_oadt.syntax]
DTADT [in oadt.lang_oadt.typing]
DTFun [in oadt.lang_oadt.typing]
DTOADT [in oadt.lang_oadt.typing]

E

EAbs [in oadt.lang_oadt.syntax]
EApp [in oadt.lang_oadt.syntax]
EBool [in oadt.lang_oadt.syntax]
EBoxedInj [in oadt.lang_oadt.syntax]
EBoxedLit [in oadt.lang_oadt.syntax]
EBVar [in oadt.lang_oadt.syntax]
ECase [in oadt.lang_oadt.syntax]
EFold [in oadt.lang_oadt.syntax]
EFVar [in oadt.lang_oadt.syntax]
EGVar [in oadt.lang_oadt.syntax]
EInj [in oadt.lang_oadt.syntax]
EIte [in oadt.lang_oadt.syntax]
ELet [in oadt.lang_oadt.syntax]
ELit [in oadt.lang_oadt.syntax]
EMux [in oadt.lang_oadt.syntax]
EPair [in oadt.lang_oadt.syntax]
EPi [in oadt.lang_oadt.syntax]
EProd [in oadt.lang_oadt.syntax]
EProj [in oadt.lang_oadt.syntax]
EPsi [in oadt.lang_oadt.syntax]
EPsiPair [in oadt.lang_oadt.syntax]
EPsiProj [in oadt.lang_oadt.syntax]
ESec [in oadt.lang_oadt.syntax]
ESum [in oadt.lang_oadt.syntax]
ETApp [in oadt.lang_oadt.syntax]
EUnfold [in oadt.lang_oadt.syntax]
EUnitT [in oadt.lang_oadt.syntax]
EUnitV [in oadt.lang_oadt.syntax]

K

KAny [in oadt.lang_oadt.kind]
KApp [in oadt.lang_oadt.typing]
KBool [in oadt.lang_oadt.typing]
KCase [in oadt.lang_oadt.typing]
kernel.IBoxedInj [in oadt.lang_oadt.indistinguishable]
kernel.IBoxedLit [in oadt.lang_oadt.indistinguishable]
KGVar [in oadt.lang_oadt.typing]
KIte [in oadt.lang_oadt.typing]
KLet [in oadt.lang_oadt.typing]
KMixed [in oadt.lang_oadt.kind]
KObliv [in oadt.lang_oadt.kind]
KOBool [in oadt.lang_oadt.typing]
KOProd [in oadt.lang_oadt.typing]
KOSum [in oadt.lang_oadt.typing]
KPi [in oadt.lang_oadt.typing]
KProd [in oadt.lang_oadt.typing]
KPsi [in oadt.lang_oadt.typing]
KPublic [in oadt.lang_oadt.kind]
KSub [in oadt.lang_oadt.typing]
KSum [in oadt.lang_oadt.typing]
KUnit [in oadt.lang_oadt.typing]

L

LCAbs [in oadt.lang_oadt.syntax]
LCApp [in oadt.lang_oadt.syntax]
LCBool [in oadt.lang_oadt.syntax]
LCBoxedInj [in oadt.lang_oadt.syntax]
LCBoxedLit [in oadt.lang_oadt.syntax]
LCCase [in oadt.lang_oadt.syntax]
LCFold [in oadt.lang_oadt.syntax]
LCFVar [in oadt.lang_oadt.syntax]
LCGVar [in oadt.lang_oadt.syntax]
LCInj [in oadt.lang_oadt.syntax]
LCIte [in oadt.lang_oadt.syntax]
LCLet [in oadt.lang_oadt.syntax]
LCLit [in oadt.lang_oadt.syntax]
LCMux [in oadt.lang_oadt.syntax]
LCPair [in oadt.lang_oadt.syntax]
LCPi [in oadt.lang_oadt.syntax]
LCProd [in oadt.lang_oadt.syntax]
LCProj [in oadt.lang_oadt.syntax]
LCPsi [in oadt.lang_oadt.syntax]
LCPsiPair [in oadt.lang_oadt.syntax]
LCPsiProj [in oadt.lang_oadt.syntax]
LCSec [in oadt.lang_oadt.syntax]
LCSum [in oadt.lang_oadt.syntax]
LCTApp [in oadt.lang_oadt.syntax]
LCUnfold [in oadt.lang_oadt.syntax]
LCUnitT [in oadt.lang_oadt.syntax]
LCUnitV [in oadt.lang_oadt.syntax]

O

OTOBool [in oadt.lang_oadt.semantics]
OTOSum [in oadt.lang_oadt.semantics]
OTProd [in oadt.lang_oadt.semantics]
OTUnit [in oadt.lang_oadt.semantics]
OVBoxedInj [in oadt.lang_oadt.syntax]
OVBoxedLit [in oadt.lang_oadt.syntax]
OVOBool [in oadt.lang_oadt.syntax]
OVOSum [in oadt.lang_oadt.syntax]
OVPair [in oadt.lang_oadt.syntax]
OVProd [in oadt.lang_oadt.syntax]
OVUnitT [in oadt.lang_oadt.syntax]
OVUnitV [in oadt.lang_oadt.syntax]

Q

QRRedL [in oadt.lang_oadt.typing]
QRRedR [in oadt.lang_oadt.typing]
QRRefl [in oadt.lang_oadt.typing]

R

RApp [in oadt.lang_oadt.typing]
RCase [in oadt.lang_oadt.typing]
RCgrAbs [in oadt.lang_oadt.typing]
RCgrApp [in oadt.lang_oadt.typing]
RCgrCase [in oadt.lang_oadt.typing]
RCgrFold [in oadt.lang_oadt.typing]
RCgrInj [in oadt.lang_oadt.typing]
RCgrIte [in oadt.lang_oadt.typing]
RCgrLet [in oadt.lang_oadt.typing]
RCgrMux [in oadt.lang_oadt.typing]
RCgrPair [in oadt.lang_oadt.typing]
RCgrPi [in oadt.lang_oadt.typing]
RCgrProd [in oadt.lang_oadt.typing]
RCgrProj [in oadt.lang_oadt.typing]
RCgrPsiPair [in oadt.lang_oadt.typing]
RCgrPsiProj [in oadt.lang_oadt.typing]
RCgrSec [in oadt.lang_oadt.typing]
RCgrSum [in oadt.lang_oadt.typing]
RCgrTApp [in oadt.lang_oadt.typing]
RCgrUnfold [in oadt.lang_oadt.typing]
RFun [in oadt.lang_oadt.typing]
RIte [in oadt.lang_oadt.typing]
RLet [in oadt.lang_oadt.typing]
RMux [in oadt.lang_oadt.typing]
ROCase [in oadt.lang_oadt.typing]
ROInj [in oadt.lang_oadt.typing]
RProj [in oadt.lang_oadt.typing]
RPsiProj [in oadt.lang_oadt.typing]
RRefl [in oadt.lang_oadt.typing]
RSec [in oadt.lang_oadt.typing]
RTApp [in oadt.lang_oadt.typing]
RUnfold [in oadt.lang_oadt.typing]

S

SApp [in oadt.lang_oadt.semantics]
SCase [in oadt.lang_oadt.semantics]
SCtx [in oadt.lang_oadt.semantics]
SFun [in oadt.lang_oadt.semantics]
SIte [in oadt.lang_oadt.semantics]
SLet [in oadt.lang_oadt.semantics]
SMux [in oadt.lang_oadt.semantics]
SOCase [in oadt.lang_oadt.semantics]
SOInj [in oadt.lang_oadt.semantics]
SProj [in oadt.lang_oadt.semantics]
SPsiProj [in oadt.lang_oadt.semantics]
SSec [in oadt.lang_oadt.semantics]
stale [in oadt.ln]
STApp [in oadt.lang_oadt.semantics]
SUnfold [in oadt.lang_oadt.semantics]

T

TAbs [in oadt.lang_oadt.typing]
TApp [in oadt.lang_oadt.typing]
TBoxedInj [in oadt.lang_oadt.typing]
TBoxedLit [in oadt.lang_oadt.typing]
TCase [in oadt.lang_oadt.typing]
TConv [in oadt.lang_oadt.typing]
TFold [in oadt.lang_oadt.typing]
TFVar [in oadt.lang_oadt.typing]
TGVar [in oadt.lang_oadt.typing]
TInj [in oadt.lang_oadt.typing]
TIte [in oadt.lang_oadt.typing]
TLet [in oadt.lang_oadt.typing]
TLit [in oadt.lang_oadt.typing]
TMux [in oadt.lang_oadt.typing]
TOCase [in oadt.lang_oadt.typing]
TOInj [in oadt.lang_oadt.typing]
TOPair [in oadt.lang_oadt.typing]
TOProj [in oadt.lang_oadt.typing]
TPair [in oadt.lang_oadt.typing]
TProj [in oadt.lang_oadt.typing]
TPsiPair [in oadt.lang_oadt.typing]
TPsiProj1 [in oadt.lang_oadt.typing]
TPsiProj2 [in oadt.lang_oadt.typing]
TSec [in oadt.lang_oadt.typing]
TUnfold [in oadt.lang_oadt.typing]
TUnit [in oadt.lang_oadt.typing]

V

VAbs [in oadt.lang_oadt.syntax]
VFold [in oadt.lang_oadt.syntax]
VInj [in oadt.lang_oadt.syntax]
VLit [in oadt.lang_oadt.syntax]
VOVal [in oadt.lang_oadt.syntax]
VPair [in oadt.lang_oadt.syntax]
VPsiPair [in oadt.lang_oadt.syntax]

W

WADT [in oadt.lang_oadt.equivalence]
WBool [in oadt.lang_oadt.equivalence]
WPi [in oadt.lang_oadt.equivalence]
WProd [in oadt.lang_oadt.equivalence]
WPsi [in oadt.lang_oadt.equivalence]
WQADT [in oadt.lang_oadt.equivalence]
WQBool [in oadt.lang_oadt.equivalence]
WQPi [in oadt.lang_oadt.equivalence]
WQProd [in oadt.lang_oadt.equivalence]
WQPsi [in oadt.lang_oadt.equivalence]
WQSum [in oadt.lang_oadt.equivalence]
WQUnitT [in oadt.lang_oadt.equivalence]
WSum [in oadt.lang_oadt.equivalence]
WUnitT [in oadt.lang_oadt.equivalence]

Inductive Index

E

ectx [in oadt.lang_oadt.semantics]
expr [in oadt.lang_oadt.syntax]

G

gdef [in oadt.lang_oadt.syntax]
gdef_typing [in oadt.lang_oadt.typing]

K

kernel.indistinguishable [in oadt.lang_oadt.indistinguishable]
kind [in oadt.lang_oadt.kind]
kinding [in oadt.lang_oadt.typing]

L

lc [in oadt.lang_oadt.syntax]

O

otval [in oadt.lang_oadt.syntax]
oval [in oadt.lang_oadt.syntax]
ovalty [in oadt.lang_oadt.semantics]

P

pared [in oadt.lang_oadt.typing]
pared_equiv [in oadt.lang_oadt.typing]

S

Stale [in oadt.ln]
step [in oadt.lang_oadt.semantics]

T

typing [in oadt.lang_oadt.typing]

V

val [in oadt.lang_oadt.syntax]

W

whnf [in oadt.lang_oadt.equivalence]
whnf_equiv [in oadt.lang_oadt.equivalence]

Projection Index

A

atom_is_fresh [in oadt.ln]
atom_fresh [in oadt.ln]
atom_finmap_elem_of_dec [in oadt.ln]
atom_elem_of_dom [in oadt.ln]
atom_finmap [in oadt.ln]
atom_finset [in oadt.ln]
atom_infinite [in oadt.ln]
atom_eq_decision [in oadt.ln]
atom_finset_elements [in oadt.ln]
atom_finset_difference [in oadt.ln]
atom_finset_intersection [in oadt.ln]
atom_finset_union [in oadt.ln]
atom_finset_singleton [in oadt.ln]
atom_finset_empty [in oadt.ln]
atom_finset_elem_of [in oadt.ln]
atom_finmap_map_fold [in oadt.ln]
atom_finmap_merge [in oadt.ln]
atom_finmap_omap [in oadt.ln]
atom_finmap_partial_alter [in oadt.ln]
atom_finmap_empty [in oadt.ln]
atom_finmap_lookup [in oadt.ln]
atom_finmap_fmap [in oadt.ln]
atom_finmap_dom [in oadt.ln]

J

join_consistent [in oadt.semilattice]
join_left_absorb [in oadt.semilattice]
join_left_id [in oadt.semilattice]
join_idemp [in oadt.semilattice]
join_assoc [in oadt.semilattice]
join_comm [in oadt.semilattice]

P

pack_finmap [in oadt.base]
pack_finmap_map_fold [in oadt.base]
pack_finmap_merge [in oadt.base]
pack_finmap_omap [in oadt.base]
pack_finmap_partial_alter [in oadt.base]
pack_finmap_empty [in oadt.base]
pack_finmap_lookup [in oadt.base]
pack_finmap_fmap [in oadt.base]
pack_finmap_decision [in oadt.base]

S

stale [in oadt.ln]

Section Index

A

admissible [in oadt.lang_oadt.admissible]

C

close [in oadt.lang_oadt.infrastructure]

D

definitions [in oadt.lang_oadt.syntax]

E

equivalence [in oadt.lang_oadt.equivalence]
equivalence [in oadt.lang_oadt.equivalence]

F

fix_gctx [in oadt.lang_oadt.progress]
fix_gctx [in oadt.lang_oadt.progress]
fix_gctx [in oadt.lang_oadt.values]
fix_gctx [in oadt.lang_oadt.preservation]
fix_gctx [in oadt.lang_oadt.obliviousness]

S

set [in oadt.base]
step [in oadt.lang_oadt.semantics]

T

theorems [in oadt.semilattice]
typing [in oadt.lang_oadt.typing]
typing.fix_gctx [in oadt.lang_oadt.typing]

Instance Index

A

aamap_is_finmap [in oadt.lang_oadt.base]
aset_stale [in oadt.lang_oadt.infrastructure]
atom_stale [in oadt.lang_oadt.infrastructure]
atom_instance.is_atom [in oadt.ln]
atom_dom_spec [in oadt.ln]

B

bool_semilattice [in oadt.semilattice]
bool_le [in oadt.semilattice]
bool_bot [in oadt.semilattice]
bool_top [in oadt.semilattice]
bool_join [in oadt.semilattice]

E

elem_of_subseteq_flip_proper [in oadt.base]
elem_of_subseteq_proper [in oadt.base]
expr_stale [in oadt.lang_oadt.infrastructure]
expr_eq [in oadt.lang_oadt.syntax]

I

indistinguishable_is_equiv [in oadt.lang_oadt.obliviousness]

J

join_right_absorb [in oadt.semilattice]
join_right_id [in oadt.semilattice]

K

kind_semilattice [in oadt.lang_oadt.kind]
kind_bot [in oadt.lang_oadt.kind]
kind_top [in oadt.lang_oadt.kind]
kind_le [in oadt.lang_oadt.kind]
kind_join [in oadt.lang_oadt.kind]
kind_eq [in oadt.lang_oadt.kind]

P

pared_equiv_is_trans [in oadt.lang_oadt.equivalence]
pared_equiv_is_symm [in oadt.lang_oadt.equivalence]
pared_equiv_is_refl [in oadt.lang_oadt.equivalence]

S

semilattice_is_po [in oadt.semilattice]

T

tctx_stale [in oadt.lang_oadt.infrastructure]

U

union_subseteq_flip_proper [in oadt.base]
union_subseteq_proper [in oadt.base]

W

whnf_equiv_is_symm [in oadt.lang_oadt.equivalence]

Abbreviation Index

L

LObliv [in oadt.lang_oadt.syntax]
LPub [in oadt.lang_oadt.syntax]

O

olabel [in oadt.lang_oadt.syntax]

P

program [in oadt.lang_oadt.syntax]

T

tctx [in oadt.lang_oadt.typing]

Definition Index

A

aamap [in oadt.lang_oadt.base]
atom_instance.aset [in oadt.ln]
atom_instance.amap [in oadt.ln]
atom_instance.atom [in oadt.ln]

B

body [in oadt.lang_oadt.infrastructure]

C

close [in oadt.lang_oadt.infrastructure]
closed [in oadt.lang_oadt.infrastructure]
close_ [in oadt.lang_oadt.infrastructure]

E

expr_sind [in oadt.lang_oadt.syntax]
expr_rec [in oadt.lang_oadt.syntax]
expr_ind [in oadt.lang_oadt.syntax]
expr_rect [in oadt.lang_oadt.syntax]

F

fv [in oadt.lang_oadt.infrastructure]

G

gctx [in oadt.lang_oadt.syntax]
gctx_wf [in oadt.lang_oadt.typing]
gctx_typing [in oadt.lang_oadt.typing]
gdef_typing_sind [in oadt.lang_oadt.typing]
gdef_typing_ind [in oadt.lang_oadt.typing]

K

kernel.indistinguishable_sind [in oadt.lang_oadt.indistinguishable]
kernel.indistinguishable_ind [in oadt.lang_oadt.indistinguishable]
kinding_typing_ind [in oadt.lang_oadt.typing]
kinding_sind [in oadt.lang_oadt.typing]
kinding_ind [in oadt.lang_oadt.typing]

L

lc_sind [in oadt.lang_oadt.syntax]
lc_ind [in oadt.lang_oadt.syntax]

O

open [in oadt.lang_oadt.syntax]
open_ [in oadt.lang_oadt.syntax]
otval_sind [in oadt.lang_oadt.syntax]
otval_ind [in oadt.lang_oadt.syntax]
ovalty_sind [in oadt.lang_oadt.semantics]
ovalty_ind [in oadt.lang_oadt.semantics]
oval_sind [in oadt.lang_oadt.syntax]
oval_ind [in oadt.lang_oadt.syntax]

P

pared_equiv_join [in oadt.lang_oadt.typing]
pared_equiv_sind [in oadt.lang_oadt.typing]
pared_equiv_ind [in oadt.lang_oadt.typing]
pared_sind [in oadt.lang_oadt.typing]
pared_ind [in oadt.lang_oadt.typing]
program_typing [in oadt.lang_oadt.typing]

S

step_sind [in oadt.lang_oadt.semantics]
step_ind [in oadt.lang_oadt.semantics]
stuck [in oadt.lang_oadt.metatheories]
subst [in oadt.lang_oadt.syntax]

T

tctx_fv [in oadt.lang_oadt.infrastructure]
trace_indistinguishable [in oadt.lang_oadt.metatheories]
typing_kinding_ind [in oadt.lang_oadt.typing]
typing_sind [in oadt.lang_oadt.typing]
typing_ind [in oadt.lang_oadt.typing]

V

val_sind [in oadt.lang_oadt.syntax]
val_ind [in oadt.lang_oadt.syntax]

W

whnf_equiv_sind [in oadt.lang_oadt.equivalence]
whnf_equiv_ind [in oadt.lang_oadt.equivalence]
whnf_sind [in oadt.lang_oadt.equivalence]
whnf_ind [in oadt.lang_oadt.equivalence]

Record Index

A

Atom [in oadt.ln]

F

FinMapPack [in oadt.base]

S

SemiLattice [in oadt.semilattice]
Stale [in oadt.ln]

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

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

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

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

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

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

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

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

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

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

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

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

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

(4 entries)