Nuprl Definition : new-evd-to-proof
new-evd-to-proof(G;evd) == let p ⟵ ν(ex.new-evd-proof(ex;<[], G>;λM.evd)) in p
Definitions occuring in Statement :
new-evd-proof: new-evd-proof(exname;sequent;evd),
nil: [],
callbyvalueall: callbyvalueall,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
new-evd-proof: new-evd-proof(exname;sequent;evd),
pair: <a, b>,
nil: [],
lambda: λx.A[x]
FDL editor aliases :
new-evd-to-proof
Latex:
new-evd-to-proof(G;evd) == let p \mleftarrow{}{} \mnu{}(ex.new-evd-proof(ex;<[], G>\mlambda{}M.evd)) in p
Date html generated:
2016_05_15-PM-10_33_46
Last ObjectModification:
2015_12_09-PM-00_42_45
Theory : minimal-first-order-logic
Home
Index