Nuprl Definition : apply def
f a == PRIMITIVE
Rules referencing :
imageMemberEquality,
imageElimination,
imageEqInduction,
dependent_functionElimination,
applyEquality,
functionExtensionality,
independent_functionElimination,
cut,
comment,
barInduction,
bar_Induction,
strong_bar_Induction,
Continuity,
StrongContinuity2,
compactness,
fixpointLeast,
freeFromAtomApplication,
callbyvalueApply,
sqleLambda,
applyPair,
applyInl,
applyInr,
applyInt,
applyExceptionCases,
islambdaCases,
pertypeEquality,
pertypeMemberEquality,
pertypeElimination,
perfunctionExtensionality,
allFunctionality,
uallFunctionality,
impliesFunctionality
FDL editor aliases :
ap
Latex:
f a == PRIMITIVE
Date html generated:
2016_05_13-PM-03_04_00
Last ObjectModification:
2006_01_26-PM-03_54_57
Theory : core_1
Home
Index