Nuprl Definition : fun-evd-proof-step
fun-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
fun-do-Intro(exname;H;G;numhyps;v;fullevd)?exname:n.fun-do-Elim(exname;H;G;numhyps;n;fullevd)
Definitions occuring in Statement :
fun-do-Elim: fun-do-Elim(exname;H;G;numhyps;m';fullevd),
fun-do-Intro: fun-do-Intro(exname;H;G;numhyps;val;fullevd),
length: ||as||,
callbyvalue: callbyvalue,
apply: f a,
spread: spread def
Definitions occuring in definition :
fun-do-Elim: fun-do-Elim(exname;H;G;numhyps;m';fullevd),
fun-do-Intro: fun-do-Intro(exname;H;G;numhyps;val;fullevd),
apply: f a,
callbyvalue: callbyvalue,
spread: spread def,
length: ||as||
FDL editor aliases :
fun-evd-proof-step
Latex:
fun-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
fun-do-Intro(exname;H;G;numhyps;v;fullevd)?exname:n.fun-do-Elim(exname;H;G;numhyps;n;...)
Date html generated:
2017_01_19-PM-02_32_21
Last ObjectModification:
2017_01_18-PM-06_41_07
Theory : minimal-first-order-logic
Home
Index