Nuprl Definition : list_proof_to_W_proof
list_proof_to_W_proof(p)
==r let sr,subgoals = p
in let L ⟵ map(λp.list_proof_to_W_proof(p);subgoals)
in <sr, list-to-fun(L)>
list_proof_to_W_proof(p) ==
fix((λlist_proof_to_W_proof,p. let sr,subgoals = p
in let L ⟵ map(λp.(list_proof_to_W_proof p);subgoals)
in <sr, list-to-fun(L)>))
p
Definitions occuring in Statement :
list-to-fun: list-to-fun(L),
map: map(f;as),
callbyvalueall: callbyvalueall,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>
Definitions occuring in definition :
fix: fix(F),
spread: spread def,
callbyvalueall: callbyvalueall,
map: map(f;as),
lambda: λx.A[x],
apply: f a,
pair: <a, b>,
list-to-fun: list-to-fun(L)
FDL editor aliases :
list_proof_to_W_proof
Latex:
list\_proof\_to\_W\_proof(p)
==r let sr,subgoals = p
in let L \mleftarrow{}{} map(\mlambda{}p.list\_proof\_to\_W\_proof(p);subgoals)
in <sr, list-to-fun(L)>
Latex:
list\_proof\_to\_W\_proof(p) ==
fix((\mlambda{}list\_proof\_to\_W$_{proof}$,p. let sr,subgoals = p
in let L \mleftarrow{}{} map(\mlambda{}p.(list\_proof\_to\_W$_{proof}$ p)\000C;subgoals)
in <sr, list-to-fun(L)>))
p
Date html generated:
2016_05_15-PM-10_33_13
Last ObjectModification:
2015_09_25-PM-04_03_06
Theory : minimal-first-order-logic
Home
Index