Nuprl Definition : test-mutual-corec

test-mutual-corec() ==
  mutual-corec(X.λi.if (i =z 0) then Unit + (X 0 × ((X 1) List)) else Unit + (X 1 × ((X 0) List)) fi )


Definitions occuring in Statement :  list: T List,  mutual-corec: mutual-corec(T.F[T]),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  unit: Unit,  apply: f a,  lambda: λx.A[x],  product: x:A × B[x],  union: left + right,  natural_number: $n
Definitions occuring in definition :  mutual-corec: mutual-corec(T.F[T]),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  union: left + right,  unit: Unit,  product: x:A × B[x],  list: T List,  apply: f a,  natural_number: $n
FDL editor aliases :  test-mutual-corec
Latex:
test-mutual-corec()  ==
    mutual-corec(X.\mlambda{}i.if  (i  =\msubz{}  0)
                                        then  Unit  +  (X  0  \mtimes{}  ((X  1)  List))
                                        else  Unit  +  (X  1  \mtimes{}  ((X  0)  List))
                                        fi  )


Date html generated: 2018_05_21-PM-00_31_16
Last ObjectModification: 2017_10_18-PM-04_15_51

Theory : int_2


Home Index