| 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 | (974 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 | (109 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 | (2 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 | (27 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 | (17 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 | (455 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 | (83 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 | (2 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 | (15 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 | (10 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 | (11 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 | (240 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 | (3 entries) |
Global Index
A
able [lemma, in PredomProd]Adequacy [library]
Adequacy1_b [lemma, in Adequacy]
_ e⊢ _ ▶̂ _ ⦂ _ [notation, in Adequacy]
_ v⊢ _ ▷̂ _ ⦂ _ [notation, in Adequacy]
_ e⊢ _ ▶̂̅ _ ⦂ _ [notation, in Adequacy]
_ v⊢ _ ▷̂̅ _ ⦂ _ [notation, in Adequacy]
_ ⊵ _ ⦂ _ [notation, in Adequacy]
_ ▷̅ _ ⦂ _ [notation, in Adequacy]
_ ▷ _ ⦂ _ [notation, in Adequacy]
⇑ _ [notation, in Adequacy]
↓ _ [notation, in Adequacy]
↓r _ [notation, in Adequacy]
Adequacy1_b.b [variable, in Adequacy]
Adequacy1_b [section, in Adequacy]
Adequacy1_n [lemma, in Adequacy]
_ e⊢ _ ▶̂ _ ⦂ _ [notation, in Adequacy]
_ v⊢ _ ▷̂ _ ⦂ _ [notation, in Adequacy]
_ e⊢ _ ▶̂̅ _ ⦂ _ [notation, in Adequacy]
_ v⊢ _ ▷̂̅ _ ⦂ _ [notation, in Adequacy]
_ ⊵ _ ⦂ _ [notation, in Adequacy]
_ ▷̅ _ ⦂ _ [notation, in Adequacy]
_ ▷ _ ⦂ _ [notation, in Adequacy]
⇑ _ [notation, in Adequacy]
↓ _ [notation, in Adequacy]
↓r _ [notation, in Adequacy]
Adequacy1_n.n [variable, in Adequacy]
Adequacy1_n [section, in Adequacy]
Adequacy2 [lemma, in Adequacy]
Adequacy2 [section, in Adequacy]
_ e⊢ _ ◀̂ _ ⦂ _ [notation, in Adequacy]
_ v⊢ _ ◁̂ _ ⦂ _ [notation, in Adequacy]
_ ⊴ _ | _ ⦂ _ [notation, in Adequacy]
_ ◀ _ | _ ⦂ _ [notation, in Adequacy]
_ ◁ _ | _ ⦂ _ [notation, in Adequacy]
_ ⇡ [notation, in Adequacy]
_ ⟿ _ [notation, in Adequacy]
↓r _ [notation, in Adequacy]
↓ _ [notation, in Adequacy]
⇑ _ [notation, in Adequacy]
admit [definition, in Utils]
AndOP [constructor, in Lang]
antiExec [projection, in DenoApprox]
AntiexecE [definition, in DenoApprox]
Antiexec_step [definition, in OperApprox]
AntiE_SemOper [lemma, in Adequacy]
anti_step [projection, in OperApprox]
APP [constructor, in Lang]
App [constructor, in OperSem]
appCase [lemma, in MoT]
applyComposeRen [lemma, in Lang]
applyComposeRenSub [lemma, in Lang]
applyIdMap [lemma, in Lang]
AppOp [definition, in ExSem]
ApproxEquivE [lemma, in DenoApprox]
ApproxEquivV [lemma, in DenoApprox]
AppRule [constructor, in Types]
AppRule_simpl [lemma, in InSem]
AppTy [definition, in InSem]
a_fibn [definition, in fib_Adequacy]
B
b [variable, in Adequacy]bbot_down_closed [lemma, in OperApprox]
ble [lemma, in Adequacy]
BOOL [constructor, in Lang]
BoolCast [constructor, in OperSem]
BoolOp [inductive, in Lang]
BoolOpLemma [lemma, in ExSem]
boolopsimplE [lemma, in MoT]
BoolRelBFun [lemma, in MoT]
BoolRelBinFun [lemma, in MoT]
BoolRule [constructor, in Types]
BoolsimpE [lemma, in MoT]
BoolsimpE' [lemma, in MoT]
BoolToNatRule [constructor, in Types]
BoolTy [constructor, in Types]
bool_sum_coherent [lemma, in CoherenceExample]
bool_sum_app_tj' [lemma, in CoherenceExample]
bool_sum_app_tj [lemma, in CoherenceExample]
bool_sum_tj' [lemma, in CoherenceExample]
bool_sum_tj [lemma, in CoherenceExample]
bool_sum_app [definition, in CoherenceExample]
bool_sum [definition, in CoherenceExample]
BOp [constructor, in Lang]
BOpRule [constructor, in Types]
BOpRule_Val2 [lemma, in InSem]
BOpRule_Val [lemma, in InSem]
BOpRule_simpl [lemma, in InSem]
Bracketing [lemma, in MoT]
BTONInj [lemma, in MoT]
B_to_N [definition, in DomainStuff]
C
Case1 [lemma, in OperApprox]Case1 [lemma, in DenoApprox]
Case1_IC [lemma, in DenoApprox]
Case10 [lemma, in OperApprox]
Case10 [lemma, in DenoApprox]
Case10_IC [lemma, in DenoApprox]
Case11 [lemma, in OperApprox]
Case11 [lemma, in DenoApprox]
Case11_IC [lemma, in DenoApprox]
Case12 [lemma, in OperApprox]
Case12 [lemma, in DenoApprox]
Case12_IC [lemma, in DenoApprox]
Case2 [lemma, in OperApprox]
Case2 [lemma, in DenoApprox]
Case2_IC [lemma, in DenoApprox]
Case3 [lemma, in OperApprox]
Case3 [lemma, in DenoApprox]
Case3_IC [lemma, in DenoApprox]
Case4 [lemma, in OperApprox]
Case4 [lemma, in DenoApprox]
Case4_IC [lemma, in DenoApprox]
Case5 [lemma, in OperApprox]
Case5 [lemma, in DenoApprox]
Case5_IC [lemma, in DenoApprox]
Case6 [lemma, in OperApprox]
Case6 [lemma, in DenoApprox]
Case6_IC [lemma, in DenoApprox]
Case7 [lemma, in OperApprox]
Case7 [lemma, in DenoApprox]
Case7_IC [lemma, in DenoApprox]
Case8 [lemma, in OperApprox]
Case8 [lemma, in DenoApprox]
Case8_IC [lemma, in DenoApprox]
Case9 [lemma, in OperApprox]
Case9 [lemma, in DenoApprox]
Case9_IC [lemma, in DenoApprox]
CCURRY [definition, in DomainStuff]
chain_complete [definition, in StrictExt]
closed_star_transition [lemma, in OperSem]
closed_transition [lemma, in OperSem]
Coherence [lemma, in MoT]
CoherenceExample [library]
composeCons [lemma, in Lang]
composeRen [definition, in Lang]
composeRenSub [definition, in Lang]
composeSub [definition, in Lang]
composeSubIdLeft [lemma, in Lang]
composeSubIdRight [lemma, in Lang]
comp_simpl [lemma, in DomainStuff]
consMap [definition, in Lang]
consMapEta [lemma, in Lang]
coq_fib_prop2 [lemma, in fib_Adequacy]
coq_fib_prop [lemma, in fib_Adequacy]
coq_fib [definition, in fib_Adequacy]
Curry1_cont [lemma, in DomainStuff]
CURRY1_mon [definition, in DomainStuff]
Curry1_mon [lemma, in DomainStuff]
D
DBOp [constructor, in OperSem]Def_Bracketing [definition, in MoT]
deltaArrCComp [lemma, in MoT]
deltaArrow [lemma, in MoT]
deltaBoolCComp [lemma, in MoT]
deltaBoolCompat [lemma, in MoT]
deltaBoolFunc [lemma, in MoT]
deltaBoolOpP [lemma, in MoT]
deltaNatCComp [lemma, in MoT]
deltaNatCompat [lemma, in MoT]
deltaNatFunc [lemma, in MoT]
deltaNatOp [lemma, in MoT]
deltaNatOpP [lemma, in MoT]
deltaNatOpt [lemma, in MoT]
deltaOrdOpP [lemma, in MoT]
deltaPairCComp [lemma, in MoT]
deltaPairCompat [lemma, in MoT]
delta_rho_cc [lemma, in MoT]
delta_rho_compat [lemma, in MoT]
DenoApprox [section, in DenoApprox]
DenoApprox [library]
DenoApprox.RE [variable, in DenoApprox]
_ e⊢ _ ▶̂ _ ⦂ _ [notation, in DenoApprox]
_ v⊢ _ ▷̂ _ ⦂ _ [notation, in DenoApprox]
_ e⊢ _ ▶̂̅ _ ⦂ _ [notation, in DenoApprox]
_ v⊢ _ ▷̂̅ _ ⦂ _ [notation, in DenoApprox]
_ ⊵ _ ⦂ _ [notation, in DenoApprox]
_ ▶ _ ⦂ _ [notation, in DenoApprox]
_ ▷ _ ⦂ _ [notation, in DenoApprox]
↓r _ [notation, in DenoApprox]
↓ _ [notation, in DenoApprox]
⇑ _ [notation, in DenoApprox]
DenotApproxCtx [definition, in DenoApprox]
DenotApproxE [definition, in DenoApprox]
DenotApproxE_PBot [lemma, in DenoApprox]
DenotApproxV [definition, in DenoApprox]
DInfToNat [definition, in MoT]
DInfToNat_bot' [lemma, in MoT]
DInfToNat_bot [lemma, in MoT]
discrete_eq [lemma, in DomainStuff]
DLleEpsTrans [lemma, in DomainStuff]
DLleEq [lemma, in DomainStuff]
DLleEqR [lemma, in DomainStuff]
DNOp [constructor, in OperSem]
Domains [library]
DomainStuff [library]
DOOp [constructor, in OperSem]
DownR [definition, in OperApprox]
DownR [definition, in DenoApprox]
E
EFST [constructor, in Lang]EmbProjPair [lemma, in EmbProjPair]
EmbProjPair [lemma, in MoT]
EmbProjPair [library]
Empty [constructor, in Lang]
Env [definition, in Lang]
EPPair_SemSubType [lemma, in MoT]
EpsStable [lemma, in DomainStuff]
eqLubChains [lemma, in StrictExt]
EqOP [constructor, in Lang]
ESND [constructor, in Lang]
Expand2ApproxCtx [lemma, in OperApprox]
Expand2ApproxCtx [lemma, in DenoApprox]
Expr [inductive, in Lang]
ExSem [library]
Extrinsic_Adequacy_b [lemma, in Adequacy]
Extrinsic_Adequacy [lemma, in Adequacy]
Extrinsic_Adequacy1_b [lemma, in Adequacy]
Extrinsic_Adequacy1 [lemma, in Adequacy]
Ex_eqV_In [lemma, in MoT]
Ex_eq_In_b [lemma, in MoT]
Ex_eq_In [lemma, in MoT]
Ex_Adequacy_2_from_In [lemma, in Adequacy]
E_False [definition, in CoherenceExample]
E_True [definition, in CoherenceExample]
E_induction [definition, in Lang]
F
F [definition, in DenoApprox]F [definition, in ExSem]
FC [definition, in DenoApprox]
FChain [definition, in DenoApprox]
FChainCore [definition, in DenoApprox]
FChainCore_mon [lemma, in DenoApprox]
FChainCore_S [lemma, in DenoApprox]
FChainCore_S_unfold [lemma, in DenoApprox]
FChainCore_unfold [lemma, in DenoApprox]
FChain_mon [lemma, in DenoApprox]
FChain_S [lemma, in DenoApprox]
FC_lub [lemma, in DenoApprox]
FC_unfold [lemma, in DenoApprox]
FC_zero [lemma, in DenoApprox]
FC_simpl [lemma, in DenoApprox]
Fib [inductive, in fib_Adequacy]
fib [lemma, in fib_Adequacy]
FibCorr [lemma, in fib_Adequacy]
fibn_eq [lemma, in fib_Adequacy]
fibn_prop [lemma, in fib_Adequacy]
fibn_sem [definition, in fib_Adequacy]
fibn_syn [definition, in fib_Adequacy]
FibS [constructor, in fib_Adequacy]
Fib_Adequacy.Fib_Sem [section, in fib_Adequacy]
fib_body [lemma, in fib_Adequacy]
Fib_body [definition, in fib_Adequacy]
Fib_Adequacy.Fib_Lang [section, in fib_Adequacy]
Fib_Adequacy.n [variable, in fib_Adequacy]
Fib_Adequacy [section, in fib_Adequacy]
fib_Adequacy [library]
Fib0 [constructor, in fib_Adequacy]
Fib1 [constructor, in fib_Adequacy]
FixF [definition, in InSem]
FIXP_Step [lemma, in OperApprox]
FIXP_Prop [lemma, in DenoApprox]
fmon_eq_bot [lemma, in DenoApprox]
fromRel [lemma, in MoT]
fromToBool [lemma, in EmbProjPair]
fromToNat [lemma, in EmbProjPair]
FS [inductive, in Lang]
FstOp [constructor, in OperSem]
FSTOp [definition, in ExSem]
FSTRule [constructor, in Types]
FstTy [definition, in InSem]
FS_In_compat [lemma, in OperApprox]
FUN [constructor, in Lang]
FuncToMono [lemma, in StrictExt]
FundamentalPropOfLogicalRelations [lemma, in OperApprox]
FundamentalPropOfLogicalRelations [lemma, in DenoApprox]
FunRule [constructor, in Types]
FunRule_simpl [lemma, in InSem]
FunTy [constructor, in Types]
G
Gamma_E_In [lemma, in MoT]GenBinOp [definition, in ExSem]
GenBinOpIn [definition, in MoT]
GenBinOpSimpl [lemma, in MoT]
genbinopsimpl [lemma, in MoT]
GenBinOpTy [definition, in InSem]
GenBinOp_DInf [definition, in ExSem]
GenBoolOp [definition, in ExSem]
GenBoolOp_DInf [definition, in ExSem]
GenDenotApproxE [definition, in DenoApprox]
GenDenotApproxV [definition, in DenoApprox]
GenNatOp [definition, in ExSem]
GenNatOp_DInf [definition, in ExSem]
GenOperApproxE [definition, in OperApprox]
GenOperApproxV [definition, in OperApprox]
GenOrdOp [definition, in ExSem]
GenOrdOp_DInf [definition, in ExSem]
GtoE [definition, in EmbProjPair]
H
hdConsMap [lemma, in Lang]hdMap [definition, in Lang]
I
IBOp [constructor, in OperSem]idMap [definition, in Lang]
idMapDef [lemma, in Lang]
idRen [definition, in Lang]
idSub [definition, in Lang]
IfB [definition, in DomainStuff]
IFB [constructor, in Lang]
IfB [constructor, in OperSem]
IfBCore [definition, in DomainStuff]
IfBCoreM [definition, in DomainStuff]
IfBCoreM2 [definition, in DomainStuff]
IfBCore_cont2 [lemma, in DomainStuff]
IfBCore_mon2 [lemma, in DomainStuff]
IfBCore_mon [lemma, in DomainStuff]
IfBF [constructor, in OperSem]
IfBOp [definition, in ExSem]
IfBRule [constructor, in Types]
IfBT [constructor, in OperSem]
IfBTy [definition, in InSem]
IfOneOp [definition, in ExSem]
IfZ [definition, in DomainStuff]
IfZCore [definition, in DomainStuff]
IfZCoreM [definition, in DomainStuff]
IfZCoreM2 [definition, in DomainStuff]
IfZCore_cont2 [lemma, in DomainStuff]
IfZCore_mon2 [lemma, in DomainStuff]
IfZCore_mon [lemma, in DomainStuff]
IfZOp [definition, in ExSem]
IfZRule_simpl [lemma, in InSem]
IFZ_Val [lemma, in InSem]
IF3 [definition, in DomainStuff]
if3 [definition, in DomainStuff]
injnToDInf [definition, in MoT]
INL_convert [lemma, in ExSem]
INOp [constructor, in OperSem]
InSem [library]
InSemE [definition, in InSem]
InSemFun_unfold [lemma, in InSem]
InSemV [definition, in InSem]
Intrinsic_Adequacy_2 [axiom, in Adequacy]
Intrinsic_Adequacy_b [lemma, in Adequacy]
Intrinsic_Adequacy [lemma, in Adequacy]
In_eqV_Ex [lemma, in MoT]
In_eq_Ex [lemma, in MoT]
In_Adequacy_1_from_Ex [lemma, in Adequacy]
IOOp [constructor, in OperSem]
K
kcpoCatAxiom [lemma, in Domains]KLEISLIL_Eps [lemma, in DomainStuff]
KLEISLIL_PBot [lemma, in DomainStuff]
KLEISLIL_unit2 [lemma, in DomainStuff]
KLEISLIR_Eps [lemma, in DomainStuff]
KLEISLIR_KR_eq2 [lemma, in DomainStuff]
KLEISLIR_KR_eq [lemma, in DomainStuff]
KLEISLIR_PBot [lemma, in DomainStuff]
KLEISLIR_unit2 [lemma, in DomainStuff]
KLEISLI_RL_Val [lemma, in DomainStuff]
KLEISLI_LR_Val [lemma, in DomainStuff]
KLESILIL_lub_comp_eq [lemma, in DomainStuff]
KLESILIR_lub_comp_eq [lemma, in DomainStuff]
KR [definition, in DomainStuff]
KRInj [lemma, in MoT]
KRInjLe [lemma, in MoT]
KRKUR_id2 [lemma, in DomainStuff]
KRKUR_id [lemma, in DomainStuff]
KUR [definition, in DomainStuff]
KURKR_id2 [lemma, in DomainStuff]
KURKR_id [lemma, in DomainStuff]
L
Lang [library]LCtx [definition, in Types]
LeOP [constructor, in Lang]
LET [constructor, in Lang]
LetApp [definition, in ExSem]
LetAppDInf [definition, in ExSem]
LetRule [constructor, in Types]
LetRule_simpl [lemma, in InSem]
LetTy [definition, in InSem]
LET_Val [lemma, in InSem]
lift [definition, in Lang]
liftComposeRen [lemma, in Lang]
liftComposeRenSub [lemma, in Lang]
liftComposeSub [lemma, in Lang]
liftIdMap [lemma, in Lang]
LiftMapDef [lemma, in Lang]
liftRen [definition, in Lang]
liftSub [definition, in Lang]
lookupType [definition, in Types]
lookupV [definition, in Types]
LType [inductive, in Types]
lub_discrete_chain [lemma, in DomainStuff]
lub_prod_fun [lemma, in PredomProd]
M
Map [definition, in Lang]MAP [section, in Lang]
mapAPP [lemma, in Lang]
mapBOOL [lemma, in Lang]
mapBOp [lemma, in Lang]
mapE [definition, in Lang]
MapExtensional [axiom, in Lang]
mapFST [lemma, in Lang]
mapFUN [lemma, in Lang]
mapIFB [lemma, in Lang]
mapLET [lemma, in Lang]
mapNAT [lemma, in Lang]
mapNOp [lemma, in Lang]
mapOOp [lemma, in Lang]
MapOps [record, in Lang]
mapPAIR [lemma, in Lang]
mapSND [lemma, in Lang]
mapV [definition, in Lang]
mapVAL [lemma, in Lang]
mapVAR [lemma, in Lang]
MAP.E [variable, in Lang]
MAP.E' [variable, in Lang]
MAP.m [variable, in Lang]
MAP.ops [variable, in Lang]
MAP.P [variable, in Lang]
miguel [lemma, in PredomProd]
MinusOP [constructor, in Lang]
mkrel [constructor, in OperApprox]
mkrelE [constructor, in DenoApprox]
MOD2 [definition, in ExSem]
mod2 [definition, in ExSem]
MoT [library]
mutual_VE_induction [definition, in Lang]
N
n [variable, in Adequacy]NAT [constructor, in Lang]
NatOp [inductive, in Lang]
NatOpLemma [lemma, in ExSem]
natopsimplE [lemma, in MoT]
NatRule [constructor, in Types]
NatRule_simpl [lemma, in InSem]
NatTy [constructor, in Types]
NOp [constructor, in Lang]
NOpRule [constructor, in Types]
NOpRule_Val2 [lemma, in InSem]
NOpRule_Val [lemma, in InSem]
NOpRule_simpl [lemma, in InSem]
N_to_B [definition, in DomainStuff]
n_steps [definition, in Adequacy]
O
OAC_Gen_StepI [lemma, in OperApprox]OAC_StepI [lemma, in OperApprox]
OAE_compat [lemma, in OperApprox]
OAE_Z_Fullset [lemma, in OperApprox]
OAE_Gen_StepI [lemma, in OperApprox]
OAE_StepI [lemma, in OperApprox]
OAV_compat [lemma, in OperApprox]
OAV_Gen_StepI [lemma, in OperApprox]
OAV_StepI [lemma, in OperApprox]
Omega_compat [lemma, in OperApprox]
OOp [constructor, in Lang]
OOpRule [constructor, in Types]
OOpRule_Val2 [lemma, in InSem]
OOpRule_Val [lemma, in InSem]
OOpRule_simpl [lemma, in InSem]
OperApprox [section, in OperApprox]
OperApprox [library]
OperApproxCtx [definition, in OperApprox]
OperApproxE [definition, in OperApprox]
OperApproxV [definition, in OperApprox]
OperApprox.RE [variable, in OperApprox]
_ e⊢ _ ◀̂ _ ⦂ _ [notation, in OperApprox]
_ v⊢ _ ◁̂ _ ⦂ _ [notation, in OperApprox]
_ ⊴ _ | _ ⦂ _ [notation, in OperApprox]
_ ◀ _ | _ ⦂ _ [notation, in OperApprox]
_ ◁ _ | _ ⦂ _ [notation, in OperApprox]
↓r _ [notation, in OperApprox]
↓ _ [notation, in OperApprox]
⇑ _ [notation, in OperApprox]
Operator2_reverse [definition, in DomainStuff]
Operator2_strictR [lemma, in DomainStuff]
Operator2_strictL [lemma, in DomainStuff]
OperSem [library]
OpPlus [definition, in DomainStuff]
OpSimplL [lemma, in MoT]
OpSimplR [lemma, in MoT]
Op_B_to_N [definition, in OperSem]
OrdOp [inductive, in Lang]
OrdOpLemma [lemma, in ExSem]
ordopsimplE [lemma, in MoT]
OrdRelBFun [lemma, in MoT]
OrdRelBinFun [lemma, in MoT]
OrdsimpE [lemma, in MoT]
OrdsimpE' [lemma, in MoT]
OrOP [constructor, in Lang]
P
pairInj_eq [lemma, in DomainStuff]PAIRL [definition, in DomainStuff]
Pairl [definition, in DomainStuff]
Pairl_cont [lemma, in DomainStuff]
pairl_mon [lemma, in DomainStuff]
PairOp [definition, in ExSem]
PairRule [constructor, in Types]
PairTy [definition, in InSem]
PairTy [constructor, in Types]
PAIR_eq [lemma, in DomainStuff]
PF [lemma, in MoT]
PF_subs_Rho [lemma, in MoT]
PF_subs_rho [lemma, in MoT]
PF_subs_Delta [lemma, in MoT]
PF_subs_delta [lemma, in MoT]
PF_SND [lemma, in MoT]
PF_FST [lemma, in MoT]
PF_FUN [lemma, in MoT]
PF_APP [lemma, in MoT]
PF_IFB [lemma, in MoT]
PF_IFB_unfolded [lemma, in MoT]
PF_LET [lemma, in MoT]
PF_LET_unfolded [lemma, in MoT]
PF_subs_E' [lemma, in OperApprox]
PF_subs_V' [lemma, in OperApprox]
PF_subs_E [lemma, in OperApprox]
PF_subs_V [lemma, in OperApprox]
PF_subs_E_IC [lemma, in DenoApprox]
PF_subs_V_IC [lemma, in DenoApprox]
PF_subs_E' [lemma, in DenoApprox]
PF_subs_V' [lemma, in DenoApprox]
PF_subs_E [lemma, in DenoApprox]
PF_subs_V [lemma, in DenoApprox]
PlusOP [constructor, in Lang]
pprodc_morph [definition, in PredomProd]
PredomProd [library]
pred_val_val [lemma, in StrictExt]
pred_eps_val [lemma, in StrictExt]
pred_Bot [lemma, in StrictExt]
prodc_morph [definition, in PredomProd]
PRODc_morph [definition, in PredomProd]
prodm_morph [definition, in PredomProd]
PRODm_morph [definition, in PredomProd]
prod_simpl [lemma, in DomainStuff]
prod_morph [definition, in PredomProd]
PUSHCond [constructor, in Lang]
PUSHLBOp [constructor, in Lang]
PUSHLet [constructor, in Lang]
PUSHLNOp [constructor, in Lang]
PUSHLOOp [constructor, in Lang]
PUSHRBOp [constructor, in Lang]
PUSHRNOp [constructor, in Lang]
PUSHROOp [constructor, in Lang]
R
RD [module, in Domains]RD.biConst [definition, in Domains]
RD.biFun [definition, in Domains]
RD.bifunc [lemma, in Domains]
RD.bifunm [lemma, in Domains]
RD.biProd [definition, in Domains]
RD.biSum [definition, in Domains]
RD.biVar [definition, in Domains]
RD.bi_fun_simpl [lemma, in Domains]
RD.bi_fun [definition, in Domains]
RD.comp_simpl [lemma, in Domains]
RD.delta [definition, in Domains]
RD.delta_eta [lemma, in Domains]
RD.delta_simpl [lemma, in Domains]
RD.DInf [definition, in Domains]
RD.eta_mono [lemma, in Domains]
RD.Fold [definition, in Domains]
RD.foldT [lemma, in Domains]
RD.FS [definition, in Domains]
RD.FU_iso [lemma, in Domains]
RD.id_min [lemma, in Domains]
RD.inBool [definition, in Domains]
RD.inFun [definition, in Domains]
RD.inNat [definition, in Domains]
RD.inPair [definition, in Domains]
RD.kcpoBaseCatMixin [definition, in Domains]
RD.kcpoCocone [definition, in Domains]
RD.kcpoCone [definition, in Domains]
RD.kcpoLimit [definition, in Domains]
RD.kcpoTerminalAxiom [lemma, in Domains]
RD.kcpo_comp_eq [lemma, in Domains]
RD.leftss [lemma, in Domains]
RD.limit_def [lemma, in Domains]
RD.ob [lemma, in Domains]
RD.prodc [lemma, in Domains]
RD.prodm [definition, in Domains]
RD.prodm_mon [lemma, in Domains]
RD.prod_func [definition, in Domains]
RD.ProjSet [definition, in Domains]
RD.ProjSet_inclusive [lemma, in Domains]
RD.retract_total [lemma, in Domains]
RD.Roll [definition, in Domains]
RD.RU_id [lemma, in Domains]
RD.sumc [lemma, in Domains]
RD.summ [definition, in Domains]
RD.summ_mon [lemma, in Domains]
RD.sum_func_simpl [lemma, in Domains]
RD.sum_func [definition, in Domains]
RD.UF_iso [lemma, in Domains]
RD.Unfold [definition, in Domains]
RD.unfoldT [lemma, in Domains]
RD.Unroll [definition, in Domains]
RD.UR_id [lemma, in Domains]
RD.VInf [definition, in Domains]
RD.xx [lemma, in Domains]
RecDom [module, in Domains]
RecDom.delta [variable, in Domains]
RecDom.delta_eta [variable, in Domains]
RecDom.delta_simpl [variable, in Domains]
RecDom.DInf [variable, in Domains]
RecDom.id_min [variable, in Domains]
RecDom.inBool [definition, in Domains]
RecDom.inFun [definition, in Domains]
RecDom.inNat [definition, in Domains]
RecDom.inPair [definition, in Domains]
RecDom.Roll [variable, in Domains]
RecDom.RU_id [variable, in Domains]
RecDom.Unroll [variable, in Domains]
RecDom.UR_id [variable, in Domains]
RecDom.VInf [definition, in Domains]
ReflRule [constructor, in Types]
rel [projection, in OperApprox]
rel [projection, in DenoApprox]
RelBFun [lemma, in MoT]
RelBinFun [lemma, in MoT]
RelE [record, in OperApprox]
RelE [record, in DenoApprox]
RelE_down_closed [lemma, in OperApprox]
RelFunc [definition, in StrictExt]
RelMono [definition, in StrictExt]
RelStable [definition, in StrictExt]
Ren [definition, in Lang]
renE [definition, in Lang]
RenMapOps [definition, in Lang]
renV [definition, in Lang]
RE_eq_Fullset [lemma, in OperApprox]
rhoBoolCComp [lemma, in MoT]
rhoBoolCompat [lemma, in MoT]
rhoBoolOp [lemma, in MoT]
rhoC [definition, in MoT]
RhoE [definition, in MoT]
rhoE_To_I_Eq_Pair [lemma, in MoT]
rhoE_To_I_Leq_Pair [lemma, in MoT]
rhoE_To_I_Geq_Pair [lemma, in MoT]
rhoE_E_In_Pair [lemma, in MoT]
rhoE_To_I_Eq_Arr [lemma, in MoT]
rhoE_To_I_Geq_Arr [lemma, in MoT]
rhoE_To_I_Leq_Arr [lemma, in MoT]
rhoE_To_I_Eq_Nat [lemma, in MoT]
rhoE_To_I_Geq_Nat [lemma, in MoT]
rhoE_To_I_Leq_Nat [lemma, in MoT]
rhoE_To_I_Eq_Bool [lemma, in MoT]
rhoE_To_I_Geq_Bool [lemma, in MoT]
rhoE_To_I_Leq_Bool [lemma, in MoT]
rhoE_E_In_Arr [lemma, in MoT]
rhoE_E_In_Nat [lemma, in MoT]
rhoE_E_In_Bool [lemma, in MoT]
rhoE_To_I_Eq [definition, in MoT]
rhoE_To_I_Geq [definition, in MoT]
rhoE_To_I_Leq [definition, in MoT]
rhoE_E_In [definition, in MoT]
rhoNatCComp [lemma, in MoT]
rhoNatCompat [lemma, in MoT]
rhoNatFunc [lemma, in MoT]
rhoNatOp [lemma, in MoT]
rhoOrdOp [lemma, in MoT]
RhoV [definition, in MoT]
rhoV_To_I_Eq_Pair [lemma, in MoT]
rhoV_E_In_Pair [lemma, in MoT]
rhoV_To_I_Eq_Arr [lemma, in MoT]
rhoV_To_I_Geq_Arr [lemma, in MoT]
rhoV_To_I_Leq_Arr [lemma, in MoT]
rhoV_To_I_Eq_Nat [lemma, in MoT]
rhoV_To_I_Eq_Bool [lemma, in MoT]
rhoV_E_In_Arr [lemma, in MoT]
rhoV_E_In_Nat [lemma, in MoT]
rhoV_E_In_Bool [lemma, in MoT]
rhoV_To_I_Eq [definition, in MoT]
rhoV_To_I_Geq [definition, in MoT]
rhoV_To_I_Leq [definition, in MoT]
rhoV_E_In [definition, in MoT]
rho_strict [lemma, in MoT]
RollInj [lemma, in MoT]
RollInjle [lemma, in MoT]
RUid [lemma, in DomainStuff]
S
SB [constructor, in StrictExt]SBOp [constructor, in OperSem]
SBotIn [lemma, in StrictExt]
SE [inductive, in StrictExt]
SEBotOutGL [lemma, in StrictExt]
SEBotOutL [lemma, in StrictExt]
SEChainComplete [lemma, in StrictExt]
SEChainCompleteG [lemma, in StrictExt]
SEChainCompleteVal [lemma, in StrictExt]
SEEpsL [lemma, in StrictExt]
SEEpsR [lemma, in StrictExt]
SEFunc [lemma, in StrictExt]
SEFuncEps [lemma, in StrictExt]
SEFuncVal [lemma, in StrictExt]
SemBoolOp [definition, in Lang]
SemBoolToNatRule [definition, in Types]
SemCtx [definition, in Types]
SemE [definition, in ExSem]
SemEnv [definition, in ExSem]
SemExp_LET_KR_equation [lemma, in ExSem]
SemExp_NatOp_equation [lemma, in ExSem]
SemExp_BoolOp_equation [lemma, in ExSem]
SemExp_OrdOp_equation [lemma, in ExSem]
SemExp_IFZ_equationVal2 [lemma, in ExSem]
SemExp_LET_equationVal2 [lemma, in ExSem]
SemExp_NatOp_equationNatNat2 [lemma, in ExSem]
SemExp_BoolOp_equationNatNat2 [lemma, in ExSem]
SemExp_OrdOp_equationNatNat2 [lemma, in ExSem]
SemExp_LET_equationVal [lemma, in ExSem]
SemExp_LET_equation_Bot [lemma, in ExSem]
SemExp_BoolOp_equation_Bot [lemma, in ExSem]
SemExp_OrdOp_equation_Bot [lemma, in ExSem]
SemExp_NatOp_equation_Bot [lemma, in ExSem]
SemExp_NatOp_equationNatNat [lemma, in ExSem]
SemExp_BoolOp_equationNatNat [lemma, in ExSem]
SemExp_OrdOp_equationNatNat [lemma, in ExSem]
SemExp_VAL_equation [lemma, in ExSem]
SemNatOp [definition, in Lang]
SEMonEps [lemma, in StrictExt]
SemOper [inductive, in OperSem]
SemOperDiverge [definition, in OperSem]
SemOperStar [definition, in OperSem]
SemOperStep [inductive, in OperSem]
SemOper_n_steps_iSet [definition, in Adequacy]
SemOper_ω_steps [definition, in Adequacy]
SemOper_n_steps [definition, in Adequacy]
SemOrdOp [definition, in Lang]
SemSubFunRule [definition, in Types]
SemType [definition, in Types]
SemTypeJudgeL [definition, in Types]
SemV [definition, in ExSem]
SemVal_FUN_equation2 [lemma, in ExSem]
SemVal_FUN_equation [lemma, in ExSem]
SemVal_INT_equation [lemma, in ExSem]
SemVal_VAR_equation [lemma, in ExSem]
SemVar [definition, in ExSem]
SEPredEpsL [lemma, in StrictExt]
SEPredEpsR [lemma, in StrictExt]
SEPredL [lemma, in StrictExt]
SEPrednthL [lemma, in StrictExt]
SEPrednthR [lemma, in StrictExt]
SEPredR [lemma, in StrictExt]
SEStable [lemma, in StrictExt]
SEStableL [lemma, in StrictExt]
SEStableR [lemma, in StrictExt]
SESym [lemma, in StrictExt]
SEValOutL [lemma, in StrictExt]
SEValOutR [lemma, in StrictExt]
SEValStable [lemma, in StrictExt]
shiftConsMap [lemma, in Lang]
shiftMap [definition, in Lang]
shiftRen [definition, in Lang]
shiftSub [definition, in Lang]
simpE [lemma, in MoT]
simpE' [lemma, in MoT]
SimpleBOp [definition, in DomainStuff]
SimpleBOpm [definition, in DomainStuff]
SimpleB_cont [lemma, in DomainStuff]
SimpleB_mon [lemma, in DomainStuff]
SimpleUOp [definition, in DomainStuff]
SimpleUOpm [definition, in DomainStuff]
SimpleU_cont [lemma, in DomainStuff]
SimpleU_mon [lemma, in DomainStuff]
simplToArr_Pair [lemma, in EmbProjPair]
simplToArr_inl_inl [lemma, in EmbProjPair]
simplToArr_Arr [lemma, in EmbProjPair]
simplToBool_inr [lemma, in EmbProjPair]
simplToBool_inl_inr [lemma, in EmbProjPair]
simplToBool_inl_inl [lemma, in EmbProjPair]
simplToNat_inr [lemma, in EmbProjPair]
simplToNat_inl_inr [lemma, in EmbProjPair]
simplToNat_Pair [lemma, in EmbProjPair]
simplToNat_Arr [lemma, in EmbProjPair]
simplToNat_Nat [lemma, in EmbProjPair]
simplToPair_Arr [lemma, in EmbProjPair]
simplToPair_inl [lemma, in EmbProjPair]
simplToPair_Pair [lemma, in EmbProjPair]
SLet [constructor, in OperSem]
SmashInv [lemma, in DomainStuff]
SmashLemmaValVal [lemma, in ExSem]
SmashLemma_Bot [lemma, in ExSem]
Smashs_eq [lemma, in DomainStuff]
Smash_ValVal [lemma, in DomainStuff]
Smash_Val [lemma, in DomainStuff]
Smash_Eps_r [lemma, in DomainStuff]
Smash_reverse [definition, in DomainStuff]
Smash_Eps_l [lemma, in DomainStuff]
Smash_ValVal [lemma, in PredomProd]
Smash_prop [lemma, in PredomProd]
Smash_prop_l [lemma, in PredomProd]
Smash_prop_r [lemma, in PredomProd]
Smash_Val [lemma, in PredomProd]
Smash_Eps_l [lemma, in PredomProd]
SndOp [constructor, in OperSem]
SNDOp [definition, in ExSem]
SNDRule [constructor, in Types]
SndTy [definition, in InSem]
SNOp [constructor, in OperSem]
SOOp [constructor, in OperSem]
stepI [projection, in OperApprox]
StepI_SemOper [lemma, in Adequacy]
StepLemma [lemma, in ExSem]
StrictExt [section, in StrictExt]
StrictExt [library]
StrictExtR [section, in StrictExt]
StrictExtR.D [variable, in StrictExt]
StrictExtR.D' [variable, in StrictExt]
StrictExtR.R [variable, in StrictExt]
StrictExt.D [variable, in StrictExt]
StrictExt.D' [variable, in StrictExt]
StrictExt.R [variable, in StrictExt]
strong_induction [lemma, in fib_Adequacy]
Sub [definition, in Lang]
subE [definition, in Lang]
SubFunRule [constructor, in Types]
SubMapOps [definition, in Lang]
SubPairRule [constructor, in Types]
SubsRule [constructor, in Types]
Subst [constructor, in OperSem]
substComposeSub [lemma, in Lang]
SubsVRule [constructor, in Types]
subV [definition, in Lang]
SV [constructor, in StrictExt]
SVAR [constructor, in Lang]
S_Step [constructor, in OperSem]
T
tlConsMap [lemma, in Lang]tlMap [definition, in Lang]
toArrBot [lemma, in EmbProjPair]
toArrEps [lemma, in EmbProjPair]
toArrVal [lemma, in EmbProjPair]
toE [definition, in EmbProjPair]
toEApp [lemma, in MoT]
toEArr [definition, in EmbProjPair]
toFromBool [lemma, in EmbProjPair]
toFromNat [lemma, in EmbProjPair]
toI [definition, in EmbProjPair]
toIArr [definition, in EmbProjPair]
toIDec [lemma, in EmbProjPair]
toIEps [lemma, in EmbProjPair]
toIProdInv [lemma, in EmbProjPair]
toIVal [lemma, in EmbProjPair]
toIValB [lemma, in EmbProjPair]
toNatBot [lemma, in EmbProjPair]
To_b [definition, in Adequacy]
to_const_antiE_b [lemma, in Adequacy]
to_b [definition, in Adequacy]
To_n [definition, in Adequacy]
to_const_antiE [lemma, in Adequacy]
to_n [definition, in Adequacy]
TranspCC [lemma, in StrictExt]
TranspSE [lemma, in StrictExt]
TranspStable [lemma, in StrictExt]
TransRule [constructor, in Types]
travE [definition, in Lang]
travV [definition, in Lang]
true_sum_computes [lemma, in CoherenceExample]
true_sum_false [definition, in CoherenceExample]
TypeJudgeE [inductive, in Types]
TypeJudgeL [inductive, in Types]
TypeJudgeV [inductive, in Types]
Types [library]
U
UNCURRY [definition, in DomainStuff]UnCurry_cont [lemma, in DomainStuff]
UNCURRY_mon [definition, in DomainStuff]
UnCurry_mon [lemma, in DomainStuff]
URid [lemma, in DomainStuff]
Utils [library]
V
V [inductive, in Lang]VAL [constructor, in Lang]
ValMono [lemma, in StrictExt]
ValNotBot [lemma, in StrictExt]
valNotRelBotL [lemma, in StrictExt]
valNotRelBotR [lemma, in StrictExt]
ValRule [constructor, in Types]
ValRule_simpl [lemma, in InSem]
VAR [constructor, in Lang]
Var [inductive, in Lang]
VarRule [constructor, in Types]
VarRule_simpl [lemma, in InSem]
VInfToBool [definition, in ExSem]
VInfToBool_prop [lemma, in ExSem]
VInfToFun [definition, in ExSem]
VInfToFun_Fun [lemma, in ExSem]
VInfToNat [definition, in ExSem]
VInfToNat_prop [lemma, in MoT]
VInfToNat_Nat [lemma, in ExSem]
VInfToPair [definition, in ExSem]
vl [projection, in Lang]
vlvr [projection, in Lang]
VPAIR [constructor, in Lang]
vr [projection, in Lang]
V_v3 [definition, in CoherenceExample]
V_v2 [definition, in CoherenceExample]
V_v1 [definition, in CoherenceExample]
V_v0 [definition, in CoherenceExample]
V_False [definition, in CoherenceExample]
V_True [definition, in CoherenceExample]
V_induction [definition, in Lang]
V_Fib [definition, in fib_Adequacy]
V_Two [definition, in fib_Adequacy]
V_One [definition, in fib_Adequacy]
V_Zero [definition, in fib_Adequacy]
V_v3 [definition, in fib_Adequacy]
V_v2 [definition, in fib_Adequacy]
V_v1 [definition, in fib_Adequacy]
V_v0 [definition, in fib_Adequacy]
v0 [definition, in CoherenceExample]
v0 [definition, in fib_Adequacy]
V0_eq_1 [definition, in fib_Adequacy]
V0_eq_0 [definition, in fib_Adequacy]
v1 [definition, in CoherenceExample]
v1 [definition, in fib_Adequacy]
v2 [definition, in CoherenceExample]
v2 [definition, in fib_Adequacy]
v3 [definition, in CoherenceExample]
v3 [definition, in fib_Adequacy]
W
wk [projection, in Lang]wkvr [projection, in Lang]
Z
ZVAR [constructor, in Lang]Z_Step [constructor, in OperSem]
_
_EmbProjPair [lemma, in EmbProjPair]_toEArr [definition, in EmbProjPair]
_toIArr [definition, in EmbProjPair]
_rho [definition, in MoT]
_delta [definition, in MoT]
other
[ _ , .. , _ ] (Sub_scope) [notation, in Lang]_ ⎩ _ ⎭ [notation, in Lang]
_ ⎧ _ ⎫ [notation, in Lang]
_ ∘ ( _ ⇆ _ ) [notation, in Lang]
_ ∘ ( ⊡ ⦓ _ ⦔ _ ) [notation, in Lang]
_ ∘ ( _ ⦓ _ ⦔ ⊡ ) [notation, in Lang]
_ ⊚ _ [notation, in Lang]
_ @ _ [notation, in Lang]
_ ∈ _ [notation, in OperApprox]
_ ∉ _ [notation, in OperApprox]
_ ∈ _ [notation, in DenoApprox]
_ ∉ _ [notation, in DenoApprox]
_ ⟼⋆ _ [notation, in OperSem]
_ ⟼ _ [notation, in OperSem]
_ ⇡ [notation, in Adequacy]
_ ∈ _ [notation, in Adequacy]
_ ∉ _ [notation, in Adequacy]
_ e⊢ _ ⦂ _ [notation, in Types]
_ v⊢ _ ⦂ _ [notation, in Types]
_ t≤ _ [notation, in Types]
_ × _ [notation, in Types]
_ ⨱ _ [notation, in Types]
_ ⇥ _ [notation, in Types]
_ ↓f _ [notation, in ExSem]
_ ⊥⊥⃑ _ [notation, in ExSem]
_ !! _ [notation, in ExSem]
bool̂ [notation, in Types]
e⎨ _ ⎬ [notation, in Lang]
nat̂ [notation, in Types]
t⟦ _ ⟧e [notation, in InSem]
t⟦ _ ⟧v [notation, in InSem]
t⟦ _ ⟧l [notation, in Types]
v⎨ _ ⎬ [notation, in Lang]
? [notation, in Utils]
[] [notation, in Types]
↑f _ [notation, in ExSem]
↑f⊥ _ [notation, in ExSem]
↑n _ [notation, in ExSem]
↑n⊥ _ [notation, in ExSem]
↑p _ [notation, in ExSem]
↑p⊥ _ [notation, in ExSem]
↑ [notation, in EmbProjPair]
↑⊥ _ [notation, in ExSem]
↑⊥ _ [notation, in ExSem]
↓ [notation, in EmbProjPair]
⇈ [notation, in EmbProjPair]
⇊ [notation, in EmbProjPair]
⇓ [notation, in EmbProjPair]
∅ [notation, in Lang]
⊥ [notation, in ExSem]
⌊ _ ⌋ [notation, in Lang]
⎣ _ ⎦ [notation, in Lang]
⟦ _ ⟧v [notation, in ExSem]
⟦ _ ⟧e [notation, in ExSem]
⦓ _ ⦔ [notation, in ExSem]
Δ[ _ , _ ] [notation, in MoT]
Ρ[ _ , _ ] [notation, in MoT]
γ[ _ ] [notation, in MoT]
δ[ _ ] [notation, in MoT]
λ _ [notation, in Lang]
ρ[ _ ] [notation, in MoT]
Ω [definition, in OperApprox]
Ω [definition, in DenoApprox]
Ω_down_closed [lemma, in OperApprox]
Notation Index
A
_ e⊢ _ ▶̂ _ ⦂ _ [in Adequacy]_ v⊢ _ ▷̂ _ ⦂ _ [in Adequacy]
_ e⊢ _ ▶̂̅ _ ⦂ _ [in Adequacy]
_ v⊢ _ ▷̂̅ _ ⦂ _ [in Adequacy]
_ ⊵ _ ⦂ _ [in Adequacy]
_ ▷̅ _ ⦂ _ [in Adequacy]
_ ▷ _ ⦂ _ [in Adequacy]
⇑ _ [in Adequacy]
↓ _ [in Adequacy]
↓r _ [in Adequacy]
_ e⊢ _ ▶̂ _ ⦂ _ [in Adequacy]
_ v⊢ _ ▷̂ _ ⦂ _ [in Adequacy]
_ e⊢ _ ▶̂̅ _ ⦂ _ [in Adequacy]
_ v⊢ _ ▷̂̅ _ ⦂ _ [in Adequacy]
_ ⊵ _ ⦂ _ [in Adequacy]
_ ▷̅ _ ⦂ _ [in Adequacy]
_ ▷ _ ⦂ _ [in Adequacy]
⇑ _ [in Adequacy]
↓ _ [in Adequacy]
↓r _ [in Adequacy]
_ e⊢ _ ◀̂ _ ⦂ _ [in Adequacy]
_ v⊢ _ ◁̂ _ ⦂ _ [in Adequacy]
_ ⊴ _ | _ ⦂ _ [in Adequacy]
_ ◀ _ | _ ⦂ _ [in Adequacy]
_ ◁ _ | _ ⦂ _ [in Adequacy]
_ ⇡ [in Adequacy]
_ ⟿ _ [in Adequacy]
↓r _ [in Adequacy]
↓ _ [in Adequacy]
⇑ _ [in Adequacy]
D
_ e⊢ _ ▶̂ _ ⦂ _ [in DenoApprox]_ v⊢ _ ▷̂ _ ⦂ _ [in DenoApprox]
_ e⊢ _ ▶̂̅ _ ⦂ _ [in DenoApprox]
_ v⊢ _ ▷̂̅ _ ⦂ _ [in DenoApprox]
_ ⊵ _ ⦂ _ [in DenoApprox]
_ ▶ _ ⦂ _ [in DenoApprox]
_ ▷ _ ⦂ _ [in DenoApprox]
↓r _ [in DenoApprox]
↓ _ [in DenoApprox]
⇑ _ [in DenoApprox]
O
_ e⊢ _ ◀̂ _ ⦂ _ [in OperApprox]_ v⊢ _ ◁̂ _ ⦂ _ [in OperApprox]
_ ⊴ _ | _ ⦂ _ [in OperApprox]
_ ◀ _ | _ ⦂ _ [in OperApprox]
_ ◁ _ | _ ⦂ _ [in OperApprox]
↓r _ [in OperApprox]
↓ _ [in OperApprox]
⇑ _ [in OperApprox]
other
[ _ , .. , _ ] (Sub_scope) [in Lang]_ ⎩ _ ⎭ [in Lang]
_ ⎧ _ ⎫ [in Lang]
_ ∘ ( _ ⇆ _ ) [in Lang]
_ ∘ ( ⊡ ⦓ _ ⦔ _ ) [in Lang]
_ ∘ ( _ ⦓ _ ⦔ ⊡ ) [in Lang]
_ ⊚ _ [in Lang]
_ @ _ [in Lang]
_ ∈ _ [in OperApprox]
_ ∉ _ [in OperApprox]
_ ∈ _ [in DenoApprox]
_ ∉ _ [in DenoApprox]
_ ⟼⋆ _ [in OperSem]
_ ⟼ _ [in OperSem]
_ ⇡ [in Adequacy]
_ ∈ _ [in Adequacy]
_ ∉ _ [in Adequacy]
_ e⊢ _ ⦂ _ [in Types]
_ v⊢ _ ⦂ _ [in Types]
_ t≤ _ [in Types]
_ × _ [in Types]
_ ⨱ _ [in Types]
_ ⇥ _ [in Types]
_ ↓f _ [in ExSem]
_ ⊥⊥⃑ _ [in ExSem]
_ !! _ [in ExSem]
bool̂ [in Types]
e⎨ _ ⎬ [in Lang]
nat̂ [in Types]
t⟦ _ ⟧e [in InSem]
t⟦ _ ⟧v [in InSem]
t⟦ _ ⟧l [in Types]
v⎨ _ ⎬ [in Lang]
? [in Utils]
[] [in Types]
↑f _ [in ExSem]
↑f⊥ _ [in ExSem]
↑n _ [in ExSem]
↑n⊥ _ [in ExSem]
↑p _ [in ExSem]
↑p⊥ _ [in ExSem]
↑ [in EmbProjPair]
↑⊥ _ [in ExSem]
↑⊥ _ [in ExSem]
↓ [in EmbProjPair]
⇈ [in EmbProjPair]
⇊ [in EmbProjPair]
⇓ [in EmbProjPair]
∅ [in Lang]
⊥ [in ExSem]
⌊ _ ⌋ [in Lang]
⎣ _ ⎦ [in Lang]
⟦ _ ⟧v [in ExSem]
⟦ _ ⟧e [in ExSem]
⦓ _ ⦔ [in ExSem]
Δ[ _ , _ ] [in MoT]
Ρ[ _ , _ ] [in MoT]
γ[ _ ] [in MoT]
δ[ _ ] [in MoT]
λ _ [in Lang]
ρ[ _ ] [in MoT]
Module Index
R
RD [in Domains]RecDom [in Domains]
Variable Index
A
Adequacy1_b.b [in Adequacy]Adequacy1_n.n [in Adequacy]
B
b [in Adequacy]D
DenoApprox.RE [in DenoApprox]F
Fib_Adequacy.n [in fib_Adequacy]M
MAP.E [in Lang]MAP.E' [in Lang]
MAP.m [in Lang]
MAP.ops [in Lang]
MAP.P [in Lang]
N
n [in Adequacy]O
OperApprox.RE [in OperApprox]R
RecDom.delta [in Domains]RecDom.delta_eta [in Domains]
RecDom.delta_simpl [in Domains]
RecDom.DInf [in Domains]
RecDom.id_min [in Domains]
RecDom.Roll [in Domains]
RecDom.RU_id [in Domains]
RecDom.Unroll [in Domains]
RecDom.UR_id [in Domains]
S
StrictExtR.D [in StrictExt]StrictExtR.D' [in StrictExt]
StrictExtR.R [in StrictExt]
StrictExt.D [in StrictExt]
StrictExt.D' [in StrictExt]
StrictExt.R [in StrictExt]
Library Index
A
AdequacyC
CoherenceExampleD
DenoApproxDomains
DomainStuff
E
EmbProjPairExSem
F
fib_AdequacyI
InSemL
LangM
MoTO
OperApproxOperSem
P
PredomProdS
StrictExtT
TypesU
UtilsLemma Index
A
able [in PredomProd]Adequacy1_b [in Adequacy]
Adequacy1_n [in Adequacy]
Adequacy2 [in Adequacy]
AntiE_SemOper [in Adequacy]
appCase [in MoT]
applyComposeRen [in Lang]
applyComposeRenSub [in Lang]
applyIdMap [in Lang]
ApproxEquivE [in DenoApprox]
ApproxEquivV [in DenoApprox]
AppRule_simpl [in InSem]
B
bbot_down_closed [in OperApprox]ble [in Adequacy]
BoolOpLemma [in ExSem]
boolopsimplE [in MoT]
BoolRelBFun [in MoT]
BoolRelBinFun [in MoT]
BoolsimpE [in MoT]
BoolsimpE' [in MoT]
bool_sum_coherent [in CoherenceExample]
bool_sum_app_tj' [in CoherenceExample]
bool_sum_app_tj [in CoherenceExample]
bool_sum_tj' [in CoherenceExample]
bool_sum_tj [in CoherenceExample]
BOpRule_Val2 [in InSem]
BOpRule_Val [in InSem]
BOpRule_simpl [in InSem]
Bracketing [in MoT]
BTONInj [in MoT]
C
Case1 [in OperApprox]Case1 [in DenoApprox]
Case1_IC [in DenoApprox]
Case10 [in OperApprox]
Case10 [in DenoApprox]
Case10_IC [in DenoApprox]
Case11 [in OperApprox]
Case11 [in DenoApprox]
Case11_IC [in DenoApprox]
Case12 [in OperApprox]
Case12 [in DenoApprox]
Case12_IC [in DenoApprox]
Case2 [in OperApprox]
Case2 [in DenoApprox]
Case2_IC [in DenoApprox]
Case3 [in OperApprox]
Case3 [in DenoApprox]
Case3_IC [in DenoApprox]
Case4 [in OperApprox]
Case4 [in DenoApprox]
Case4_IC [in DenoApprox]
Case5 [in OperApprox]
Case5 [in DenoApprox]
Case5_IC [in DenoApprox]
Case6 [in OperApprox]
Case6 [in DenoApprox]
Case6_IC [in DenoApprox]
Case7 [in OperApprox]
Case7 [in DenoApprox]
Case7_IC [in DenoApprox]
Case8 [in OperApprox]
Case8 [in DenoApprox]
Case8_IC [in DenoApprox]
Case9 [in OperApprox]
Case9 [in DenoApprox]
Case9_IC [in DenoApprox]
closed_star_transition [in OperSem]
closed_transition [in OperSem]
Coherence [in MoT]
composeCons [in Lang]
composeSubIdLeft [in Lang]
composeSubIdRight [in Lang]
comp_simpl [in DomainStuff]
consMapEta [in Lang]
coq_fib_prop2 [in fib_Adequacy]
coq_fib_prop [in fib_Adequacy]
Curry1_cont [in DomainStuff]
Curry1_mon [in DomainStuff]
D
deltaArrCComp [in MoT]deltaArrow [in MoT]
deltaBoolCComp [in MoT]
deltaBoolCompat [in MoT]
deltaBoolFunc [in MoT]
deltaBoolOpP [in MoT]
deltaNatCComp [in MoT]
deltaNatCompat [in MoT]
deltaNatFunc [in MoT]
deltaNatOp [in MoT]
deltaNatOpP [in MoT]
deltaNatOpt [in MoT]
deltaOrdOpP [in MoT]
deltaPairCComp [in MoT]
deltaPairCompat [in MoT]
delta_rho_cc [in MoT]
delta_rho_compat [in MoT]
DenotApproxE_PBot [in DenoApprox]
DInfToNat_bot' [in MoT]
DInfToNat_bot [in MoT]
discrete_eq [in DomainStuff]
DLleEpsTrans [in DomainStuff]
DLleEq [in DomainStuff]
DLleEqR [in DomainStuff]
E
EmbProjPair [in EmbProjPair]EmbProjPair [in MoT]
EPPair_SemSubType [in MoT]
EpsStable [in DomainStuff]
eqLubChains [in StrictExt]
Expand2ApproxCtx [in OperApprox]
Expand2ApproxCtx [in DenoApprox]
Extrinsic_Adequacy_b [in Adequacy]
Extrinsic_Adequacy [in Adequacy]
Extrinsic_Adequacy1_b [in Adequacy]
Extrinsic_Adequacy1 [in Adequacy]
Ex_eqV_In [in MoT]
Ex_eq_In_b [in MoT]
Ex_eq_In [in MoT]
Ex_Adequacy_2_from_In [in Adequacy]
F
FChainCore_mon [in DenoApprox]FChainCore_S [in DenoApprox]
FChainCore_S_unfold [in DenoApprox]
FChainCore_unfold [in DenoApprox]
FChain_mon [in DenoApprox]
FChain_S [in DenoApprox]
FC_lub [in DenoApprox]
FC_unfold [in DenoApprox]
FC_zero [in DenoApprox]
FC_simpl [in DenoApprox]
fib [in fib_Adequacy]
FibCorr [in fib_Adequacy]
fibn_eq [in fib_Adequacy]
fibn_prop [in fib_Adequacy]
fib_body [in fib_Adequacy]
FIXP_Step [in OperApprox]
FIXP_Prop [in DenoApprox]
fmon_eq_bot [in DenoApprox]
fromRel [in MoT]
fromToBool [in EmbProjPair]
fromToNat [in EmbProjPair]
FS_In_compat [in OperApprox]
FuncToMono [in StrictExt]
FundamentalPropOfLogicalRelations [in OperApprox]
FundamentalPropOfLogicalRelations [in DenoApprox]
FunRule_simpl [in InSem]
G
Gamma_E_In [in MoT]GenBinOpSimpl [in MoT]
genbinopsimpl [in MoT]
H
hdConsMap [in Lang]I
idMapDef [in Lang]IfBCore_cont2 [in DomainStuff]
IfBCore_mon2 [in DomainStuff]
IfBCore_mon [in DomainStuff]
IfZCore_cont2 [in DomainStuff]
IfZCore_mon2 [in DomainStuff]
IfZCore_mon [in DomainStuff]
IfZRule_simpl [in InSem]
IFZ_Val [in InSem]
INL_convert [in ExSem]
InSemFun_unfold [in InSem]
Intrinsic_Adequacy_b [in Adequacy]
Intrinsic_Adequacy [in Adequacy]
In_eqV_Ex [in MoT]
In_eq_Ex [in MoT]
In_Adequacy_1_from_Ex [in Adequacy]
K
kcpoCatAxiom [in Domains]KLEISLIL_Eps [in DomainStuff]
KLEISLIL_PBot [in DomainStuff]
KLEISLIL_unit2 [in DomainStuff]
KLEISLIR_Eps [in DomainStuff]
KLEISLIR_KR_eq2 [in DomainStuff]
KLEISLIR_KR_eq [in DomainStuff]
KLEISLIR_PBot [in DomainStuff]
KLEISLIR_unit2 [in DomainStuff]
KLEISLI_RL_Val [in DomainStuff]
KLEISLI_LR_Val [in DomainStuff]
KLESILIL_lub_comp_eq [in DomainStuff]
KLESILIR_lub_comp_eq [in DomainStuff]
KRInj [in MoT]
KRInjLe [in MoT]
KRKUR_id2 [in DomainStuff]
KRKUR_id [in DomainStuff]
KURKR_id2 [in DomainStuff]
KURKR_id [in DomainStuff]
L
LetRule_simpl [in InSem]LET_Val [in InSem]
liftComposeRen [in Lang]
liftComposeRenSub [in Lang]
liftComposeSub [in Lang]
liftIdMap [in Lang]
LiftMapDef [in Lang]
lub_discrete_chain [in DomainStuff]
lub_prod_fun [in PredomProd]
M
mapAPP [in Lang]mapBOOL [in Lang]
mapBOp [in Lang]
mapFST [in Lang]
mapFUN [in Lang]
mapIFB [in Lang]
mapLET [in Lang]
mapNAT [in Lang]
mapNOp [in Lang]
mapOOp [in Lang]
mapPAIR [in Lang]
mapSND [in Lang]
mapVAL [in Lang]
mapVAR [in Lang]
miguel [in PredomProd]
N
NatOpLemma [in ExSem]natopsimplE [in MoT]
NatRule_simpl [in InSem]
NOpRule_Val2 [in InSem]
NOpRule_Val [in InSem]
NOpRule_simpl [in InSem]
O
OAC_Gen_StepI [in OperApprox]OAC_StepI [in OperApprox]
OAE_compat [in OperApprox]
OAE_Z_Fullset [in OperApprox]
OAE_Gen_StepI [in OperApprox]
OAE_StepI [in OperApprox]
OAV_compat [in OperApprox]
OAV_Gen_StepI [in OperApprox]
OAV_StepI [in OperApprox]
Omega_compat [in OperApprox]
OOpRule_Val2 [in InSem]
OOpRule_Val [in InSem]
OOpRule_simpl [in InSem]
Operator2_strictR [in DomainStuff]
Operator2_strictL [in DomainStuff]
OpSimplL [in MoT]
OpSimplR [in MoT]
OrdOpLemma [in ExSem]
ordopsimplE [in MoT]
OrdRelBFun [in MoT]
OrdRelBinFun [in MoT]
OrdsimpE [in MoT]
OrdsimpE' [in MoT]
P
pairInj_eq [in DomainStuff]Pairl_cont [in DomainStuff]
pairl_mon [in DomainStuff]
PAIR_eq [in DomainStuff]
PF [in MoT]
PF_subs_Rho [in MoT]
PF_subs_rho [in MoT]
PF_subs_Delta [in MoT]
PF_subs_delta [in MoT]
PF_SND [in MoT]
PF_FST [in MoT]
PF_FUN [in MoT]
PF_APP [in MoT]
PF_IFB [in MoT]
PF_IFB_unfolded [in MoT]
PF_LET [in MoT]
PF_LET_unfolded [in MoT]
PF_subs_E' [in OperApprox]
PF_subs_V' [in OperApprox]
PF_subs_E [in OperApprox]
PF_subs_V [in OperApprox]
PF_subs_E_IC [in DenoApprox]
PF_subs_V_IC [in DenoApprox]
PF_subs_E' [in DenoApprox]
PF_subs_V' [in DenoApprox]
PF_subs_E [in DenoApprox]
PF_subs_V [in DenoApprox]
pred_val_val [in StrictExt]
pred_eps_val [in StrictExt]
pred_Bot [in StrictExt]
prod_simpl [in DomainStuff]
R
RD.bifunc [in Domains]RD.bifunm [in Domains]
RD.bi_fun_simpl [in Domains]
RD.comp_simpl [in Domains]
RD.delta_eta [in Domains]
RD.delta_simpl [in Domains]
RD.eta_mono [in Domains]
RD.foldT [in Domains]
RD.FU_iso [in Domains]
RD.id_min [in Domains]
RD.kcpoTerminalAxiom [in Domains]
RD.kcpo_comp_eq [in Domains]
RD.leftss [in Domains]
RD.limit_def [in Domains]
RD.ob [in Domains]
RD.prodc [in Domains]
RD.prodm_mon [in Domains]
RD.ProjSet_inclusive [in Domains]
RD.retract_total [in Domains]
RD.RU_id [in Domains]
RD.sumc [in Domains]
RD.summ_mon [in Domains]
RD.sum_func_simpl [in Domains]
RD.UF_iso [in Domains]
RD.unfoldT [in Domains]
RD.UR_id [in Domains]
RD.xx [in Domains]
RelBFun [in MoT]
RelBinFun [in MoT]
RelE_down_closed [in OperApprox]
RE_eq_Fullset [in OperApprox]
rhoBoolCComp [in MoT]
rhoBoolCompat [in MoT]
rhoBoolOp [in MoT]
rhoE_To_I_Eq_Pair [in MoT]
rhoE_To_I_Leq_Pair [in MoT]
rhoE_To_I_Geq_Pair [in MoT]
rhoE_E_In_Pair [in MoT]
rhoE_To_I_Eq_Arr [in MoT]
rhoE_To_I_Geq_Arr [in MoT]
rhoE_To_I_Leq_Arr [in MoT]
rhoE_To_I_Eq_Nat [in MoT]
rhoE_To_I_Geq_Nat [in MoT]
rhoE_To_I_Leq_Nat [in MoT]
rhoE_To_I_Eq_Bool [in MoT]
rhoE_To_I_Geq_Bool [in MoT]
rhoE_To_I_Leq_Bool [in MoT]
rhoE_E_In_Arr [in MoT]
rhoE_E_In_Nat [in MoT]
rhoE_E_In_Bool [in MoT]
rhoNatCComp [in MoT]
rhoNatCompat [in MoT]
rhoNatFunc [in MoT]
rhoNatOp [in MoT]
rhoOrdOp [in MoT]
rhoV_To_I_Eq_Pair [in MoT]
rhoV_E_In_Pair [in MoT]
rhoV_To_I_Eq_Arr [in MoT]
rhoV_To_I_Geq_Arr [in MoT]
rhoV_To_I_Leq_Arr [in MoT]
rhoV_To_I_Eq_Nat [in MoT]
rhoV_To_I_Eq_Bool [in MoT]
rhoV_E_In_Arr [in MoT]
rhoV_E_In_Nat [in MoT]
rhoV_E_In_Bool [in MoT]
rho_strict [in MoT]
RollInj [in MoT]
RollInjle [in MoT]
RUid [in DomainStuff]
S
SBotIn [in StrictExt]SEBotOutGL [in StrictExt]
SEBotOutL [in StrictExt]
SEChainComplete [in StrictExt]
SEChainCompleteG [in StrictExt]
SEChainCompleteVal [in StrictExt]
SEEpsL [in StrictExt]
SEEpsR [in StrictExt]
SEFunc [in StrictExt]
SEFuncEps [in StrictExt]
SEFuncVal [in StrictExt]
SemExp_LET_KR_equation [in ExSem]
SemExp_NatOp_equation [in ExSem]
SemExp_BoolOp_equation [in ExSem]
SemExp_OrdOp_equation [in ExSem]
SemExp_IFZ_equationVal2 [in ExSem]
SemExp_LET_equationVal2 [in ExSem]
SemExp_NatOp_equationNatNat2 [in ExSem]
SemExp_BoolOp_equationNatNat2 [in ExSem]
SemExp_OrdOp_equationNatNat2 [in ExSem]
SemExp_LET_equationVal [in ExSem]
SemExp_LET_equation_Bot [in ExSem]
SemExp_BoolOp_equation_Bot [in ExSem]
SemExp_OrdOp_equation_Bot [in ExSem]
SemExp_NatOp_equation_Bot [in ExSem]
SemExp_NatOp_equationNatNat [in ExSem]
SemExp_BoolOp_equationNatNat [in ExSem]
SemExp_OrdOp_equationNatNat [in ExSem]
SemExp_VAL_equation [in ExSem]
SEMonEps [in StrictExt]
SemVal_FUN_equation2 [in ExSem]
SemVal_FUN_equation [in ExSem]
SemVal_INT_equation [in ExSem]
SemVal_VAR_equation [in ExSem]
SEPredEpsL [in StrictExt]
SEPredEpsR [in StrictExt]
SEPredL [in StrictExt]
SEPrednthL [in StrictExt]
SEPrednthR [in StrictExt]
SEPredR [in StrictExt]
SEStable [in StrictExt]
SEStableL [in StrictExt]
SEStableR [in StrictExt]
SESym [in StrictExt]
SEValOutL [in StrictExt]
SEValOutR [in StrictExt]
SEValStable [in StrictExt]
shiftConsMap [in Lang]
simpE [in MoT]
simpE' [in MoT]
SimpleB_cont [in DomainStuff]
SimpleB_mon [in DomainStuff]
SimpleU_cont [in DomainStuff]
SimpleU_mon [in DomainStuff]
simplToArr_Pair [in EmbProjPair]
simplToArr_inl_inl [in EmbProjPair]
simplToArr_Arr [in EmbProjPair]
simplToBool_inr [in EmbProjPair]
simplToBool_inl_inr [in EmbProjPair]
simplToBool_inl_inl [in EmbProjPair]
simplToNat_inr [in EmbProjPair]
simplToNat_inl_inr [in EmbProjPair]
simplToNat_Pair [in EmbProjPair]
simplToNat_Arr [in EmbProjPair]
simplToNat_Nat [in EmbProjPair]
simplToPair_Arr [in EmbProjPair]
simplToPair_inl [in EmbProjPair]
simplToPair_Pair [in EmbProjPair]
SmashInv [in DomainStuff]
SmashLemmaValVal [in ExSem]
SmashLemma_Bot [in ExSem]
Smashs_eq [in DomainStuff]
Smash_ValVal [in DomainStuff]
Smash_Val [in DomainStuff]
Smash_Eps_r [in DomainStuff]
Smash_Eps_l [in DomainStuff]
Smash_ValVal [in PredomProd]
Smash_prop [in PredomProd]
Smash_prop_l [in PredomProd]
Smash_prop_r [in PredomProd]
Smash_Val [in PredomProd]
Smash_Eps_l [in PredomProd]
StepI_SemOper [in Adequacy]
StepLemma [in ExSem]
strong_induction [in fib_Adequacy]
substComposeSub [in Lang]
T
tlConsMap [in Lang]toArrBot [in EmbProjPair]
toArrEps [in EmbProjPair]
toArrVal [in EmbProjPair]
toEApp [in MoT]
toFromBool [in EmbProjPair]
toFromNat [in EmbProjPair]
toIDec [in EmbProjPair]
toIEps [in EmbProjPair]
toIProdInv [in EmbProjPair]
toIVal [in EmbProjPair]
toIValB [in EmbProjPair]
toNatBot [in EmbProjPair]
to_const_antiE_b [in Adequacy]
to_const_antiE [in Adequacy]
TranspCC [in StrictExt]
TranspSE [in StrictExt]
TranspStable [in StrictExt]
true_sum_computes [in CoherenceExample]
U
UnCurry_cont [in DomainStuff]UnCurry_mon [in DomainStuff]
URid [in DomainStuff]
V
ValMono [in StrictExt]ValNotBot [in StrictExt]
valNotRelBotL [in StrictExt]
valNotRelBotR [in StrictExt]
ValRule_simpl [in InSem]
VarRule_simpl [in InSem]
VInfToBool_prop [in ExSem]
VInfToFun_Fun [in ExSem]
VInfToNat_prop [in MoT]
VInfToNat_Nat [in ExSem]
_
_EmbProjPair [in EmbProjPair]other
Ω_down_closed [in OperApprox]Constructor Index
A
AndOP [in Lang]APP [in Lang]
App [in OperSem]
AppRule [in Types]
B
BOOL [in Lang]BoolCast [in OperSem]
BoolRule [in Types]
BoolToNatRule [in Types]
BoolTy [in Types]
BOp [in Lang]
BOpRule [in Types]
D
DBOp [in OperSem]DNOp [in OperSem]
DOOp [in OperSem]
E
EFST [in Lang]Empty [in Lang]
EqOP [in Lang]
ESND [in Lang]
F
FibS [in fib_Adequacy]Fib0 [in fib_Adequacy]
Fib1 [in fib_Adequacy]
FstOp [in OperSem]
FSTRule [in Types]
FUN [in Lang]
FunRule [in Types]
FunTy [in Types]
I
IBOp [in OperSem]IFB [in Lang]
IfB [in OperSem]
IfBF [in OperSem]
IfBRule [in Types]
IfBT [in OperSem]
INOp [in OperSem]
IOOp [in OperSem]
L
LeOP [in Lang]LET [in Lang]
LetRule [in Types]
M
MinusOP [in Lang]mkrel [in OperApprox]
mkrelE [in DenoApprox]
N
NAT [in Lang]NatRule [in Types]
NatTy [in Types]
NOp [in Lang]
NOpRule [in Types]
O
OOp [in Lang]OOpRule [in Types]
OrOP [in Lang]
P
PairRule [in Types]PairTy [in Types]
PlusOP [in Lang]
PUSHCond [in Lang]
PUSHLBOp [in Lang]
PUSHLet [in Lang]
PUSHLNOp [in Lang]
PUSHLOOp [in Lang]
PUSHRBOp [in Lang]
PUSHRNOp [in Lang]
PUSHROOp [in Lang]
R
ReflRule [in Types]S
SB [in StrictExt]SBOp [in OperSem]
SLet [in OperSem]
SndOp [in OperSem]
SNDRule [in Types]
SNOp [in OperSem]
SOOp [in OperSem]
SubFunRule [in Types]
SubPairRule [in Types]
SubsRule [in Types]
Subst [in OperSem]
SubsVRule [in Types]
SV [in StrictExt]
SVAR [in Lang]
S_Step [in OperSem]
T
TransRule [in Types]V
VAL [in Lang]ValRule [in Types]
VAR [in Lang]
VarRule [in Types]
VPAIR [in Lang]
Z
ZVAR [in Lang]Z_Step [in OperSem]
Axiom Index
I
Intrinsic_Adequacy_2 [in Adequacy]M
MapExtensional [in Lang]Inductive Index
B
BoolOp [in Lang]E
Expr [in Lang]F
Fib [in fib_Adequacy]FS [in Lang]
L
LType [in Types]N
NatOp [in Lang]O
OrdOp [in Lang]S
SE [in StrictExt]SemOper [in OperSem]
SemOperStep [in OperSem]
T
TypeJudgeE [in Types]TypeJudgeL [in Types]
TypeJudgeV [in Types]
V
V [in Lang]Var [in Lang]
Projection Index
A
antiExec [in DenoApprox]anti_step [in OperApprox]
R
rel [in OperApprox]rel [in DenoApprox]
S
stepI [in OperApprox]V
vl [in Lang]vlvr [in Lang]
vr [in Lang]
W
wk [in Lang]wkvr [in Lang]
Section Index
A
Adequacy1_b [in Adequacy]Adequacy1_n [in Adequacy]
Adequacy2 [in Adequacy]
D
DenoApprox [in DenoApprox]F
Fib_Adequacy.Fib_Sem [in fib_Adequacy]Fib_Adequacy.Fib_Lang [in fib_Adequacy]
Fib_Adequacy [in fib_Adequacy]
M
MAP [in Lang]O
OperApprox [in OperApprox]S
StrictExt [in StrictExt]StrictExtR [in StrictExt]
Definition Index
A
admit [in Utils]AntiexecE [in DenoApprox]
Antiexec_step [in OperApprox]
AppOp [in ExSem]
AppTy [in InSem]
a_fibn [in fib_Adequacy]
B
bool_sum_app [in CoherenceExample]bool_sum [in CoherenceExample]
B_to_N [in DomainStuff]
C
CCURRY [in DomainStuff]chain_complete [in StrictExt]
composeRen [in Lang]
composeRenSub [in Lang]
composeSub [in Lang]
consMap [in Lang]
coq_fib [in fib_Adequacy]
CURRY1_mon [in DomainStuff]
D
Def_Bracketing [in MoT]DenotApproxCtx [in DenoApprox]
DenotApproxE [in DenoApprox]
DenotApproxV [in DenoApprox]
DInfToNat [in MoT]
DownR [in OperApprox]
DownR [in DenoApprox]
E
Env [in Lang]E_False [in CoherenceExample]
E_True [in CoherenceExample]
E_induction [in Lang]
F
F [in DenoApprox]F [in ExSem]
FC [in DenoApprox]
FChain [in DenoApprox]
FChainCore [in DenoApprox]
fibn_sem [in fib_Adequacy]
fibn_syn [in fib_Adequacy]
Fib_body [in fib_Adequacy]
FixF [in InSem]
FSTOp [in ExSem]
FstTy [in InSem]
G
GenBinOp [in ExSem]GenBinOpIn [in MoT]
GenBinOpTy [in InSem]
GenBinOp_DInf [in ExSem]
GenBoolOp [in ExSem]
GenBoolOp_DInf [in ExSem]
GenDenotApproxE [in DenoApprox]
GenDenotApproxV [in DenoApprox]
GenNatOp [in ExSem]
GenNatOp_DInf [in ExSem]
GenOperApproxE [in OperApprox]
GenOperApproxV [in OperApprox]
GenOrdOp [in ExSem]
GenOrdOp_DInf [in ExSem]
GtoE [in EmbProjPair]
H
hdMap [in Lang]I
idMap [in Lang]idRen [in Lang]
idSub [in Lang]
IfB [in DomainStuff]
IfBCore [in DomainStuff]
IfBCoreM [in DomainStuff]
IfBCoreM2 [in DomainStuff]
IfBOp [in ExSem]
IfBTy [in InSem]
IfOneOp [in ExSem]
IfZ [in DomainStuff]
IfZCore [in DomainStuff]
IfZCoreM [in DomainStuff]
IfZCoreM2 [in DomainStuff]
IfZOp [in ExSem]
IF3 [in DomainStuff]
if3 [in DomainStuff]
injnToDInf [in MoT]
InSemE [in InSem]
InSemV [in InSem]
K
KR [in DomainStuff]KUR [in DomainStuff]
L
LCtx [in Types]LetApp [in ExSem]
LetAppDInf [in ExSem]
LetTy [in InSem]
lift [in Lang]
liftRen [in Lang]
liftSub [in Lang]
lookupType [in Types]
lookupV [in Types]
M
Map [in Lang]mapE [in Lang]
mapV [in Lang]
MOD2 [in ExSem]
mod2 [in ExSem]
mutual_VE_induction [in Lang]
N
N_to_B [in DomainStuff]n_steps [in Adequacy]
O
OperApproxCtx [in OperApprox]OperApproxE [in OperApprox]
OperApproxV [in OperApprox]
Operator2_reverse [in DomainStuff]
OpPlus [in DomainStuff]
Op_B_to_N [in OperSem]
P
PAIRL [in DomainStuff]Pairl [in DomainStuff]
PairOp [in ExSem]
PairTy [in InSem]
pprodc_morph [in PredomProd]
prodc_morph [in PredomProd]
PRODc_morph [in PredomProd]
prodm_morph [in PredomProd]
PRODm_morph [in PredomProd]
prod_morph [in PredomProd]
R
RD.biConst [in Domains]RD.biFun [in Domains]
RD.biProd [in Domains]
RD.biSum [in Domains]
RD.biVar [in Domains]
RD.bi_fun [in Domains]
RD.delta [in Domains]
RD.DInf [in Domains]
RD.Fold [in Domains]
RD.FS [in Domains]
RD.inBool [in Domains]
RD.inFun [in Domains]
RD.inNat [in Domains]
RD.inPair [in Domains]
RD.kcpoBaseCatMixin [in Domains]
RD.kcpoCocone [in Domains]
RD.kcpoCone [in Domains]
RD.kcpoLimit [in Domains]
RD.prodm [in Domains]
RD.prod_func [in Domains]
RD.ProjSet [in Domains]
RD.Roll [in Domains]
RD.summ [in Domains]
RD.sum_func [in Domains]
RD.Unfold [in Domains]
RD.Unroll [in Domains]
RD.VInf [in Domains]
RecDom.inBool [in Domains]
RecDom.inFun [in Domains]
RecDom.inNat [in Domains]
RecDom.inPair [in Domains]
RecDom.VInf [in Domains]
RelFunc [in StrictExt]
RelMono [in StrictExt]
RelStable [in StrictExt]
Ren [in Lang]
renE [in Lang]
RenMapOps [in Lang]
renV [in Lang]
rhoC [in MoT]
RhoE [in MoT]
rhoE_To_I_Eq [in MoT]
rhoE_To_I_Geq [in MoT]
rhoE_To_I_Leq [in MoT]
rhoE_E_In [in MoT]
RhoV [in MoT]
rhoV_To_I_Eq [in MoT]
rhoV_To_I_Geq [in MoT]
rhoV_To_I_Leq [in MoT]
rhoV_E_In [in MoT]
S
SemBoolOp [in Lang]SemBoolToNatRule [in Types]
SemCtx [in Types]
SemE [in ExSem]
SemEnv [in ExSem]
SemNatOp [in Lang]
SemOperDiverge [in OperSem]
SemOperStar [in OperSem]
SemOper_n_steps_iSet [in Adequacy]
SemOper_ω_steps [in Adequacy]
SemOper_n_steps [in Adequacy]
SemOrdOp [in Lang]
SemSubFunRule [in Types]
SemType [in Types]
SemTypeJudgeL [in Types]
SemV [in ExSem]
SemVar [in ExSem]
shiftMap [in Lang]
shiftRen [in Lang]
shiftSub [in Lang]
SimpleBOp [in DomainStuff]
SimpleBOpm [in DomainStuff]
SimpleUOp [in DomainStuff]
SimpleUOpm [in DomainStuff]
Smash_reverse [in DomainStuff]
SNDOp [in ExSem]
SndTy [in InSem]
Sub [in Lang]
subE [in Lang]
SubMapOps [in Lang]
subV [in Lang]
T
tlMap [in Lang]toE [in EmbProjPair]
toEArr [in EmbProjPair]
toI [in EmbProjPair]
toIArr [in EmbProjPair]
To_b [in Adequacy]
to_b [in Adequacy]
To_n [in Adequacy]
to_n [in Adequacy]
travE [in Lang]
travV [in Lang]
true_sum_false [in CoherenceExample]
U
UNCURRY [in DomainStuff]UNCURRY_mon [in DomainStuff]
V
VInfToBool [in ExSem]VInfToFun [in ExSem]
VInfToNat [in ExSem]
VInfToPair [in ExSem]
V_v3 [in CoherenceExample]
V_v2 [in CoherenceExample]
V_v1 [in CoherenceExample]
V_v0 [in CoherenceExample]
V_False [in CoherenceExample]
V_True [in CoherenceExample]
V_induction [in Lang]
V_Fib [in fib_Adequacy]
V_Two [in fib_Adequacy]
V_One [in fib_Adequacy]
V_Zero [in fib_Adequacy]
V_v3 [in fib_Adequacy]
V_v2 [in fib_Adequacy]
V_v1 [in fib_Adequacy]
V_v0 [in fib_Adequacy]
v0 [in CoherenceExample]
v0 [in fib_Adequacy]
V0_eq_1 [in fib_Adequacy]
V0_eq_0 [in fib_Adequacy]
v1 [in CoherenceExample]
v1 [in fib_Adequacy]
v2 [in CoherenceExample]
v2 [in fib_Adequacy]
v3 [in CoherenceExample]
v3 [in fib_Adequacy]
_
_toEArr [in EmbProjPair]_toIArr [in EmbProjPair]
_rho [in MoT]
_delta [in MoT]
other
Ω [in OperApprox]Ω [in DenoApprox]
Record Index
M
MapOps [in Lang]R
RelE [in OperApprox]RelE [in DenoApprox]
| 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 | (974 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 | (109 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 | (2 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 | (27 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 | (17 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 | (455 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 | (83 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 | (2 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 | (15 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 | (10 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 | (11 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 | (240 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 | (3 entries) |
This page has been generated by coqdoc