Nuprl Definition : update-context-lvl
update-context-lvl(ctxt;lvl;T;v) ==
let X,vs,f = ctxt in
<X.T, [v / vs], λx.if eq_var(x;v) then var-term-meaning(lvl;T) else (f x)p fi >
Definitions occuring in Statement :
var-term-meaning: var-term-meaning(lvl;T),
csm-ap-term-meaning: (t)s,
cc-fst: p,
cube-context-adjoin: X.A,
eq_var: eq_var(a;b),
cons: [a / b],
ifthenelse: if b then t else f fi ,
spreadn: spread3,
apply: f a,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
spreadn: spread3,
cube-context-adjoin: X.A,
pair: <a, b>,
cons: [a / b],
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_var: eq_var(a;b),
var-term-meaning: var-term-meaning(lvl;T),
csm-ap-term-meaning: (t)s,
cc-fst: p,
apply: f a
FDL editor aliases :
update-context-lvl
Latex:
update-context-lvl(ctxt;lvl;T;v) ==
let X,vs,f = ctxt in
<X.T, [v / vs], \mlambda{}x.if eq\_var(x;v) then var-term-meaning(lvl;T) else (f x)p fi >
Date html generated:
2020_05_20-PM-08_07_39
Last ObjectModification:
2020_05_04-AM-11_14_44
Theory : cubical!type!theory
Home
Index