Nuprl Definition : uniform-evd-to-proof
uniform-evd-to-proof(G;evd) == evalall(ν(ex.ex-evd-proof(ex;<[], G>;<λM.evd, [], []>)))
Definitions occuring in Statement :
ex-evd-proof: ex-evd-proof(exname;sequent;F),
nil: [],
evalall: evalall(t),
lambda: λx.A[x],
pair: <a, b>
FDL editor aliases :
uniform-evd-to-proof
uniform-evd-to-proof(G;evd) == evalall(\mnu{}(ex.ex-evd-proof(ex;<[], G><\mlambda{}M.evd, [], []>)))
Date html generated:
2015_07_17-AM-07_57_49
Last ObjectModification:
2015_03_25-AM-10_15_38
Home
Index