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: T List,
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bool: 𝔹,
product: x:A × B[x],
int: ℤ,
token: "$token",
atom: Atom,
void: Void
Definitions occuring in definition :
corec: corec(T.F[T]),
list: T List,
atom: Atom,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
token: "$token",
bool: 𝔹,
product: x:A × B[x],
int: ℤ,
void: Void
FDL editor aliases :
mFOLco
Latex:
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:
2016_05_15-PM-10_12_44
Last ObjectModification:
2015_09_23-AM-08_22_48
Theory : minimal-first-order-logic
Home
Index