Nuprl Definition : pi_term_ind
... ==
fix((λpi_term_ind,v. let lbl,v1 = v
in if lbl="zero" then zero
if lbl="comm" then let pre,v2 = v1 in comm[pre; v2; pi_term_ind v2]
if lbl="option" then let left,v2 = v1 in option[left; v2; pi_term_ind left; pi_term_ind v2]
if lbl="par" then let left,v2 = v1 in par[left; v2; pi_term_ind left; pi_term_ind v2]
if lbl="rep" then rep[v1; pi_term_ind v1]
if lbl="new" then let name,v2 = v1 in new[name; v2; pi_term_ind v2]
else ⊥
fi ))
v
Definitions occuring in Statement :
bottom: ⊥,
atom_eq: if a=b then c else d fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
token: "$token"
FDL editor aliases :
pi_term_ind
pi_ind
Latex:
... ==
fix((\mlambda{}pi\_term$_{ind}$,v. let lbl,v1 = v
in if lbl="zero" then zero
if lbl="comm" then let pre,v2 = v1 in comm[pre; v2; pi\_term$_{i\000Cnd}$ v2]
if lbl="option"
then let left,v2 = v1
in option[left; v2; pi\_term$_{ind}$ left; pi\_ter\000Cm$_{ind}$ v2]
if lbl="par"
then let left,v2 = v1
in par[left; v2; pi\_term$_{ind}$ left; pi\_term\mbackslash{}f\000Cf24_{ind}$ v2]
if lbl="rep" then rep[v1; pi\_term$_{ind}$ v1]
if lbl="new" then let name,v2 = v1 in new[name; v2; pi\_term$_{i\000Cnd}$ v2]
else \mbot{}
fi ))
v
Date html generated:
2015_07_23-AM-11_32_46
Last ObjectModification:
2014_05_04-PM-08_23_26
Home
Index