Nuprl Definition : Formco
Formco(C) ==
corec(X.lbl:Atom × if lbl =a "Var" then Atom
if lbl =a "Const" then C
if lbl =a "Set" then var:Atom × X
if lbl =a "Equal" then left:X × X
if lbl =a "Member" then element:X × X
if lbl =a "And" then left:X × X
if lbl =a "Or" then left:X × X
if lbl =a "Not" then X
if lbl =a "All" then var:Atom × X
if lbl =a "Exists" then var:Atom × X
else Void
fi )
Definitions occuring in Statement :
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
Definitions occuring in definition :
corec: corec(T.F[T]),
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
token: "$token",
product: x:A × B[x],
atom: Atom,
void: Void
FDL editor aliases :
Formco
Formco
Latex:
Formco(C) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Var" then Atom
if lbl =a "Const" then C
if lbl =a "Set" then var:Atom \mtimes{} X
if lbl =a "Equal" then left:X \mtimes{} X
if lbl =a "Member" then element:X \mtimes{} X
if lbl =a "And" then left:X \mtimes{} X
if lbl =a "Or" then left:X \mtimes{} X
if lbl =a "Not" then X
if lbl =a "All" then var:Atom \mtimes{} X
if lbl =a "Exists" then var:Atom \mtimes{} X
else Void
fi )
Date html generated:
2018_05_21-PM-10_41_54
Last ObjectModification:
2017_10_10-PM-04_30_31
Theory : PZF
Home
Index