Nuprl Definition : new-evd-proof-step
NewEvdProofStep(exname;sequent;evd) ==
let H,G = sequent
in eval numhyps = ||H|| in
eval v = evd probe(H;exname) in
new-do-Intro(exname;H;G;numhyps;v;evd)?exname:n.new-do-Elim(exname;H;G;numhyps;n;evd)
Definitions occuring in Statement :
probe: probe(H;exname),
new-do-Elim: new-do-Elim(exname;H;G;numhyps;m';evd),
new-do-Intro: new-do-Intro(exname;H;G;numhyps;val;evd),
length: ||as||,
callbyvalue: callbyvalue,
apply: f a,
spread: spread def
Definitions occuring in definition :
spread: spread def,
length: ||as||,
callbyvalue: callbyvalue,
apply: f a,
probe: probe(H;exname),
new-do-Intro: new-do-Intro(exname;H;G;numhyps;val;evd),
new-do-Elim: new-do-Elim(exname;H;G;numhyps;m';evd)
FDL editor aliases :
new-evd-proof-step
Latex:
NewEvdProofStep(exname;sequent;evd) ==
let H,G = sequent
in eval numhyps = ||H|| in
eval v = evd probe(H;exname) in
new-do-Intro(exname;H;G;numhyps;v;evd)?exname:n.new-do-Elim(exname;H;G;numhyps;n;evd)
Date html generated:
2016_05_15-PM-10_33_37
Last ObjectModification:
2016_02_04-PM-02_30_59
Theory : minimal-first-order-logic
Home
Index