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>
Definitions occuring in definition :
evalall: evalall(t),
ex-evd-proof-check: ex-evd-proof-check(exname;sequent;F),
lambda: λx.A[x],
pair: <a, b>,
nil: []
Latex:
uniform-evd-proof-check(exname; fmla; evd) == evalall(ex-evd-proof-check(exname;<[], fmla><\mlambda{}M.evd,\000C [], []>))
Date html generated:
2016_05_15-PM-10_33_21
Last ObjectModification:
2015_09_23-AM-08_26_44
Theory : minimal-first-order-logic
Home
Index