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