Nuprl Definition : uniform-evd-proof-check
uniform-evd-proof-check(exname; fmla; evd) == evalall(ex-evd-proof-check(exname;<[], fmla>;<λM.evd, [], []>))
Definitions occuring in Statement :
ex-evd-proof-check: ex-evd-proof-check(exname;sequent;F),
nil: [],
evalall: evalall(t),
lambda: λx.A[x],
pair: <a, b>
uniform-evd-proof-check(exname; fmla; evd) == evalall(ex-evd-proof-check(exname;<[], fmla><\mlambda{}M.evd,\000C [], []>))
Date html generated:
2015_07_17-AM-07_57_51
Last ObjectModification:
2014_06_12-PM-05_44_07
Home
Index