Nuprl Definition : per-function
per-function(A;a.B[a]) == pertype(λf,g. function-eq(A;a.B[a];f;g))
Definitions occuring in Statement :
function-eq: function-eq(A;a.B[a];f;g),
pertype: pertype(R),
lambda: λx.A[x]
Definitions occuring in definition :
pertype: pertype(R),
lambda: λx.A[x],
function-eq: function-eq(A;a.B[a];f;g)
Rules referencing :
perfunctionExtensionality
FDL editor aliases :
per-function
Latex:
per-function(A;a.B[a]) == pertype(\mlambda{}f,g. function-eq(A;a.B[a];f;g))
Date html generated:
2016_05_13-PM-03_53_37
Last ObjectModification:
2015_09_22-PM-05_45_31
Theory : per!type
Home
Index