Nuprl Definition : pi-choices
pi-choices(t) == pi_term_ind(t;[];pr,P,r.[<pr, P>];P,Q,cp,cq.cp @ cq;P,Q,a,b.[];P,a.[];x,P,a.[])
Definitions occuring in Statement :
pi_term_ind: pi_term_ind(v;zero;pre,body,rec1....;left,right,rec2,rec3....;left,right,rec4,rec5....;body,rec6....;name,body,rec7....),
append: as @ bs,
cons: [a / b],
nil: [],
pair: <a, b>
FDL editor aliases :
pi-choices
Latex:
pi-choices(t) == pi\_term\_ind(t;[];pr,P,r.[<pr, P>];P,Q,cp,cq.cp @ cq;P,Q,a,b.[];P,a.[];x,P,a.[])
Date html generated:
2015_07_23-AM-11_33_55
Last ObjectModification:
2012_08_30-PM-01_19_45
Home
Index