Nuprl Definition : mFO-dest-atomic
let a,b = dest-atomic(fmla) in
F[a; b] ==
if mFOatomic?(fmla) then F[mFOatomic-name(fmla); mFOatomic-vars(fmla)] else inr ⋅ fi
Definitions occuring in Statement :
mFOatomic-vars: mFOatomic-vars(v),
mFOatomic-name: mFOatomic-name(v),
mFOatomic?: mFOatomic?(v),
ifthenelse: if b then t else f fi ,
it: ⋅,
inr: inr x
FDL editor aliases :
mFO-dest-atomic
let a,b = dest-atomic(fmla) in
F[a; b] ==
if mFOatomic?(fmla) then F[mFOatomic-name(fmla); mFOatomic-vars(fmla)] else inr \mcdot{} fi
Date html generated:
2015_07_17-AM-07_53_56
Last ObjectModification:
2012_09_04-AM-00_26_41
Home
Index