Nuprl Definition : type-functor-sum

  let F,MF 
  in let G,MG 
     in <λT.(F (G T)), λf,d. case of inl(x) => inl (MF x) inr(y) => inr (MG y) >

Definitions occuring in Statement :  apply: a lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x union: left right
Definitions occuring in definition :  spread: spread def pair: <a, b> union: left right lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inl: inl x inr: inr  apply: a

p  +  q  ==
    let  F,MF  =  p 
    in  let  G,MG  =  q 
          in  <\mlambda{}T.(F  T  +  (G  T)),  \mlambda{}f,d.  case  d  of  inl(x)  =>  inl  (MF  f  x)  |  inr(y)  =>  inr  (MG  f  y)  >

Date html generated: 2016_05_15-PM-01_44_48
Last ObjectModification: 2015_09_23-AM-07_37_01

Theory : basic

Home Index