Nuprl Definition : lifting1
lifting1(f;b) == lifting-gen-rev(1;f;λx.b)
Definitions occuring in Statement :
lifting-gen-rev: lifting-gen-rev(n;f;bags),
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]
FDL editor aliases :
lifting1
Latex:
lifting1(f;b) == lifting-gen-rev(1;f;\mlambda{}x.b)
Date html generated:
2016_05_15-PM-03_00_47
Last ObjectModification:
2015_09_23-AM-07_40_56
Theory : bags
Home
Index