Nuprl Definition : concat-lifting-0
concat-lifting-0(f) ==  concat-lifting(0;f;λn.[][n])
Definitions occuring in Statement : 
concat-lifting: concat-lifting(n;f;bags)
, 
select: L[n]
, 
nil: []
, 
lambda: λx.A[x]
, 
natural_number: $n
Definitions occuring in definition : 
concat-lifting: concat-lifting(n;f;bags)
, 
natural_number: $n
, 
lambda: λx.A[x]
, 
select: L[n]
, 
nil: []
FDL editor aliases : 
concat-lifting-0
Latex:
concat-lifting-0(f)  ==    concat-lifting(0;f;\mlambda{}n.[][n])
Date html generated:
2016_05_15-PM-03_07_33
Last ObjectModification:
2015_09_23-AM-07_41_56
Theory : bags
Home
Index