Nuprl Definition : ctt-binder-context
ctt-binder-context ==
λX,vs,f,trs,bt. if ||trs|| <z ||ctt-arity(f)||
∧b (||fst(bt)|| =z fst(ctt-arity(f)[||trs||]))
∧b bdd-all(||trs||;i.(ctt-kind(snd(fst(snd(trs[i])))) =z snd(ctt-arity(f)[i])))
then provisional-subterm-context{i:l}(X;f;fst(bt);trs)
else X
fi
Definitions occuring in Statement :
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L)
,
ctt-arity: ctt-arity(x)
,
ctt-kind: ctt-kind(t)
,
select: L[n]
,
length: ||as||
,
bdd-all: bdd-all(n;i.P[i])
,
band: p ∧b q
,
ifthenelse: if b then t else f fi
,
lt_int: i <z j
,
eq_int: (i =z j)
,
pi1: fst(t)
,
pi2: snd(t)
,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x]
,
ifthenelse: if b then t else f fi
,
lt_int: i <z j
,
band: p ∧b q
,
bdd-all: bdd-all(n;i.P[i])
,
length: ||as||
,
eq_int: (i =z j)
,
ctt-kind: ctt-kind(t)
,
pi2: snd(t)
,
select: L[n]
,
ctt-arity: ctt-arity(x)
,
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L)
,
pi1: fst(t)
FDL editor aliases :
ctt-binder-context
Latex:
ctt-binder-context ==
\mlambda{}X,vs,f,trs,bt. if ||trs|| <z ||ctt-arity(f)||
\mwedge{}\msubb{} (||fst(bt)|| =\msubz{} fst(ctt-arity(f)[||trs||]))
\mwedge{}\msubb{} bdd-all(||trs||;i.(ctt-kind(snd(fst(snd(trs[i])))) =\msubz{} snd(ctt-arity(f)[i])))
then provisional-subterm-context\{i:l\}(X;f;fst(bt);trs)
else X
fi
Date html generated:
2020_05_21-AM-10_38_07
Last ObjectModification:
2020_03_13-AM-11_13_34
Theory : cubical!type!theory
Home
Index