Nuprl Definition : mk_deq

mk_deq(p) ==  λx,y. isl(p y)



Definitions occuring in Statement :  isl: isl(x) apply: a lambda: λx.A[x]
Definitions occuring in definition :  lambda: λx.A[x] isl: isl(x) apply: a
FDL editor aliases :  mk_deq

Latex:
mk\_deq(p)  ==    \mlambda{}x,y.  isl(p  x  y)



Date html generated: 2016_05_14-AM-06_06_30
Last ObjectModification: 2015_09_22-PM-05_48_11

Theory : equality!deciders


Home Index