Nuprl Definition : type-functor-sum
p + q ==
let F,MF = p
in let G,MG = q
in <λT.(F T + (G T)), λf,d. case d of inl(x) => inl (MF f x) | inr(y) => inr (MG f y) >
Definitions occuring in Statement :
apply: f a,
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
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 b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
inr: inr x ,
apply: f a
Latex:
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