Nuprl Definition : cube+
cube+(I;i) == λA,fx. let f,x = fx in λj.if (j =z i) then x else f j fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
spread: spread def,
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a
FDL editor aliases :
cube+
Latex:
cube+(I;i) == \mlambda{}A,fx. let f,x = fx in \mlambda{}j.if (j =\msubz{} i) then x else f j fi
Date html generated:
2016_05_18-PM-02_01_35
Last ObjectModification:
2016_03_21-AM-01_32_47
Theory : cubical!type!theory
Home
Index