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