Nuprl Definition : change-from1
change-from1(a) == λn.if n=0 then ff else if a 1=a 0 then tt else ff
Definitions occuring in Statement :
bfalse: ff,
btrue: tt,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
bfalse: ff,
btrue: tt,
natural_number: $n,
apply: f a,
int_eq: if a=b then c else d,
lambda: λx.A[x]
FDL editor aliases :
change-from1
Latex:
change-from1(a) == \mlambda{}n.if n=0 then ff else if a 1=a 0 then tt else ff
Date html generated:
2017_04_21-AM-11_23_17
Last ObjectModification:
2017_04_20-PM-04_55_10
Theory : continuity
Home
Index