Nuprl Definition : int_formulaco
int_formulaco() ==
corec(X.lbl:Atom × if lbl =a "less" then left:int_term() × int_term()
if lbl =a "le" then left:int_term() × int_term()
if lbl =a "eq" then left:int_term() × int_term()
if lbl =a "and" then left:X × X
if lbl =a "or" then left:X × X
if lbl =a "implies" then left:X × X
if lbl =a "not" then X
else Void
fi )
Definitions occuring in Statement :
int_term: int_term(),
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]),
atom: Atom,
int_term: int_term(),
product: x:A × B[x],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
token: "$token",
void: Void
FDL editor aliases :
int_formulaco
Latex:
int\_formulaco() ==
corec(X.lbl:Atom \mtimes{} if lbl =a "less" then left:int\_term() \mtimes{} int\_term()
if lbl =a "le" then left:int\_term() \mtimes{} int\_term()
if lbl =a "eq" then left:int\_term() \mtimes{} int\_term()
if lbl =a "and" then left:X \mtimes{} X
if lbl =a "or" then left:X \mtimes{} X
if lbl =a "implies" then left:X \mtimes{} X
if lbl =a "not" then X
else Void
fi )
Date html generated:
2016_05_14-AM-07_04_04
Last ObjectModification:
2015_09_22-PM-05_51_55
Theory : omega
Home
Index