Nuprl Definition : RankEx2co

RankEx2co(S;T) ==
  corec(X.lbl:Atom × if lbl =a "LeafT" then T
                     if lbl =a "LeafS" then S
                     if lbl =a "Prod" then X × S × T
                     if lbl =a "Union" then S × X + X
                     if lbl =a "ListProd" then (S × X) List
                     if lbl =a "UnionList" then T + (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], union: left + right, token: "$token", atom: Atom, void: Void
FDL editor aliases : RankEx2co
RankEx2co(S;T) == corec(X.lbl:Atom \mtimes{} if lbl =a "LeafT" then T if lbl =a "LeafS" then S if lbl =a "Prod" then X \mtimes{} S \mtimes{} T if lbl =a "Union" then S \mtimes{} X + X if lbl =a "ListProd" then (S \mtimes{} X) List if lbl =a "UnionList" then T + (X List) else Void fi ) Date html generated: 2015_07_17-AM-07_48_47 Last ObjectModification: 2014_05_06-PM-01_37_43 Home Index