Nuprl Definition : RankEx1co
RankEx1co(T) ==
corec(X.lbl:Atom × if lbl =a "Leaf" then T
if lbl =a "Prod" then X × X
if lbl =a "ProdL" then T × X
if lbl =a "ProdR" then X × T
if lbl =a "List" then X List
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,
product: x:A × B[x],
token: "$token",
atom: Atom,
void: Void
FDL editor aliases :
RankEx1co
RankEx1co(T) ==
corec(X.lbl:Atom \mtimes{} if lbl =a "Leaf" then T
if lbl =a "Prod" then X \mtimes{} X
if lbl =a "ProdL" then T \mtimes{} X
if lbl =a "ProdR" then X \mtimes{} T
if lbl =a "List" then X List
else Void
fi )
Date html generated:
2015_07_17-AM-07_47_25
Last ObjectModification:
2014_05_06-PM-02_30_47
Home
Index