Nuprl Definition : lifting2
lifting2(f;abag;bbag) == lifting-gen-rev(2;f;λx.[abag; bbag][x])
Definitions occuring in Statement :
lifting-gen-rev: lifting-gen-rev(n;f;bags),
select: L[n],
cons: [a / b],
nil: [],
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
lifting-gen-rev: lifting-gen-rev(n;f;bags),
natural_number: $n,
lambda: λx.A[x],
select: L[n],
cons: [a / b],
nil: []
FDL editor aliases :
lifting2
Latex:
lifting2(f;abag;bbag) == lifting-gen-rev(2;f;\mlambda{}x.[abag; bbag][x])
Date html generated:
2016_05_15-PM-03_00_59
Last ObjectModification:
2015_09_23-AM-07_41_01
Theory : bags
Home
Index