Nuprl Definition : mFOLco

mFOLco() ==
  corec(X.lbl:Atom × if lbl =a "atomic" then name:Atom × (ℤ List)
                     if lbl =a "connect" then knd:Atom × left:X × X
                     if lbl =a "quant" then isall:𝔹 × var:ℤ × X
                     else Void
                     fi )



Definitions occuring in Statement :  list: List corec: corec(T.F[T]) ifthenelse: if then else fi  eq_atom: =a y bool: 𝔹 product: x:A × B[x] int: token: "$token" atom: Atom void: Void
FDL editor aliases :  mFOLco
mFOLco()  ==
    corec(X.lbl:Atom  \mtimes{}  if  lbl  =a  "atomic"  then  name:Atom  \mtimes{}  (\mBbbZ{}  List)
                                          if  lbl  =a  "connect"  then  knd:Atom  \mtimes{}  left:X  \mtimes{}  X
                                          if  lbl  =a  "quant"  then  isall:\mBbbB{}  \mtimes{}  var:\mBbbZ{}  \mtimes{}  X
                                          else  Void
                                          fi  )



Date html generated: 2015_07_17-AM-07_53_19
Last ObjectModification: 2014_04_30-PM-01_13_49

Home Index