Nuprl Definition : nc-r'
g,i=1-j == λx.if (x =z i) then <1-j> else g x fi
Definitions occuring in Statement :
dM_opp: <1-x>,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
dM_opp: <1-x>,
apply: f a
FDL editor aliases :
nc-r'
Latex:
g,i=1-j == \mlambda{}x.if (x =\msubz{} i) then ə-j> else g x fi
Date html generated:
2016_05_18-PM-00_04_28
Last ObjectModification:
2015_11_11-PM-09_41_45
Theory : cubical!type!theory
Home
Index