Nuprl Definition : lift-predicate
P? == λX.((X)↓ ⇒ (P X))
Definitions occuring in Statement :
has-value: (a)↓,
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
implies: P ⇒ Q,
has-value: (a)↓,
apply: f a
FDL editor aliases :
lift-predicate
Latex:
P? == \mlambda{}X.((X)\mdownarrow{} {}\mRightarrow{} (P X))
Date html generated:
2016_05_15-PM-10_04_25
Last ObjectModification:
2015_09_23-AM-08_22_07
Theory : bar!type
Home
Index