Nuprl Definition : awf-example1
awf-example1() == λg,i. [inr [awf-leaf(1); g 2] ; inr [g 0; g 2] ; inr [g 0; g 1; g 2] ][i]
Definitions occuring in Statement :
awf-leaf: awf-leaf(x),
select: L[n],
cons: [a / b],
nil: [],
apply: f a,
lambda: λx.A[x],
inr: inr x ,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
select: L[n],
awf-leaf: awf-leaf(x),
inr: inr x ,
cons: [a / b],
apply: f a,
natural_number: $n,
nil: []
FDL editor aliases :
awf-example1
Latex:
awf-example1() == \mlambda{}g,i. [inr [awf-leaf(1); g 2] ; inr [g 0; g 2] ; inr [g 0; g 1; g 2] ][i]
Date html generated:
2016_05_15-PM-07_27_07
Last ObjectModification:
2015_09_23-AM-08_15_15
Theory : general
Home
Index