Nuprl Definition : ex-evd-proof-step
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Definitions occuring in Statement :
ex-do-Elim: ex-do-Elim(exname;H;G;numhyps;m';fullevd),
ex-do-Intro: ex-do-Intro(exname; H; G; numhyps; val; fullevd),
length: ||as||,
callbyvalue: callbyvalue,
apply: f a,
spread: spread def
ex-evd-proof-step(exname; sequent; fullevd) ==
let H,G = sequent
in eval numhyps = ||H|| in
let F,M = fullevd
in eval v = F M in
ex-do-Intro(exname; H; G; numhyps; v; fullevd
)?exname:n.ex-do-Elim(exname;H;G;numhyps;n;fullevd)
Date html generated:
2015_07_17-AM-07_57_46
Last ObjectModification:
2014_06_12-PM-10_34_50
Home
Index