Nuprl Definition : rv-qle
A ≤ B == λs.if q_le(A s;B s) then 1 else 0 fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
natural_number: $n,
q_le: q_le(r;s)
Definitions :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
q_le: q_le(r;s),
apply: f a,
natural_number: $n
FDL editor aliases :
rv-qle
A \mleq{} B == \mlambda{}s.if q\_le(A s;B s) then 1 else 0 fi
Date html generated:
2015_07_17-AM-07_58_47
Last ObjectModification:
2008_02_27-PM-05_48_25
Home
Index