Nuprl Definition : note-is-function
note-is-function(A;hnum;M) == if mFOLisImp(A) ∨bmFOLisAll(A) then M[hnum:= `function`] else M fi
Definitions occuring in Statement :
modelAdd: M[n:= lbl,i,j],
mFOLisAll: mFOLisAll(A),
mFOLisImp: mFOLisImp(A),
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
natural_number: $n,
token: "$token"
FDL editor aliases :
note-is-function
note-is-function(A;hnum;M) == if mFOLisImp(A) \mvee{}\msubb{}mFOLisAll(A) then M[hnum:= `function`] else M fi
Date html generated:
2015_07_17-AM-07_57_40
Last ObjectModification:
2013_04_19-PM-06_47_08
Home
Index